ball_mem_nhds — Mathlib

English

There is a basis of neighborhoods around 0 in the uniformity compatible with the seminorm p.

Русский

Существует базис окрестностей точки 0 в униформной структуре, совместимый с семинормой p.

LaTeX

$$$ (\\mathcal{N}_0) \\text{ has a basis given by shells } p(B) \\Rightarrow \\ text{UniformSpace equality.} $$$

Lean4

theorem ball_mem_nhds [TopologicalSpace E] {p : Seminorm 𝕝 E} (hp : Continuous p) {r : ℝ} (hr : 0 < r) :
    p.ball 0 r ∈ (𝓝 0 : Filter E) :=
  have this : Tendsto p (𝓝 0) (𝓝 0) := map_zero p ▸ hp.tendsto 0
  by simpa only [p.ball_zero_eq] using this (Iio_mem_nhds hr)

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