Theorems · Theorem · Lie groups

Topology.IsInducing.topologicalAddGroup

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

Defined in

Mathlib.Topology.Algebra.Group.Basic

Cited by

2 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceAddGroupIsTopologicalAddGroupAddGroupTopologicalSpaceFunLikeAddMonoidHomClass