bddBelow_range_of_cofinite — Mathlib

English

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

Русский

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

LaTeX

$$$\forall {\alpha \beta} [\text{Preorder } \beta] [\text{IsDirected } \beta (\ge)] \ {f: \alpha \to \beta},\ (\operatorname{IsBoundedUnder}(\ge)\ \text{cofinite } f) \Rightarrow \operatorname{BddBelow}(\operatorname{range} f).$$$

Lean4

theorem bddBelow_range_of_cofinite [Preorder β] [IsDirected β (· ≥ ·)] {f : α → β}
    (hf : IsBoundedUnder (· ≥ ·) cofinite f) : BddBelow (range f) :=
  IsBoundedUnder.bddAbove_range_of_cofinite (β := βᵒᵈ) hf

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