hasBasis_open_twoSidedIdeal — Mathlib

English

If both linear topologies exist, the zero-neighborhood basis can be taken from open two-sided ideals.

Русский

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

LaTeX

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

Lean4

theorem hasBasis_open_twoSidedIdeal [ContinuousAdd R] [IsLinearTopology R R] [IsLinearTopology Rᵐᵒᵖ R] :
    (𝓝 (0 : R)).HasBasis (fun I : TwoSidedIdeal R ↦ IsOpen (I : Set R)) (fun I : TwoSidedIdeal R ↦ (I : Set R)) :=
  hasBasis_twoSidedIdeal.congr (fun I ↦ ⟨I.asIdeal.toAddSubgroup.isOpen_of_mem_nhds, fun hI ↦ hI.mem_nhds (zero_mem I)⟩)
    (fun _ _ ↦ rfl)

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