isLinearTopology_iff_hasBasis_ideal

English

For a ring R, IsLinearTopology R R is equivalent to the neighborhood basis at 0 being indexed by ideals of R.

Русский

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

LaTeX

$$$ IsLinearTopology\\ R\\ R \\iff (\\mathcal{N}0).HasBasis (fun I : Ideal R \\mapsto (I:Set R) \\in 𝓝 0) (fun I : Ideal R \\mapsto (I:Set R)) $$$

Lean4

theorem _root_.isLinearTopology_iff_hasBasis_ideal :
    IsLinearTopology R R ↔ (𝓝 0).HasBasis (fun I : Ideal R ↦ (I : Set R) ∈ 𝓝 0) (fun I : Ideal R ↦ (I : Set R)) :=
  isLinearTopology_iff_hasBasis_submodule

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