isLinearTopology_iff_hasBasis_submodule

English

IsLinearTopology is equivalent to having a basis of neighborhoods of 0 formed by submodules.

Русский

IsLinearTopology эквивалентно существованию базиса окрестностей нуля из подмодулей.

LaTeX

$$$\\text{IsLinearTopology } R M \\iff (\\mathcal N 0).HasBasis (N \\mapsto N) (N \\mapsto N)$$$

Lean4

theorem _root_.isLinearTopology_iff_hasBasis_submodule :
    IsLinearTopology R M ↔
      (𝓝 0).HasBasis (fun N : Submodule R M ↦ (N : Set M) ∈ 𝓝 0) (fun N : Submodule R M ↦ (N : Set M)) :=
  ⟨fun _ ↦ hasBasis_submodule R, fun h ↦ .mk_of_hasBasis R h⟩

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