English
Let f be a function between linearly ordered sets. The function is monotone or antitone if and only if for all a,b,c, whenever c lies in the unordered interval between a and b, then f(c) lies in the unordered interval between f(a) and f(b).
Русский
Пусть f — функция между линейно упорядоченными множествами. Она монотонна или антитонирована тогда и только тогда, когда для любых a,b,c с c в неупорядоченном интервале между a и b выполняется f(c) в неупорядоченном интервале между f(a) и f(b).
LaTeX
$$$ (\\mathrm{Monotone}\\ f \\lor \\mathrm{Antitone}\\ f) \\iff \\forall a,b,c,\\ c \\in [[a,b]] \\implies f(c) \\in [[f(a),f(b)]] $$$
Lean4
theorem monotone_or_antitone_iff_uIcc : Monotone f ∨ Antitone f ↔ ∀ a b c, c ∈ [[a, b]] → f c ∈ [[f a, f b]] :=
by
constructor
· rintro (hf | hf) a b c <;> simp_rw [← Icc_min_max, ← hf.map_min, ← hf.map_max]
exacts [fun hc => ⟨hf hc.1, hf hc.2⟩, fun hc => ⟨hf hc.2, hf hc.1⟩]
contrapose!
rw [not_monotone_not_antitone_iff_exists_le_le]
rintro ⟨a, b, c, hab, hbc, ⟨hfab, hfcb⟩ | ⟨hfba, hfbc⟩⟩
· exact ⟨a, c, b, Icc_subset_uIcc ⟨hab, hbc⟩, fun h => h.2.not_gt <| max_lt hfab hfcb⟩
· exact ⟨a, c, b, Icc_subset_uIcc ⟨hab, hbc⟩, fun h => h.1.not_gt <| lt_min hfba hfbc⟩
