bddBelow_range — Mathlib

English

If α is directed under ≥, then the range of f: β → α is bounded below: there exists m with m ≤ a for all a in range f.

Русский

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

LaTeX

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

Lean4

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

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