hasBasis — Mathlib

English

The topology of the space is equal to the topology induced by the moduleFilterBasis from p.

Русский

Топология пространства равна топологии, индуцированной moduleFilterBasis из p.

LaTeX

$$WithSeminorms p → t = p.moduleFilterBasis.topology$$

Lean4

theorem hasBasis (hp : WithSeminorms p) : (𝓝 (0 : E)).HasBasis (fun s : Set E => s ∈ p.basisSets) id :=
  by
  rw [congr_fun (congr_arg (@nhds E) hp.1) 0]
  exact AddGroupFilterBasis.nhds_zero_hasBasis _

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