bddBelow_range_of_cofinite — Mathlib

English

If α is directed by ≥ and u converges to a along the cofinite filter, then the range of u is bounded below.

Русский

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

LaTeX

$$$ [IsDirected\; α (\ge)]\; (h: Tendsto\, u\, cofinite\, (\mathcal{N}a)) \Rightarrow BddBelow (Set.range\, u). $$$

Lean4

theorem bddBelow_range_of_cofinite [IsDirected α (· ≥ ·)] (h : Tendsto u cofinite (𝓝 a)) : BddBelow (Set.range u) :=
  h.isBoundedUnder_ge.bddBelow_range_of_cofinite

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