topologicalSemiring_of_contMDiffRing

English

Under the ContMDiffRing structure, R inherits a topological semiring structure.

Русский

При структуре ContMDiffRing R наследует топологическую полукольцо.

LaTeX

$$$\\text{IsTopologicalSemiring}(R)$ under ContMDiffRing I n R$$

Lean4

/-- A `C^n` (semi)ring is a topological (semi)ring. This is not an instance for technical reasons,
see note [Design choices about smooth algebraic structures]. -/
theorem topologicalSemiring_of_contMDiffRing [Semiring R] [ContMDiffRing I n R] : IsTopologicalSemiring R :=
  { continuousMul_of_contMDiffMul I n, continuousAdd_of_contMDiffAdd I n with }

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