English
If f is continuous on Icc[a,b], then f(Icc[a,b]) equals the closed interval between the infimum and supremum of the image.
Русский
Если f непрерывна на Icc[a,b], то образ f(Icc[a,b]) равен замкнутому интервалу между sInf и sSup образа.
LaTeX
$$$f''\\mathrm{Icc}(a,b) = \\mathrm{Icc}(sInf(f''\\mathrm{Icc}(a,b)), sSup(f''\\mathrm{Icc}(a,b)))$$$
Lean4
theorem image_Icc (hab : a ≤ b) (h : ContinuousOn f <| Icc a b) :
f '' Icc a b = Icc (sInf <| f '' Icc a b) (sSup <| f '' Icc a b) :=
eq_Icc_of_connected_compact ⟨(nonempty_Icc.2 hab).image f, isPreconnected_Icc.image f h⟩
(isCompact_Icc.image_of_continuousOn h)