Users' Mathboxes 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  R is a retraction from  J to  K. or  R  e.  ( J Retr  K ) iff there is an  S such that  R : J --> K ,  S : K
--> J are continuous functions called the retraction and section respectively, and their composite  R  o.  S is homotopic to the identity map. If a retraction exists, we say  J is a retract of  K. (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  =  ( j  e.  Top , 
k  e.  Top  |->  { r  e.  ( j  Cn  k )  |  E. s  e.  ( k  Cn  j ) ( ( r  o.  s ) ( j Htpy  j ) (  _I  |`  U. j ) )  =/=  (/) } )
Distinct variable group:    j, k, r, s

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