minimal_of_minimal_image — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem minimal_of_minimal_image (hf : StrictMono f) {a} (hmin : ∀ p, f a ≤ p) (x : α) : a ≤ x :=
  hf.le_iff_le.mp (hmin (f x))

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