Theorems · Theorem · manifolds

SingularManifold.comap_M

∀ {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]
  [inst_7 : IsManifold I k M] [inst_8 : CompactSpace M] [inst_9 : BoundarylessManifold I M] (s : SingularManifold X k I)
  {φ : M → s.M} (hφ : Continuous φ), (s.comap hφ).M = M

Defined in

Mathlib.Geometry.Manifold.Bordism

Cited by

0 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceNormedAddCommGroupNormedSpaceFiniteDimensionalTopologicalSpaceTopologicalSpaceChartedSpaceIsManifoldCompactSpaceBoundarylessManifold