instContinuousStarProd — Mathlib

English

If R and S have ContinuousStar, then their product R×S has a ContinuousStar.

Русский

Если на пространствах R и S есть ContinuousStar, то в произведении R×S имеется ContinuousStar.

LaTeX

$$$\mathrm{ContinuousStar}(R\times S)$$$

Lean4

instance [Star R] [Star S] [TopologicalSpace R] [TopologicalSpace S] [ContinuousStar R] [ContinuousStar S] :
    ContinuousStar (R × S) :=
  ⟨(continuous_star.comp continuous_fst).prodMk (continuous_star.comp continuous_snd)⟩

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