instContinuousMulCoePrincipal — Mathlib

English

Continuity of bilinear map (multiplication) on restricted products reduces to continuity on the principal components.

Русский

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

LaTeX

$$$\\text{ContinuousMul}$ on restricted product via principal inclusions$$

Lean4

@[to_additive]
instance [Π i, Mul (R i)] [∀ i, MulMemClass (S i) (R i)] [∀ i, ContinuousMul (R i)] :
    ContinuousMul (Πʳ i, [R i, B i]_[𝓟 T]) :=
  let φ : Πʳ i, [R i, B i]_[𝓟 T] →ₙ* Π i, R i :=
    { toFun := (↑)
      map_mul' := fun _ _ ↦ rfl }
  isEmbedding_coe_of_principal.continuousMul φ

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