Theorems · Theorem · Lie groups

TopologicalGroup.IsSES.mulExact

∀ {A : Type u_1} {B : Type u_2} {C : Type u_3} [inst : Group A] [inst_1 : Group B] [inst_2 : Group C]
  [inst_3 : TopologicalSpace A] [inst_4 : TopologicalSpace B] [inst_5 : TopologicalSpace C] {φ : A →* B} {ψ : B →* C},
  TopologicalGroup.IsSES φ ψ → Function.MulExact ⇑φ ⇑ψ

Defined in

Mathlib.Topology.Algebra.Group.Extension

Cited by

2 results in Mathlib

Foundations

Depth 12 from the axioms · uses propext

Assumes

GroupGroupGroupTopologicalSpaceTopologicalSpaceTopologicalSpace