image_Icc_of_monotoneOn — Mathlib

English

If a ≤ b and f is continuous on Icc(a,b) and monotone on Icc(a,b), then f(Icc(a,b)) = Icc(f(a), f(b)).

Русский

Пусть a ≤ b, f непрерывна на Icc(a,b) и монотонна на Icc(a,b). Тогда образ Icc(a,b) при f равен Icc(f(a), f(b)).

LaTeX

$$$ f\left( Icc(a,b) \right) = Icc\left( f(a), f(b) \right). $$$

Lean4

theorem image_Icc_of_monotoneOn (hab : a ≤ b) (h : ContinuousOn f <| Icc a b) (h' : MonotoneOn f <| Icc a b) :
    f '' Icc a b = Icc (f a) (f b) := by
  rw [h.image_Icc hab]
  congr!
  · exact h'.sInf_image_Icc hab
  · exact h'.sSup_image_Icc hab

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