isLinearTopology_iff_hasBasis_open_submodule

English

If there is a linear topology, neighborhoods of 0 can be taken as open submodules.

Русский

Для линейной топологии окрестности нуля можно выбрать как открытые подмодули.

LaTeX

$$$(\\text{nhds }0).HasBasis (N \\mapsto IsOpen (N)) (N \\mapsto N)$$$

Lean4

theorem _root_.isLinearTopology_iff_hasBasis_open_submodule [ContinuousAdd M] :
    IsLinearTopology R M ↔
      (𝓝 0).HasBasis (fun N : Submodule R M ↦ IsOpen (N : Set M)) (fun N : Submodule R M ↦ (N : Set M)) :=
  ⟨fun _ ↦ hasBasis_open_submodule R, fun h ↦ .mk_of_hasBasis R h⟩

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