Strictly_Monotone_Mapping_with_Totally_Ordered_Domain_is_Injective
Provedinjectionsmonotone-mappingsorder-theoryproofwiki
Let (S, ≤₁) be a totally ordered set and (T, ≤₂) be an ordered set. A strictly monotone mapping φ: S → T is injective.
Preamble
import Mathlib.Order.Monotone.Basic import Mathlib.Logic.Function.Basic
Formal statement
theorem Strictly_Monotone_Mapping_with_Totally_Ordered_Domain_is_Injective {α : Type _} {β : Type _} [LinearOrder α] [Preorder β] {f : α → β} (hf : StrictMono f) : Function.Injective f := by sorrySource