hasBasis_open_ideal — Mathlib

English

If there is a continuous addition and R-linear topology on R, then the neighborhoods basis at 0 can be taken to consist of open ideals.

Русский

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

LaTeX

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

Lean4

theorem hasBasis_open_ideal [ContinuousAdd R] [IsLinearTopology R R] :
    (𝓝 0).HasBasis (fun I : Ideal R ↦ IsOpen (I : Set R)) (fun I : Ideal R ↦ (I : Set R)) :=
  hasBasis_open_submodule R

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