map_isGreatest — 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

/-- An antitone map sends a greatest element of a set to a least element of its image. -/
theorem map_isGreatest (Hf : AntitoneOn f t) : IsGreatest t a → IsLeast (f '' t) (f a) :=
  Hf.dual_right.map_isGreatest

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