Theorems · Definition · manifolds

SingularManifold.f

{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} → (self : SingularManifold X k I) → self.M → X

The underlying map M → X of a singular n-manifold (M, f) on X

Defined in

Mathlib.Geometry.Manifold.Bordism

Cited by

5 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceNormedAddCommGroupNormedSpaceFiniteDimensionalTopologicalSpace