English
If f is continuous on the closed interval Icc(a,b) in a densely ordered space, then f(Icc(a,b)) equals the closed interval between the infimum and supremum of the image, with appropriate endpoints.
Русский
Если f непрерывна на замкнутом интервале Icc(a,b) в плотно упорядоченном пространстве, то образ Icc(a,b) равен замкнутому интервалу между sInf и sSup образа.
LaTeX
$$$\\mathrm{image}(f, \\mathrm{Icc}(a,b)) = \\mathrm{Icc}(sInf(f(\\mathrm{Icc}(a,b))), sSup(f(\\mathrm{Icc}(a,b))))$$$
Lean4
theorem image_uIcc (h : ContinuousOn f <| [[a, b]]) : f '' [[a, b]] = [[sInf (f '' [[a, b]]), sSup (f '' [[a, b]])]] :=
by
refine h.image_uIcc_eq_Icc.trans (uIcc_of_le ?_).symm
refine csInf_le_csSup ?_ ?_ (nonempty_uIcc.image _) <;> rw [h.image_uIcc_eq_Icc]
exacts [bddBelow_Icc, bddAbove_Icc]
