map_bddAbove — Mathlib

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

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