Metamath Proof Explorer

Definition df-retr

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)

Ref Expression
Assertion df-retr ⊢ Retr = j ∈ Top , k ∈ Top ⟼ r ∈ j Cn k | ∃ s ∈ k Cn j r ∘ s j Htpy j I ↾ ⋃ j ≠ ∅

Detailed syntax breakdown

Step Hyp Ref Expression
0 cretr class Retr
1 vj setvar j
2 ctop class Top
3 vk setvar k
4 vr setvar r
5 1 cv setvar j
6 ccn class Cn
7 3 cv setvar k
8 5 7 6 co class j Cn k
9 vs setvar s
10 7 5 6 co class k Cn j
11 4 cv setvar r
12 9 cv setvar s
13 11 12 ccom class r ∘ s
14 chtpy class Htpy
15 5 5 14 co class j Htpy j
16 cid class I
17 5 cuni class ⋃ j
18 16 17 cres class I ↾ ⋃ j
19 13 18 15 co class r ∘ s j Htpy j I ↾ ⋃ j
20 c0 class ∅
21 19 20 wne wff r ∘ s j Htpy j I ↾ ⋃ j ≠ ∅
22 21 9 10 wrex wff ∃ s ∈ k Cn j r ∘ s j Htpy j I ↾ ⋃ j ≠ ∅
23 22 4 8 crab class r ∈ j Cn k | ∃ s ∈ k Cn j r ∘ s j Htpy j I ↾ ⋃ j ≠ ∅
24 1 3 2 2 23 cmpo class j ∈ Top , k ∈ Top ⟼ r ∈ j Cn k | ∃ s ∈ k Cn j r ∘ s j Htpy j I ↾ ⋃ j ≠ ∅
25 0 24 wceq wff Retr = j ∈ Top , k ∈ Top ⟼ r ∈ j Cn k | ∃ s ∈ k Cn j r ∘ s j Htpy j I ↾ ⋃ j ≠ ∅