topologicalGroup — Mathlib

English

The space of functions from β to a family C(b) of groups, with the product topology, forms a topological group under pointwise multiplication.

Русский

Пространство функций β → C(b) с произведением топологий образует топологическую группу под поконой покомпонентной умножением.

LaTeX

$$$IsTopologicalGroup\left(\prod_{b\in \beta} C(b)\right)$$$

Lean4

@[to_additive]
instance topologicalGroup {C : β → Type*} [∀ b, TopologicalSpace (C b)] [∀ b, Group (C b)]
    [∀ b, IsTopologicalGroup (C b)] : IsTopologicalGroup (∀ b, C b) where
  continuous_inv := continuous_pi fun i => (continuous_apply i).inv

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