isLinearTopology_iff_hasBasis_open_ideal

English

If a ring R has continuous addition and is linearly topologized, a basis of neighborhoods of zero can be taken from open ideals.

Русский

Если сложение в кольце непрерывно, и кольцо линейно топологизировано, база окрестностей нуля может состоять из открытых идеалов.

LaTeX

$$$ [IsLinearTopology\\ R\\ R] \\Rightarrow (\\mathcal{N}0).HasBasis (fun I : Ideal R \\mapsto IsOpen(I:Set R)) (fun I => I:Set R) $$$

Lean4

theorem _root_.isLinearTopology_iff_hasBasis_open_ideal [IsTopologicalRing R] :
    IsLinearTopology R R ↔ (𝓝 0).HasBasis (fun I : Ideal R ↦ IsOpen (I : Set R)) (fun I : Ideal R ↦ (I : Set R)) :=
  isLinearTopology_iff_hasBasis_open_submodule

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