image_Icc — Mathlib

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)

Похожие утверждения