hasBasis_submodule — Mathlib

English

A neighborhood basis for 0 in a linear topology can be taken as submodules of the underlying module.

Русский

Базис окрестностей нуля в линейной топологии можно взять состоящим из подмодулей.

LaTeX

$$$\\text{nhds}(0)\\text{ HasBasis } (N\\mapsto N\\text{ подмодуль})$$$

Lean4

theorem hasBasis_submodule [IsLinearTopology R M] :
    (𝓝 (0 : M)).HasBasis (fun N : Submodule R M ↦ (N : Set M) ∈ 𝓝 0) (fun N : Submodule R M ↦ (N : Set M)) :=
  IsLinearTopology.hasBasis_submodule'

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