instContinuousSMulForall — Mathlib

English

If each γ_i has a continuous SMul by M, then the action of M on the product ∀ i, γ_i is continuous.

Русский

Если для каждого i топологическое пространство γ_i допускает непрерывное действие M, то на произведении ∀ i, γ_i действие непрерывно.

LaTeX

$$ContinuousSMul M (∀ i, γ_i)$$

Lean4

@[to_additive]
instance {ι : Type*} {γ : ι → Type*} [∀ i, TopologicalSpace (γ i)] [∀ i, SMul M (γ i)] [∀ i, ContinuousSMul M (γ i)] :
    ContinuousSMul M (∀ i, γ i) :=
  ⟨continuous_pi fun i =>
      (continuous_fst.smul continuous_snd).comp <| continuous_fst.prodMk ((continuous_apply i).comp continuous_snd)⟩

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