instContinuousStarForall — Mathlib

English

If each C i has ContinuousStar and Star, then the function space ∀ i, C i has ContinuousStar.

Русский

Если каждый C i имеет ContinuousStar и Star, то пространство функций ∀ i, C i имеет ContinuousStar.

LaTeX

$$$\mathrm{ContinuousStar}\bigl((i:\!\iota) \to C(i)\bigr)$$$

Lean4

instance {C : ι → Type*} [∀ i, TopologicalSpace (C i)] [∀ i, Star (C i)] [∀ i, ContinuousStar (C i)] :
    ContinuousStar (∀ i, C i) where continuous_star := continuous_pi fun i => Continuous.star (continuous_apply i)

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