bddBelow_range — Mathlib

English

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

Русский

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

LaTeX

$$$\forall β [\text{Preorder } β] [\text{IsDirected } β (≥)] \ {f: \mathbb{N} o β},\ (\operatorname{IsBoundedUnder}(≥) \operatorname{atTop} f) \Rightarrow \operatorname{BddBelow}(\operatorname{range} f).$$$

Lean4

theorem bddBelow_range [Preorder β] [IsDirected β (· ≥ ·)] {f : ℕ → β} (hf : IsBoundedUnder (· ≥ ·) atTop f) :
    BddBelow (range f) :=
  IsBoundedUnder.bddAbove_range (β := βᵒᵈ) hf

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