bddAbove_range_of_cofinite — Mathlib

English

If f tends to a along the cofinite filter, then the range of f is bounded above.

Русский

Если f стремится к a вдоль фильтра cofinite, тогда множество значений f ограничено сверху.

LaTeX

$$$$ (\text{IsDirected } α) \Rightarrow (Tendsto\, u\, cofinite\, (nhds\, a)) \Rightarrow BddAbove(\text{range } u). $$$$

Lean4

theorem bddAbove_range_of_cofinite [IsDirected α (· ≤ ·)] (h : Tendsto u cofinite (𝓝 a)) : BddAbove (Set.range u) :=
  h.isBoundedUnder_le.bddAbove_range_of_cofinite

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