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