instContinuousAdd — Mathlib

English

If R and M are additive topological spaces with continuous addition, then the additive structure on the trivial square-zero extension tsze R M is continuous.

Русский

Если R и M являются топологическими пространствами с операцией сложения, непрерывной по обеим компонентам, то сложение в тривиальном квадрат-ноль расширении tsze R M непрерывно.

LaTeX

$$$\\operatorname{ContinuousAdd}(\\mathrm{tsze}(R,M))$$$

Lean4

instance [Add R] [Add M] [ContinuousAdd R] [ContinuousAdd M] : ContinuousAdd (tsze R M) :=
  Prod.continuousAdd

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