English
If f is monotone on the closed interval Icc[a,b], the supremum of the image f''Icc[a,b] is f(b).
Русский
Пусть f монотонна на Icc[a,b]. Тогда sup{ f(x) : x ∈ Icc[a,b] } = f(b).
LaTeX
$$$[Preorder\ \alpha][ConditionallyCompleteLattice\ \beta]\ {f:\alpha\to\beta}\ {a,b:\alpha}\ (hab: a \le b) (h': MonotoneOn f (Icc a b)) : sSup (f '' Icc a b) = f b$$$
Lean4
theorem sSup_image_Icc [Preorder α] [ConditionallyCompleteLattice β] {f : α → β} {a b : α} (hab : a ≤ b)
(h' : MonotoneOn f (Icc a b)) : sSup (f '' Icc a b) = f b :=
by
have : Icc a b = Icc (α := αᵒᵈ) (toDual b) (toDual a) := by rw [Icc_toDual]; rfl
rw [this] at h' ⊢
exact h'.dual_right.dual_left.sInf_image_Icc (β := βᵒᵈ) (α := αᵒᵈ) hab