instIsTopologicalGroupCoePrincipal

English

Let (R_i) be topological groups and S_i ≤ R_i be subgroups for each i. Then the restricted product Π^r_i (R_i, S_i) with respect to the principal filter on a subset T is a topological group.

Русский

Пусть для каждого i дано топологическое группа R_i и подгруппа S_i ⊆ R_i. Тогда ограниченное произведение Π^r_i (R_i, S_i) относительно фильтра principal(T) является топологической группой.

LaTeX

$$$\\mathrm{IsTopologicalGroup}\\big(\\mathrm{RestrictedProduct}(\\{R_i\\}, \\{S_i\\}; \\mathrm{principal}(T))\\big)$$$

Lean4

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

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