isBounded_range_of_tendsto_cofinite

English

Let α be a metric space and f: β → α. If f converges to a point a along the cofinite filter, then the set {f(b) : b ∈ β} is bounded.

Русский

Пусть α — метрическое пространство и f: β → α. Если f сходится к точке a вдоль кофинитного фильтра, то образ {f(b) : b ∈ β} ограничен.

LaTeX

$$$\\forall f:\\\\beta \\to \\alpha, \\forall a:\\\\alpha, \\\\ Tendsto\, f\, cofinite\, (\\\\nhds a) \\Rightarrow \\\\ IsBounded(\\\\range f). $$$

Lean4

theorem isBounded_range_of_tendsto_cofinite {f : β → α} {a : α} (hf : Tendsto f cofinite (𝓝 a)) : IsBounded (range f) :=
  isBounded_range_of_tendsto_cofinite_uniformity <|
    (hf.prodMap hf).mono_right <| nhds_prod_eq.symm.trans_le (nhds_le_uniformity a)

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