Monomorphism_from_Total_Ordering
Provedmonomorphismsproofwikitotal-orderings
Let the following conditions hold Let and be ordered semigroups. Let be a mapping. Let be a total ordering on . Then is a (structure) monomorphism iff is strictly increasing from into ; is a homomorphism from into .
Preamble
import Mathlib.Order.Hom.Basic import Mathlib.Algebra.Group.Defs
Formal statement
theorem Monomorphism_from_Total_Ordering {S T : Type _} [LinearOrder S] [LinearOrder T] [Mul S] [Mul T] (f : S → T) (hf : StrictMono f) : Function.Injective f := by sorrySource