Theorems · Theorem · Lie groups

Topology.IsInducing.topologicalGroup

∀ {G : Type w} {H : Type x} [inst : TopologicalSpace G] [inst_1 : Group G] [IsTopologicalGroup G] {F : Type u_1}
  [inst_3 : Group H] [inst_4 : TopologicalSpace H] [inst_5 : FunLike F H G] [MonoidHomClass F H G] (f : F),
  Topology.IsInducing ⇑f → IsTopologicalGroup H

Defined in

Mathlib.Topology.Algebra.Group.Basic

Cited by

1 results in Mathlib

Foundations

Depth 78 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

TopologicalSpaceGroupIsTopologicalGroupGroupTopologicalSpaceFunLikeMonoidHomClass