isTopologicalGroup — Mathlib

English

If each R_i is a locally compact group, every B_i is a subgroup, and all are compatible with the topology, then the restricted product with principal filter on T is locally compact.

Русский

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

LaTeX

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

Lean4

@[to_additive]
instance isTopologicalGroup [Π i, Group (R i)] [∀ i, SubgroupClass (S i) (R i)] [∀ i, IsTopologicalGroup (R i)] :
    IsTopologicalGroup (Πʳ i, [R i, B i]) where

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