map_bddBelow — 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) : (\mathrm{upperBounds}(s) \cap t).Nonempty \Rightarrow \mathrm{BddBelow}(\mathrm{image}(f,s))$$$

Lean4

/-- The image under an antitone function of a set which is bounded below is bounded above. -/
theorem map_bddBelow (Hf : AntitoneOn f t) (Hst : s ⊆ t) : (lowerBounds s ∩ t).Nonempty → BddAbove (f '' s) :=
  Hf.dual_right.map_bddBelow Hst

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