instLieGroupOfNatWithTopENatOfIsTopologicalGroup

English

If G is a topological group, then for any Lie group I and any a=0, the structure LieGroup I 0 G exists.

Русский

Если G является топологической группой, то для любого I и a=0 существует структура LieGroup I 0 G.

LaTeX

$$[IsTopologicalGroup G] ⇒ [LieGroup I 0 G].$$

Lean4

@[to_additive]
instance [IsTopologicalGroup G] : LieGroup I 0 G := by
  constructor
  rw [contMDiff_zero_iff]
  exact continuous_inv

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