Theorems · Definition · manifolds

SingularManifold.mk.noConfusion

{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} →
                    {P : Sort u_4} →
                      {M : Type u} →
                        {topSpaceM : TopologicalSpace M} →
                          {chartedSpace : ChartedSpace H M} →
                            {isManifold : IsManifold I k M} →
                              {compactSpace : CompactSpace M} →
                                {boundaryless : BoundarylessManifold I M} →
                                  {f : M → X} →
                                    {hf : Continuous f} →
                                      {M' : Type u} →
                                        {topSpaceM' : TopologicalSpace M'} →
                                          {chartedSpace' : ChartedSpace H M'} →
                                            {isManifold' : IsManifold I k M'} →
                                              {compactSpace' : CompactSpace M'} →
                                                {boundaryless' : BoundarylessManifold I M'} →
                                                  {f' : M' → X} →
                                                    {hf' : Continuous f'} →
                                                      { M := M, topSpaceM := topSpaceM, chartedSpace := chartedSpace,
                                                            isManifold := isManifold, compactSpace := compactSpace,
                                                            boundaryless := boundaryless, f := f, hf := hf } =
                                                          { M := M', topSpaceM := topSpaceM',
                                                            chartedSpace := chartedSpace', isManifold := isManifold',
                                                            compactSpace := compactSpace',
                                                            boundaryless := boundaryless', f := f', hf := hf' } →
                                                        (M = M' →
                                                            topSpaceM ≍ topSpaceM' →
                                                              chartedSpace ≍ chartedSpace' → f ≍ f' → P) →
                                                          P

Defined in

Mathlib.Geometry.Manifold.Bordism

Cited by

1 results in Mathlib

Foundations

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