✐‹creator "Kevin Kappelmann"› subsection ‹Basic Properties› theory Function_Properties imports Functions_Bijection Functions_Injective Functions_Inverse Functions_Monotone Functions_Surjective begin paragraph ‹Summary› text ‹Basic properties on functions.› end