topologicalGroup — Mathlib

English

If f is an inducing map that is a monoid homomorphism, then the target H inherits a topological group structure from the domain via f.

Русский

Если отображение f является вводящим (inducing) и является гомоморфизмом моидов, то цель H наследует топологическую группу через f.

LaTeX

$$$IsInducing\ f\;\Rightarrow\; IsTopologicalGroup(H)$$$

Lean4

@[to_additive]
protected theorem topologicalGroup {F : Type*} [Group H] [TopologicalSpace H] [FunLike F H G] [MonoidHomClass F H G]
    (f : F) (hf : IsInducing f) : IsTopologicalGroup H :=
  { toContinuousMul := hf.continuousMul _
    toContinuousInv := hf.continuousInv (map_inv f) }

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