Theorems · Definition · manifolds

SingularManifold.empty

(X : Type u_1) →
  [inst : TopologicalSpace X] →
    {k : WithTop ℕ∞} →
      {E : Type u_4} →
        {H : Type u_5} →
          [inst_1 : NormedAddCommGroup E] →
            [inst_2 : NormedSpace ℝ E] →
              [inst_3 : FiniteDimensional ℝ E] →
                [inst_4 : TopologicalSpace H] →
                  (M : Type u) →
                    [inst_5 : TopologicalSpace M] →
                      [inst_6 : ChartedSpace H M] →
                        (I : ModelWithCorners ℝ E H) → [IsManifold I k M] → [IsEmpty M] → SingularManifold X k I

The canonical singular manifold associated to the empty set (seen as a smooth manifold)

Defined in

Mathlib.Geometry.Manifold.Bordism

Cited by

1 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceNormedAddCommGroupNormedSpaceFiniteDimensionalTopologicalSpaceTopologicalSpaceChartedSpaceIsManifoldIsEmpty