Theorems · Definition · manifolds

SingularManifold.toPUnit

{k : WithTop ℕ∞} →
  {E : Type u_4} →
    {H : Type u_5} →
      (M : Type u_6) →
        [inst : NormedAddCommGroup E] →
          [inst_1 : NormedSpace ℝ E] →
            [inst_2 : FiniteDimensional ℝ E] →
              [inst_3 : TopologicalSpace H] →
                (I : ModelWithCorners ℝ E H) →
                  [inst_4 : TopologicalSpace M] →
                    [inst_5 : ChartedSpace H M] →
                      [IsManifold I k M] →
                        [CompactSpace M] → [BoundarylessManifold I M] → SingularManifold PUnit.{u_9 + 1} k I

A smooth manifold induces a singular manifold on the one-point space.

Defined in

Mathlib.Geometry.Manifold.Bordism

Cited by

0 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupNormedSpaceFiniteDimensionalTopologicalSpaceTopologicalSpaceChartedSpaceIsManifoldCompactSpaceBoundarylessManifold