minimal_of_maximal_image — Mathlib

English

If f is strictly antitone and f(a) is maximal in the image, then a ≤ x for all x.

Русский

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

LaTeX

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

Lean4

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

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