hasBasis_ball — Mathlib

English

If p is a WithSeminorms, then nhds balls around any point x can be described as unions of seminorm balls (basis).

Русский

Если p — WithSeminorms, окрестности точки x описываются как объединения шаров семинорм (база).

LaTeX

$$WithSeminorms p → (nhds x).HasBasis (fun s => Set.instMembership mem p.basisSets s) id$$

Lean4

theorem hasBasis_ball (hp : WithSeminorms p) {x : E} :
    (𝓝 (x : E)).HasBasis (fun sr : Finset ι × ℝ => 0 < sr.2) fun sr => (sr.1.sup p).ball x sr.2 :=
  by
  have : IsTopologicalAddGroup E := hp.topologicalAddGroup
  rw [← map_add_left_nhds_zero]
  convert hp.hasBasis_zero_ball.map (x + ·) using 1
  ext sr : 1
    -- Porting note: extra type ascriptions needed on `0`

  have : (sr.fst.sup p).ball (x +ᵥ (0 : E)) sr.snd = x +ᵥ (sr.fst.sup p).ball 0 sr.snd :=
    Eq.symm (Seminorm.vadd_ball (sr.fst.sup p))
  rwa [vadd_eq_add, add_zero] at this

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