Theorems · Definition · manifolds

SingularManifold.sum

{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] →
                  {I : ModelWithCorners ℝ E H} →
                    SingularManifold X k I → SingularManifold X k I → SingularManifold X k I

The disjoint union of two singular I-manifolds on X is a singular I-manifold on X.

Defined in

Mathlib.Geometry.Manifold.Bordism

Cited by

2 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceNormedAddCommGroupNormedSpaceFiniteDimensionalTopologicalSpace