Theorems · Theorem · Lie groups

ContinuousAddEquiv.mk.inj

∀ {G : Type u} {inst : TopologicalSpace G} {H : Type v} {inst_1 : TopologicalSpace H} {inst_2 : Add G} {inst_3 : Add H}
  {toAddEquiv : G ≃+ H}
  {continuous_toFun : autoParam (Continuous toAddEquiv.toFun) Homeomorph.continuous_toFun._autoParam}
  {continuous_invFun : autoParam (Continuous toAddEquiv.invFun) Homeomorph.continuous_invFun._autoParam}
  {toAddEquiv_1 : G ≃+ H}
  {continuous_toFun_1 : autoParam (Continuous toAddEquiv_1.toFun) Homeomorph.continuous_toFun._autoParam}
  {continuous_invFun_1 : autoParam (Continuous toAddEquiv_1.invFun) Homeomorph.continuous_invFun._autoParam},
  { toAddEquiv := toAddEquiv, continuous_toFun := continuous_toFun, continuous_invFun := continuous_invFun } =
      { toAddEquiv := toAddEquiv_1, continuous_toFun := continuous_toFun_1, continuous_invFun := continuous_invFun_1 } →
    toAddEquiv = toAddEquiv_1

Defined in

Mathlib.Topology.Algebra.ContinuousMonoidHom

Cited by

1 results in Mathlib

Foundations

Depth 15 from the axioms · uses no axioms