isLinearTopology_iff_hasBasis_twoSidedIdeal

English

The linear topologies on R and on Rᵐᵒᵖ R are characterized by a basis of neighborhoods of zero formed by two-sided ideals.

Русский

Линейные топологии на R и на Rᵐᵒᵖ R задаются базой окрестностей нуля, сформированной двусторонними идеалами.

LaTeX

$$$ IsLinearTopology R R \\wedge IsLinearTopology R^{op} R \\iff (\\mathcal{N}0).HasBasis (fun I : TwoSidedIdeal R \\mapsto (I:Set R) \\in 𝓝 0) (fun I => I:Set R) $$$

Lean4

theorem _root_.isLinearTopology_iff_hasBasis_twoSidedIdeal :
    IsLinearTopology R R ∧ IsLinearTopology Rᵐᵒᵖ R ↔
      (𝓝 0).HasBasis (fun I : TwoSidedIdeal R ↦ (I : Set R) ∈ 𝓝 0) (fun I : TwoSidedIdeal R ↦ (I : Set R)) :=
  ⟨fun ⟨_, _⟩ ↦ hasBasis_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⟩⟩

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