image_uIcc_eq_Icc — Mathlib

English

If f is continuous on the closed interval uIcc[a,b], then f(uIcc[a,b]) is the closed interval between the infimum and supremum of the image.

Русский

Если f непрерывна на uIcc[a,b], то образ f(uIcc[a,b]) есть замкнутый интервал между sInf и sSup образа.

LaTeX

$$$f''\\mathrm{uIcc}(a,b) = \\mathrm{Icc}(sInf(f''\\mathrm{uIcc}(a,b)), sSup(f''\\mathrm{uIcc}(a,b)))$$$

Lean4

theorem image_uIcc_eq_Icc (h : ContinuousOn f [[a, b]]) :
    f '' [[a, b]] = Icc (sInf (f '' [[a, b]])) (sSup (f '' [[a, b]])) :=
  image_Icc min_le_max h

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