bddAbove_range — Mathlib

English

If α is directed under ≤, then the range of any function f: β → α is bounded above: there exists M with a ≤ M for all a in range f.

Русский

Пусть α ориентировано по ≤. Образ диапазона функции f: β → α имеет верхнюю границу: существует M такой, что a ≤ M для всех a ∈ range(f).

LaTeX

$$$\\\\exists M \\\\in \\\\alpha, \\\\forall a, a \\\\in \\\\operatorname{range}(f) \\\\Rightarrow a \\\\le M.$$$

Lean4

@[simp]
theorem bddAbove_range [IsDirected α (· ≤ ·)] (f : β → α) : BddAbove (Set.range f) :=
  by
  obtain ⟨M, hM⟩ := Finite.exists_le f
  refine ⟨M, fun a ha => ?_⟩
  obtain ⟨b, rfl⟩ := ha
  exact hM b

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