isVonNBounded_iff_tendsto_smallSets_nhds

English

For a normed division ring 𝕜, a set S is von Neumann bounded iff the scalar action by 𝕜 tends to 0 on small sets near 0.

Русский

Для нормированного делимого кольца 𝕜 множество S VN‑ограничено ⇔ отображение умножения на 𝕜 у малых множеств стремится к 0.

LaTeX

$$IsVonNBounded 𝕜 S ↔ Tendsto (· • S) (nhds 0) (nhds 0).smallSets$$

Lean4

theorem isVonNBounded_iff_tendsto_smallSets_nhds {𝕜 E : Type*} [NormedDivisionRing 𝕜] [AddCommGroup E] [Module 𝕜 E]
    [TopologicalSpace E] {S : Set E} : IsVonNBounded 𝕜 S ↔ Tendsto (· • S : 𝕜 → Set E) (𝓝 0) (𝓝 0).smallSets :=
  by
  rw [tendsto_smallSets_iff]
  refine forall₂_congr fun V hV ↦ ?_
  simp only [absorbs_iff_eventually_nhds_zero (mem_of_mem_nhds hV), mapsTo_iff_image_subset, image_smul]

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