map_isLeast — Mathlib

English

An antitone map sends a least element of a set to a greatest element of its image.

Русский

Антитонное отображение переводит наименьший элемент множества в наибольший элемент его образа.

LaTeX

$$$\text{AntitoneOn}(f,t) \Rightarrow \text{IsLeast}(t,a) \Rightarrow \text{IsGreatest}(\mathrm{image}(f,t), f(a))$$$

Lean4

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

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