image_Icc_of_antitoneOn — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem image_Icc_of_antitoneOn (hab : a ≤ b) (h : ContinuousOn f <| Icc a b) (h' : AntitoneOn f <| Icc a b) :
    f '' Icc a b = Icc (f b) (f a) :=
  by
  have : Icc (f b) (f a) = Icc (toDual (f a)) (toDual (f b)) := by rw [Icc_toDual]; rfl
  rw [this]
  exact image_Icc_of_monotoneOn (β := βᵒᵈ) hab h h'.dual_right

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