Mathbox for Mario Carneiro < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-retr Structured version   Unicode version

Definition df-retr 24896
 Description: Define the set of retractions on two topological spaces. We say that is a retraction from to . or Retr iff there is an such that are continuous functions called the retraction and section respectively, and their composite is homotopic to the identity map. If a retraction exists, we say is a retract of . (This terminology is borrowed from HoTT and appears to be nonstandard, although it has similaries to the concept of retract in the category of topological spaces and to a deformation retract in general topology.) Two topological spaces that are retracts of each other are called homotopy equivalent. (Contributed by Mario Carneiro, 11-Feb-2015.)
Assertion
Ref Expression
df-retr Retr Htpy
Distinct variable group:   ,,,

Detailed syntax breakdown of Definition df-retr
StepHypRef Expression
1 cretr 24895 . 2 Retr
2 vj . . 3
3 vk . . 3
4 ctop 16950 . . 3
5 vr . . . . . . . . 9
65cv 1651 . . . . . . . 8
7 vs . . . . . . . . 9
87cv 1651 . . . . . . . 8
96, 8ccom 4874 . . . . . . 7
10 cid 4485 . . . . . . . 8
112cv 1651 . . . . . . . . 9
1211cuni 4007 . . . . . . . 8
1310, 12cres 4872 . . . . . . 7
14 chtpy 18984 . . . . . . . 8 Htpy
1511, 11, 14co 6073 . . . . . . 7 Htpy
169, 13, 15co 6073 . . . . . 6 Htpy
17 c0 3620 . . . . . 6
1816, 17wne 2598 . . . . 5 Htpy
193cv 1651 . . . . . 6
20 ccn 17280 . . . . . 6
2119, 11, 20co 6073 . . . . 5
2218, 7, 21wrex 2698 . . . 4 Htpy
2311, 19, 20co 6073 . . . 4
2422, 5, 23crab 2701 . . 3 Htpy
252, 3, 4, 4, 24cmpt2 6075 . 2 Htpy
261, 25wceq 1652 1 Retr Htpy
 Colors of variables: wff set class
 Copyright terms: Public domain W3C validator