instContinuousAddForallOfIsTopologicalSemiring

English

If each R_i is a topological semiring, then the addition in the product ∏_i R_i is continuous (pointwise).

Русский

Если каждый R_i — топологическое полукольцо, то сложение в произведении ∏_i R_i непрерывно (по координатам).

LaTeX

$$ContinuousAdd ( (i:ι) → R i )$$

Lean4

instance {ι : Type*} {R : ι → Type*} [∀ i, TopologicalSpace (R i)] [∀ i, NonUnitalNonAssocSemiring (R i)]
    [∀ i, IsTopologicalSemiring (R i)] : ContinuousAdd ((i : ι) → R i) :=
  inferInstance

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