English
If the subgroups form compact subtypes and all hypotheses for a locally compact group hold, then the restricted product is locally compact.
Русский
Если подмножества образуют компактные подтипы и выполняются гипотезы для локально компактной группы, то ограниченное произведение локально компактно.
LaTeX
$$$\\mathrm{LocallyCompactSpace}\\left(\\mathrm{RestrictedProduct}(\\{R_i\\}, \\{B_i\\}; \\mathrm{cofinite})\\right)$$$
Lean4
/-- Assume that each `R i` is a locally compact group with `A i` an open subgroup.
Assume also that all but finitely many `A i`s are compact.
Then the restricted product `Πʳ i, [R i, A i]` is a locally compact group. -/
@[to_additive /-- Assume that each `R i` is a locally compact additive group with `A i` an open subgroup.
Assume also that all but finitely many `A i`s are compact.
Then the restricted product `Πʳ i, [R i, A i]` is a locally compact additive group. -/
]
theorem locallyCompactSpace_of_group [Π i, Group (R i)] [∀ i, SubgroupClass (S i) (R i)] [∀ i, IsTopologicalGroup (R i)]
[∀ i, LocallyCompactSpace (R i)] (hBcompact : ∀ᶠ i in cofinite, IsCompact (B i : Set (R i))) :
LocallyCompactSpace (Πʳ i, [R i, B i]) :=
haveI : WeaklyLocallyCompactSpace (Πʳ i, [R i, B i]) := weaklyLocallyCompactSpace_of_cofinite hBopen.out hBcompact
inferInstance
