English
The image under an antitone function of a set which is bounded above is bounded below.
Русский
Образ антитонной функции множества, ограниченного сверху, ограничен снизу.
LaTeX
$$$(Hf : AntitoneOn f t) (Hst : s \subseteq t) : f''(\mathrm{upperBounds}(s) \cap t) \subseteq \mathrm{lowerBounds}(f''s)$$$
Lean4
/-- The image under an antitone function of a set which is bounded above is bounded below. -/
theorem map_bddAbove (Hf : AntitoneOn f t) (Hst : s ⊆ t) : (upperBounds s ∩ t).Nonempty → BddBelow (f '' s) :=
Hf.dual_right.map_bddAbove Hst