isLinearTopology_iff_hasBasis_open_twoSidedIdeal

English

The joint linear-topology characterization can be described by a basis of open two-sided ideals.

Русский

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

LaTeX

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

Lean4

theorem _root_.isLinearTopology_iff_hasBasis_open_twoSidedIdeal [ContinuousAdd R] :
    IsLinearTopology R R ∧ IsLinearTopology Rᵐᵒᵖ R ↔
      (𝓝 0).HasBasis (fun I : TwoSidedIdeal R ↦ IsOpen (I : Set R)) (fun I : TwoSidedIdeal R ↦ (I : Set R)) :=
  ⟨fun ⟨_, _⟩ ↦ hasBasis_open_twoSidedIdeal, fun h ↦
    ⟨.mk_of_hasBasis' R h fun I r x hx ↦ I.mul_mem_left r x hx,
      .mk_of_hasBasis' Rᵐᵒᵖ h fun I r x hx ↦ I.mul_mem_right x r.unop hx⟩⟩

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