Theorems · Definition · geometry

ContinuousAffineMap.noConfusion

{P : Sort u} →
  {R : Type u_1} →
    {V : Type u_2} →
      {W : Type u_3} →
        {P_1 : Type u_4} →
          {Q : Type u_5} →
            {inst : Ring R} →
              {inst_1 : AddCommGroup V} →
                {inst_2 : Module R V} →
                  {inst_3 : TopologicalSpace P_1} →
                    {inst_4 : AddTorsor V P_1} →
                      {inst_5 : AddCommGroup W} →
                        {inst_6 : Module R W} →
                          {inst_7 : TopologicalSpace Q} →
                            {inst_8 : AddTorsor W Q} →
                              {t : P_1 →ᴬ[R] Q} →
                                {R' : Type u_1} →
                                  {V' : Type u_2} →
                                    {W' : Type u_3} →
                                      {P' : Type u_4} →
                                        {Q' : Type u_5} →
                                          {inst' : Ring R'} →
                                            {inst'_1 : AddCommGroup V'} →
                                              {inst'_2 : Module R' V'} →
                                                {inst'_3 : TopologicalSpace P'} →
                                                  {inst'_4 : AddTorsor V' P'} →
                                                    {inst'_5 : AddCommGroup W'} →
                                                      {inst'_6 : Module R' W'} →
                                                        {inst'_7 : TopologicalSpace Q'} →
                                                          {inst'_8 : AddTorsor W' Q'} →
                                                            {t' : P' →ᴬ[R'] Q'} →
                                                              R = R' →
                                                                V = V' →
                                                                  W = W' →
                                                                    P_1 = P' →
                                                                      Q = Q' →
                                                                        inst ≍ inst' →
                                                                          inst_1 ≍ inst'_1 →
                                                                            inst_2 ≍ inst'_2 →
                                                                              inst_3 ≍ inst'_3 →
                                                                                inst_4 ≍ inst'_4 →
                                                                                  inst_5 ≍ inst'_5 →
                                                                                    inst_6 ≍ inst'_6 →
                                                                                      inst_7 ≍ inst'_7 →
                                                                                        inst_8 ≍ inst'_8 →
                                                                                          t ≍ t' →
                                                                                            ContinuousAffineMap.noConfusionType
                                                                                              P t t'

Defined in

Mathlib.Topology.Algebra.ContinuousAffineMap

Cited by

0 results in Mathlib

Foundations

Depth 12 from the axioms · uses no axioms