English
An increasing function (monotone with respect to r and s) is injective.
Русский
Неубываящая функция относительно отношений r и s является инъективной.
LaTeX
$$$\text{injective } f$ given $f$ preserves order: \forall x y, r x y \Rightarrow s (f x) (f y)$, with appropriate trichotomy and irreflexivity assumptions.$$
Lean4
/-- An increasing function is injective -/
theorem injective_of_increasing (r : α → α → Prop) (s : β → β → Prop) [IsTrichotomous α r] [IsIrrefl β s] (f : α → β)
(hf : ∀ {x y}, r x y → s (f x) (f y)) : Injective f :=
by
intro x y hxy
rcases trichotomous_of r x y with (h | h | h)
· have := hf h
rw [hxy] at this
exfalso
exact irrefl_of s (f y) this
· exact h
· have := hf h
rw [hxy] at this
exfalso
exact irrefl_of s (f y) this
