English
Let f be strictly monotone on a set S. Then for all a,b ∈ S and every ordering o, the relation o compares f(a) and f(b) is equivalent to o compares a and b.
Русский
Пусть f строго монотонна на множестве S. Тогда для любых a,b ∈ S и любого порядка o выполняется: o сравнивает f(a) и f(b) тогда и только тогда, когда o сравнивает a и b.
LaTeX
$$$ (hf : StrictMonoOn f s) \rightarrow \forall a \in s, \forall b \in s, \forall o : Ordering, o.Compares (f a) (f b) \leftrightarrow o.Compares a b $$$
Lean4
protected theorem compares (hf : StrictMonoOn f s) {a b : α} (ha : a ∈ s) (hb : b ∈ s) :
∀ {o : Ordering}, o.Compares (f a) (f b) ↔ o.Compares a b
| Ordering.lt => hf.lt_iff_lt ha hb
| Ordering.eq => ⟨fun h ↦ ((hf.le_iff_le ha hb).1 h.le).antisymm ((hf.le_iff_le hb ha).1 h.symm.le), congr_arg _⟩
| Ordering.gt => hf.lt_iff_lt hb ha
