English
On a set s, a function is strictly monotone if and only if it preserves order on s; equivalently, a ≤ b in the domain implies f(a) ≤ f(b) and vice versa.
Русский
На ограниченном множестве s функция строго монотонна тогда и только тогда, когда она сохраняет порядок на s; равносильно, а ≤ b в области определения эквивалентно f(a) ≤ f(b).
LaTeX
$$$[LinearOrder \\alpha]\\; [Preorder \\beta] \\; {f : \\alpha \\to \\beta} \\; {s : Set \\alpha} \\; (hf : StrictMonoOn f s) \\; \\forall {a b}, a ∈ s \\,\\to \\, b ∈ s \\,\\to\\; f a ≤ f b \leftrightarrow a ≤ b$$$
Lean4
theorem le_iff_le (hf : StrictMonoOn f s) {a b : α} (ha : a ∈ s) (hb : b ∈ s) : f a ≤ f b ↔ a ≤ b :=
⟨fun h ↦ le_of_not_gt fun h' ↦ (hf hb ha h').not_ge h, fun h ↦
h.lt_or_eq_dec.elim (fun h' ↦ (hf ha hb h').le) fun h' ↦ h' ▸ le_rfl⟩
