hasBasis_ideal — Mathlib

English

For a ring R with a linear topology, the neighborhoods of 0 have a basis indexed by ideals of R.

Русский

Для кольца R с линейной топологией окрестности нуля имеют базу, индексированную идеалами R.

LaTeX

$$$ IsLinearTopology R R \\iff (\\mathcal{N}0) \\text{ has basis by ideals: } (I:Set R) \\text{ with } I \\in (\\mathcal{N}0). $$$

Lean4

theorem hasBasis_ideal [IsLinearTopology R R] :
    (𝓝 0).HasBasis (fun I : Ideal R ↦ (I : Set R) ∈ 𝓝 0) (fun I : Ideal R ↦ (I : Set R)) :=
  hasBasis_submodule R

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