Theorems · Definition · Lie groups

ContinuousAddEquiv.mk.noConfusion

{G : Type u} →
  {inst : TopologicalSpace G} →
    {H : Type v} →
      {inst_1 : TopologicalSpace H} →
        {inst_2 : Add G} →
          {inst_3 : Add H} →
            {P : Sort u_1} →
              {toAddEquiv : G ≃+ H} →
                {continuous_toFun : autoParam (Continuous toAddEquiv.toFun) Homeomorph.continuous_toFun._autoParam} →
                  {continuous_invFun :
                      autoParam (Continuous toAddEquiv.invFun) Homeomorph.continuous_invFun._autoParam} →
                    {toAddEquiv' : G ≃+ H} →
                      {continuous_toFun' :
                          autoParam (Continuous toAddEquiv'.toFun) Homeomorph.continuous_toFun._autoParam} →
                        {continuous_invFun' :
                            autoParam (Continuous toAddEquiv'.invFun) Homeomorph.continuous_invFun._autoParam} →
                          { toAddEquiv := toAddEquiv, continuous_toFun := continuous_toFun,
                                continuous_invFun := continuous_invFun } =
                              { toAddEquiv := toAddEquiv', continuous_toFun := continuous_toFun',
                                continuous_invFun := continuous_invFun' } →
                            (toAddEquiv ≍ toAddEquiv' → P) → P

Defined in

Mathlib.Topology.Algebra.ContinuousMonoidHom

Cited by

1 results in Mathlib

Foundations

Depth 14 from the axioms · uses no axioms