maximal_of_maximal_image — Mathlib

English

If f is strictly increasing and f(a) is an upper bound of the image, then every x satisfies x ≤ a.

Русский

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

LaTeX

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

Lean4

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

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