instIsTopologicalSemiringProd — Mathlib

English

The product topology on the Cartesian product of two topological semirings makes the product a topological semiring.

Русский

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

LaTeX

$$IsTopologicalSemiring (R × S)$$

Lean4

/-- The product topology on the Cartesian product of two topological semirings
  makes the product into a topological semiring. -/
instance [NonUnitalNonAssocSemiring R] [NonUnitalNonAssocSemiring S] [IsTopologicalSemiring R]
    [IsTopologicalSemiring S] : IsTopologicalSemiring (R × S) where

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