map_bddAbove — Mathlib

English

If a set is bounded above, then its image under an antitone map is bounded below.

Русский

Если множество ограничено сверху, то его образ под антитонной отображающей функцией ограничен снизу.

LaTeX

$$$ BddAbove(s) \rightarrow BddBelow(f''(s)) $$$

Lean4

/-- The image under an antitone function of a set which is bounded above is bounded below. -/
theorem map_bddAbove : BddAbove s → BddBelow (f '' s) :=
  hf.dual_right.map_bddAbove

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