instContinuousConstSMulCoe — Mathlib

English

Continuous scalar multiplication on the restricted product is induced from the principal coe via the embedding.

Русский

Непрерывное умножение на ограниченное произведение задаётся через коe на подпространстве и вложение.

LaTeX

$$$\\text{ContinuousSMul}(\\text{structure}, 𝓕)$$$

Lean4

@[to_additive]
instance {G : Type*} [Π i, SMul G (R i)] [∀ i, SMulMemClass (S i) G (R i)] [∀ i, ContinuousConstSMul G (R i)] :
    ContinuousConstSMul G (Πʳ i, [R i, B i]_[𝓕]) where
  continuous_const_smul
    g := by
    rw [continuous_dom]
    intro T hT
    haveI : ContinuousConstSMul G (Πʳ i, [R i, B i]_[𝓟 T]) := isEmbedding_coe_of_principal.continuousConstSMul id rfl
    exact (continuous_inclusion hT).comp (continuous_const_smul g)

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