continuousSMul — Mathlib

English

If each R_i carries a multiplication and the subobjects B_i are closed under multiplication with compatible topology, then the restricted product has continuous multiplication.

Русский

Если в каждом R_i задано умножение, а подобъекты B_i замкнуты по умножению и соблюдают топологию, то ограниченное произведение имеет непрерывное умножение.

LaTeX

$$$\\mathrm{ContinuousMul}\\left(\\mathrm{RestrictedProduct}(\\{R_i\\}, \\{B_i\\}; \\mathrm{cofinite})\\right)$$$

Lean4

@[to_additive]
instance continuousSMul {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]) where
  continuous_smul := by
    rw [continuous_dom_prod_left hBopen.out]
    exact fun S hS ↦ (continuous_inclusion hS).comp continuous_smul

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