Theorems · Definition · manifolds

SingularManifold.map

{X : Type u_7} →
  {Y : Type u_8} →
    [inst : TopologicalSpace X] →
      [inst_1 : TopologicalSpace Y] →
        {k : WithTop ℕ∞} →
          {E : Type u_9} →
            {H : Type u_10} →
              [inst_2 : NormedAddCommGroup E] →
                [inst_3 : NormedSpace ℝ E] →
                  [inst_4 : FiniteDimensional ℝ E] →
                    [inst_5 : TopologicalSpace H] →
                      {I : ModelWithCorners ℝ E H} →
                        SingularManifold X k I → {φ : X → Y} → Continuous φ → SingularManifold Y k I

A map of topological spaces induces a corresponding map of singular manifolds.

Defined in

Mathlib.Geometry.Manifold.Bordism

Cited by

3 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceTopologicalSpaceNormedAddCommGroupNormedSpaceFiniteDimensionalTopologicalSpace