isVonNBounded_range — Mathlib

English

If a sequence f(n) tends to x in E, then its range is von Neumann bounded.

Русский

Если последовательность f(n) стремится к x в E, тогда множество значений {f(n)} ограничено по фон Нейману.

LaTeX

$$$\\operatorname{Tendsto}(f,\\, atTop,\\, \\mathcal{N}(x)) \\Rightarrow \\operatorname{IsVonNBounded}_{\\mathbb{k}}(\\operatorname{range}(f))$$$

Lean4

theorem isVonNBounded_range [NormedField 𝕜] [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] [IsTopologicalAddGroup E]
    [ContinuousSMul 𝕜 E] {f : ℕ → E} {x : E} (hf : Tendsto f atTop (𝓝 x)) : Bornology.IsVonNBounded 𝕜 (range f) :=
  letI := IsTopologicalAddGroup.toUniformSpace E
  haveI := isUniformAddGroup_of_addCommGroup (G := E)
  hf.cauchySeq.totallyBounded_range.isVonNBounded 𝕜

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