Theorems · Definition · manifolds

SingularManifold.noConfusion

{P : Sort u_4} →
  {X : Type u_1} →
    {inst : TopologicalSpace X} →
      {k : WithTop ℕ∞} →
        {E : Type u_2} →
          {H : Type u_3} →
            {inst_1 : NormedAddCommGroup E} →
              {inst_2 : NormedSpace ℝ E} →
                {inst_3 : FiniteDimensional ℝ E} →
                  {inst_4 : TopologicalSpace H} →
                    {I : ModelWithCorners ℝ E H} →
                      {t : SingularManifold X k I} →
                        {X' : Type u_1} →
                          {inst' : TopologicalSpace X'} →
                            {k' : WithTop ℕ∞} →
                              {E' : Type u_2} →
                                {H' : Type u_3} →
                                  {inst'_1 : NormedAddCommGroup E'} →
                                    {inst'_2 : NormedSpace ℝ E'} →
                                      {inst'_3 : FiniteDimensional ℝ E'} →
                                        {inst'_4 : TopologicalSpace H'} →
                                          {I' : ModelWithCorners ℝ E' H'} →
                                            {t' : SingularManifold X' k' I'} →
                                              X = X' →
                                                inst ≍ inst' →
                                                  k = k' →
                                                    E = E' →
                                                      H = H' →
                                                        inst_1 ≍ inst'_1 →
                                                          inst_2 ≍ inst'_2 →
                                                            inst_3 ≍ inst'_3 →
                                                              inst_4 ≍ inst'_4 →
                                                                I ≍ I' →
                                                                  t ≍ t' → SingularManifold.noConfusionType P t t'

Defined in

Mathlib.Geometry.Manifold.Bordism

Cited by

0 results in Mathlib

Foundations

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