hasBasis_open_submodule — Mathlib

English

To show M is linearly topologized over R, it suffices to exhibit a basis of neighborhoods generated by R-submodules.

Русский

Чтобы показать, что M является линейно топологизированной над R, достаточно привести базис окрестностей, порождаемый R-подмодулями.

LaTeX

$$$IsLinearTopology R M$ iff $(\\mathcal N_0) HasBasis (submodules)$$$

Lean4

theorem hasBasis_open_submodule [ContinuousAdd M] [IsLinearTopology R M] :
    (𝓝 (0 : M)).HasBasis (fun N : Submodule R M ↦ IsOpen (N : Set M)) (fun N : Submodule R M ↦ (N : Set M)) :=
  hasBasis_submodule R |>.congr (fun N ↦ ⟨N.toAddSubgroup.isOpen_of_mem_nhds, fun hN ↦ hN.mem_nhds (zero_mem N)⟩)
    (fun _ _ ↦ rfl)

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