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

Definition df-retr 30256
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 = (𝑗 ∈ Top, 𝑘 ∈ Top ↦ {𝑟 ∈ (𝑗 Cn 𝑘) ∣ ∃𝑠 ∈ (𝑘 Cn 𝑗)((𝑟𝑠)(𝑗 Htpy 𝑗)( I ↾ 𝑗)) ≠ ∅})
Distinct variable group:   𝑗,𝑘,𝑟,𝑠

Detailed syntax breakdown of Definition df-retr
StepHypRef Expression
1 cretr 30255 . 2 class Retr
2 vj . . 3 setvar 𝑗
3 vk . . 3 setvar 𝑘
4 ctop 20455 . . 3 class Top
5 vr . . . . . . . . 9 setvar 𝑟
65cv 1473 . . . . . . . 8 class 𝑟
7 vs . . . . . . . . 9 setvar 𝑠
87cv 1473 . . . . . . . 8 class 𝑠
96, 8ccom 5028 . . . . . . 7 class (𝑟𝑠)
10 cid 4934 . . . . . . . 8 class I
112cv 1473 . . . . . . . . 9 class 𝑗
1211cuni 4362 . . . . . . . 8 class 𝑗
1310, 12cres 5026 . . . . . . 7 class ( I ↾ 𝑗)
14 chtpy 22501 . . . . . . . 8 class Htpy
1511, 11, 14co 6523 . . . . . . 7 class (𝑗 Htpy 𝑗)
169, 13, 15co 6523 . . . . . 6 class ((𝑟𝑠)(𝑗 Htpy 𝑗)( I ↾ 𝑗))
17 c0 3869 . . . . . 6 class
1816, 17wne 2775 . . . . 5 wff ((𝑟𝑠)(𝑗 Htpy 𝑗)( I ↾ 𝑗)) ≠ ∅
193cv 1473 . . . . . 6 class 𝑘
20 ccn 20776 . . . . . 6 class Cn
2119, 11, 20co 6523 . . . . 5 class (𝑘 Cn 𝑗)
2218, 7, 21wrex 2892 . . . 4 wff 𝑠 ∈ (𝑘 Cn 𝑗)((𝑟𝑠)(𝑗 Htpy 𝑗)( I ↾ 𝑗)) ≠ ∅
2311, 19, 20co 6523 . . . 4 class (𝑗 Cn 𝑘)
2422, 5, 23crab 2895 . . 3 class {𝑟 ∈ (𝑗 Cn 𝑘) ∣ ∃𝑠 ∈ (𝑘 Cn 𝑗)((𝑟𝑠)(𝑗 Htpy 𝑗)( I ↾ 𝑗)) ≠ ∅}
252, 3, 4, 4, 24cmpt2 6525 . 2 class (𝑗 ∈ Top, 𝑘 ∈ Top ↦ {𝑟 ∈ (𝑗 Cn 𝑘) ∣ ∃𝑠 ∈ (𝑘 Cn 𝑗)((𝑟𝑠)(𝑗 Htpy 𝑗)( I ↾ 𝑗)) ≠ ∅})
261, 25wceq 1474 1 wff Retr = (𝑗 ∈ Top, 𝑘 ∈ Top ↦ {𝑟 ∈ (𝑗 Cn 𝑘) ∣ ∃𝑠 ∈ (𝑘 Cn 𝑗)((𝑟𝑠)(𝑗 Htpy 𝑗)( I ↾ 𝑗)) ≠ ∅})
Colors of variables: wff setvar class
This definition is referenced by: (None)
  Copyright terms: Public domain W3C validator