bddAbove_range — Mathlib

English

Let β be a preorder directed by ≤. If a function f: ℕ → β is bounded above along atTop, then the range of f is bounded above.

Русский

Пусть β упорядочено направлено по ≤. Если функция f: ℕ → β ограничена сверху вдоль atTop, то диапазон значений range f ограничен сверху.

LaTeX

$$$\forall \beta [\text{Preorder } \beta] [\text{IsDirected } \beta (\le)]\ {f: \mathbb{N} \to \beta},\ (\operatorname{IsBoundedUnder}(\le)\ \operatorname{atTop} f) \Rightarrow \operatorname{BddAbove}(\operatorname{range} f).$$$

Lean4

theorem bddAbove_range [Preorder β] [IsDirected β (· ≤ ·)] {f : ℕ → β} (hf : IsBoundedUnder (· ≤ ·) atTop f) :
    BddAbove (range f) := by
  rw [← Nat.cofinite_eq_atTop] at hf
  exact hf.bddAbove_range_of_cofinite

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