basisSets — Mathlib

English

There is a basis of neighborhoods of 0 generated by the family of seminorms, i.e., basisSets of seminormFamily.

Русский

Существуют базис окрестностей нуля, порождаемые семинормами из семейства seminormFamily.

LaTeX

$$theorem hasBasis_seminorms : (𝓝 (0 : E →WOT[𝕜] F)).HasBasis (seminormFamily 𝕜 E F).basisSets id$$

Lean4

/-- The sets of a filter basis for the neighborhood filter of 0. -/
def basisSets (p : SeminormFamily R E ι) : Set (Set E) :=
  ⋃ (s : Finset ι) (r) (_ : 0 < r), singleton (ball (s.sup p) (0 : E) r)

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