instContinuousMulCoeCofinite — Mathlib

English

If each R_i is locally compact and all but finitely many B_i are compact, the restricted product of R_i with respect to B_i is locally compact.

Русский

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

LaTeX

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

Lean4

@[to_additive]
instance [Π i, Mul (R i)] [∀ i, MulMemClass (S i) (R i)] [∀ i, ContinuousMul (R i)] : ContinuousMul (Πʳ i, [R i, B i])
    where
  continuous_mul := by
    rw [continuous_dom_prod hBopen.out hBopen.out]
    exact fun S hS ↦ (continuous_inclusion hS).comp continuous_mul

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