instContinuousSMulCoePrincipal — Mathlib

English

An invariant instance: continuous scalar multiplication on the principal restricted product over S is defined coordinatewise.

Русский

Инвариантный экземпляр: непрерывное действие умножения по координатам на принципиальном ограниченном произведении.

LaTeX

$$$\\text{ContinuousSMul}$ for principal restricted product$$

Lean4

@[to_additive]
instance {G : Type*} [TopologicalSpace G] [Π i, SMul G (R i)] [∀ i, SMulMemClass (S i) G (R i)]
    [∀ i, ContinuousSMul G (R i)] : ContinuousSMul G (Πʳ i, [R i, B i]_[𝓟 T]) :=
  isEmbedding_coe_of_principal.continuousSMul continuous_id rfl

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