Theorems · Definition · manifolds

SingularManifold.comap

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

If (N, f) is a singular manifold on X and M another C^k manifold, a continuous map φ : M → N induces a singular manifold structure (M, f ∘ φ) on X.

Defined in

Mathlib.Geometry.Manifold.Bordism

Cited by

2 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceNormedAddCommGroupNormedSpaceFiniteDimensionalTopologicalSpaceTopologicalSpaceChartedSpaceIsManifoldCompactSpaceBoundarylessManifold