instIsLinearTopologyMulOpposite — Mathlib

English

If R has a linear topology, then the opposite topology on MvPowerSeries(σ,R) gives a right linear topology, i.e., IsLinearTopology((MvPowerSeries(σ,R))ᵐᵒᵖ, MvPowerSeries(σ,R)).

Русский

Если R обладает линейной топологией, то правая линейная топология на произведении MvPowerSeries(σ,R) имеется в виде IsLinearTopology((MvPowerSeries(σ,R))ᵐᵒᵖ, MvPowerSeries(σ,R)).

LaTeX

$$$\operatorname{IsLinearTopology}\bigl( (\mathrm{MvPowerSeries}(\sigma,R))^{\mathrm{op}},\ \mathrm{MvPowerSeries}(\sigma,R) \bigr).$$$

Lean4

/-- The topology on `MvPowerSeries` is a right linear topology
  when the ring of coefficients has a linear topology. -/
instance [IsLinearTopology R R] [IsLinearTopology Rᵐᵒᵖ R] :
    IsLinearTopology (MvPowerSeries σ R)ᵐᵒᵖ (MvPowerSeries σ R) :=
  IsLinearTopology.mk_of_hasBasis' _ hasBasis_nhds_zero (fun J _ _ hg ↦ J.mul_mem_right _ _ hg)

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