Theorems · Definition · algebraic topology
ContinuousMap.HomotopyEquiv.toFun
{X : Type u} →
{Y : Type v} → [inst : TopologicalSpace X] → [inst_1 : TopologicalSpace Y] → ContinuousMap.HomotopyEquiv X Y → C(X, Y)The forward map of a homotopy. Do NOT use directly. Use the coercion instead.
- Defined in
- Mathlib.Topology.Homotopy.Equiv
- Cited by
- 12 results in Mathlib
- Foundations
- Depth 2 from the axioms · uses no axioms
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites3
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- TopologicalSpacestatement and proof · cited by 24,529
- ContinuousMapstatement · cited by 2,491
- ContinuousMap.HomotopyEquivstatement and proof · cited by 23
Cited by19
Results whose statement or proof uses this declaration.
- ContinuousMap.HomotopyEquiv.symmproof · cited by 8
- ContinuousMap.HomotopyEquiv.transproof · cited by 6
- id_nullhomotopicproof · cited by 2
- ContinuousMap.HomotopyEquiv.extstatement and proof · cited by 1
- ContinuousMap.HomotopyEquiv.left_invstatement · cited by 1
- FundamentalGroupoidFunctor.equivOfHomotopyEquivproof · cited by 1
- ContinuousMap.HomotopyEquiv.ext_iffstatement and proof · cited by 0
- ContinuousMap.HomotopyEquiv.Simps.applyproof · cited by 0
- ContinuousMap.HomotopyEquiv.Simps.symm_applyproof · cited by 0
- ContinuousMap.HomotopyEquiv.piCongrRightproof · cited by 0
- ContinuousMap.HomotopyEquiv.prodCongrproof · cited by 0
- ContinuousMap.HomotopyEquiv.refl_applystatement and proof · cited by 0