maximal_of_minimal_image — Mathlib

English

If f is strictly antitone and f(a) is a lower bound of the image, then x ≤ a for all x.

Русский

Если f строго антимонотонна и f(a) является нижней границей образа, то для всех x выполняется x ≤ a.

LaTeX

$$$ (hf : StrictAnti f) \rightarrow (\forall p, p \le f(a)) \rightarrow \forall x, x \le a $$$

Lean4

theorem maximal_of_minimal_image (hf : StrictAnti f) {a} (hmin : ∀ p, f a ≤ p) (x : α) : x ≤ a :=
  hf.le_iff_ge.mp (hmin (f x))

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