:: Introduction to Homotopy Theory
:: by Adam Grabowski
::
:: Received September 10, 1997
:: Copyright (c) 1997-2021 Association of Mizar Users


Lm1: for r being Real holds
( ( 0 <= r & r <= 1 ) iff r in the carrier of I[01] )
proof end;

scheme :: BORSUK_2:sch 1
FrCard{ F1() -> non empty set , F2() -> set , F3( object ) -> set , P1[ set ] } :
card { F3(w) where w is Element of F1() : ( w in F2() & P1[w] ) } c= card F2()
proof end;

theorem :: BORSUK_2:1
for T, T1, T2, S being non empty TopSpace
for f being Function of T1,S
for g being Function of T2,S st T1 is SubSpace of T & T2 is SubSpace of T & ([#] T1) \/ ([#] T2) = [#] T & T1 is compact & T2 is compact & T is T_2 & f is continuous & g is continuous & ( for p being set st p in ([#] T1) /\ ([#] T2) holds
f . p = g . p ) holds
ex h being Function of T,S st
( h = f +* g & h is continuous )
proof end;

registration
let T be TopStruct ;
cluster id T -> continuous open ;
coherence
( id T is open & id T is continuous ) by FUNCT_1:92, FUNCT_2:94;
end;

registration
let T be TopStruct ;
cluster Relation-like the carrier of T -defined the carrier of T -valued Function-like one-to-one V17( the carrier of T) V21( the carrier of T, the carrier of T) continuous for Element of bool [: the carrier of T, the carrier of T:];
existence
ex b1 being Function of T,T st
( b1 is continuous & b1 is one-to-one )
proof end;
end;

theorem :: BORSUK_2:2
for S, T being non empty TopSpace
for f being Function of S,T st f is being_homeomorphism holds
f " is open
proof end;

theorem Th3: :: BORSUK_2:3
for T being non empty TopSpace
for a being Point of T ex f being Function of I[01],T st
( f is continuous & f . 0 = a & f . 1 = a )
proof end;

definition
let T be TopStruct ;
let a, b be Point of T;
pred a,b are_connected means :: BORSUK_2:def 1
 ex f being Function of I[01],T st
( f is continuous & f . 0 = a & f . 1 = b );
end;

:: deftheorem defines are_connected BORSUK_2:def 1 :
for T being TopStruct
for a, b being Point of T holds
( a,b are_connected iff ex f being Function of I[01],T st
( f is continuous & f . 0 = a & f . 1 = b ) );

definition
let T be non empty TopSpace;
let a, b be Point of T;
:: original: are_connected
redefine pred a,b are_connected ;
reflexivity
for a being Point of T holds (T,b1,b1) by Th3;
end;

definition
let T be TopStruct ;
let a, b be Point of T;
assume A1: a,b are_connected ;
mode Path of a,b -> Function of I[01],T means :Def2: :: BORSUK_2:def 2
( it is continuous & it . 0 = a & it . 1 = b );
existence
ex b1 being Function of I[01],T st
( b1 is continuous & b1 . 0 = a & b1 . 1 = b ) by A1;
end;

:: deftheorem Def2 defines Path BORSUK_2:def 2 :
for T being TopStruct
for a, b being Point of T st a,b are_connected holds
for b4 being Function of I[01],T holds
( b4 is Path of a,b iff ( b4 is continuous & b4 . 0 = a & b4 . 1 = b ) );

registration
let T be non empty TopSpace;
let a be Point of T;
cluster non empty Relation-like the carrier of I[01] -defined the carrier of T -valued Function-like V17( the carrier of I[01]) V21( the carrier of I[01], the carrier of T) continuous for Path of a,a;
existence
ex b1 being Path of a,a st b1 is continuous
proof end;
end;

definition
let T be TopStruct ;
attr T is pathwise_connected means :Def3: :: BORSUK_2:def 3
 for a, b being Point of T holds a,b are_connected ;
correctness
;
end;

:: deftheorem Def3 defines pathwise_connected BORSUK_2:def 3 :
for T being TopStruct holds
( T is pathwise_connected iff for a, b being Point of T holds a,b are_connected );

registration
cluster non empty strict TopSpace-like pathwise_connected for TopStruct ;
existence
ex b1 being TopSpace st
( b1 is strict & b1 is pathwise_connected & not b1 is empty )
proof end;
end;

definition
let T be pathwise_connected TopStruct ;
let a, b be Point of T;
redefine mode Path of a,b means :Def4: :: BORSUK_2:def 4
( it is continuous & it . 0 = a & it . 1 = b );
compatibility
for b1 being Function of I[01],T holds
( b1 is Path of a,b iff ( b1 is continuous & b1 . 0 = a & b1 . 1 = b ) )
proof end;
end;

:: deftheorem Def4 defines Path BORSUK_2:def 4 :
for T being pathwise_connected TopStruct
for a, b being Point of T
for b4 being Function of I[01],T holds
( b4 is Path of a,b iff ( b4 is continuous & b4 . 0 = a & b4 . 1 = b ) );

registration
let T be pathwise_connected TopStruct ;
let a, b be Point of T;
cluster -> continuous for Path of a,b;
coherence
for b1 being Path of a,b holds b1 is continuous by Def4;
end;

Lm2: ( 0 in [.0,1.] & 1 in [.0,1.] )
by XXREAL_1:1;

registration
cluster non empty TopSpace-like pathwise_connected -> non empty connected for TopStruct ;
coherence
for b1 being non empty TopSpace st b1 is pathwise_connected holds
b1 is connected
proof end;
end;

Lm3: for G being non empty TopSpace
for w1, w2, w3 being Point of G
for h1, h2 being Function of I[01],G st h1 is continuous & w1 = h1 . 0 & w2 = h1 . 1 & h2 is continuous & w2 = h2 . 0 & w3 = h2 . 1 holds
ex h3 being Function of I[01],G st
( h3 is continuous & w1 = h3 . 0 & w3 = h3 . 1 & rng h3 c= (rng h1) \/ (rng h2) )
proof end;

definition
let T be non empty TopSpace;
let a, b, c be Point of T;
let P be Path of a,b;
let Q be Path of b,c;
assume that
A1: a,b are_connected and
A2: b,c are_connected ;
func P + Q -> Path of a,c means :Def5: :: BORSUK_2:def 5
 for t being Point of I[01] holds
( ( t <= 1 / 2 implies it . t = P . (2 * t) ) & ( 1 / 2 <= t implies it . t = Q . ((2 * t) - 1) ) );
existence
ex b1 being Path of a,c st
for t being Point of I[01] holds
( ( t <= 1 / 2 implies b1 . t = P . (2 * t) ) & ( 1 / 2 <= t implies b1 . t = Q . ((2 * t) - 1) ) )
proof end;
uniqueness
for b1, b2 being Path of a,c st ( for t being Point of I[01] holds
( ( t <= 1 / 2 implies b1 . t = P . (2 * t) ) & ( 1 / 2 <= t implies b1 . t = Q . ((2 * t) - 1) ) ) ) & ( for t being Point of I[01] holds
( ( t <= 1 / 2 implies b2 . t = P . (2 * t) ) & ( 1 / 2 <= t implies b2 . t = Q . ((2 * t) - 1) ) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def5 defines + BORSUK_2:def 5 :
for T being non empty TopSpace
for a, b, c being Point of T
for P being Path of a,b
for Q being Path of b,c st a,b are_connected & b,c are_connected holds
for b7 being Path of a,c holds
( b7 = P + Q iff for t being Point of I[01] holds
( ( t <= 1 / 2 implies b7 . t = P . (2 * t) ) & ( 1 / 2 <= t implies b7 . t = Q . ((2 * t) - 1) ) ) );

registration
let T be non empty TopSpace;
let a be Point of T;
cluster non empty Relation-like the carrier of I[01] -defined the carrier of T -valued Function-like constant V17( the carrier of I[01]) V21( the carrier of I[01], the carrier of T) for Path of a,a;
existence
ex b1 being Path of a,a st b1 is constant
proof end;
end;

theorem :: BORSUK_2:4
canceled;

::$CT
theorem :: BORSUK_2:5
for T being non empty TopSpace
for a being Point of T
for P being constant Path of a,a holds P = I[01] --> a
proof end;

theorem Th5: :: BORSUK_2:6
for T being non empty TopSpace
for a being Point of T
for P being constant Path of a,a holds P + P = P
proof end;

registration
let T be non empty TopSpace;
let a be Point of T;
let P be constant Path of a,a;
cluster P + P -> constant ;
coherence
P + P is constant by Th5;
end;

definition
let T be non empty TopSpace;
let a, b be Point of T;
let P be Path of a,b;
assume A1: a,b are_connected ;
func - P -> Path of b,a means :Def6: :: BORSUK_2:def 6
 for t being Point of I[01] holds it . t = P . (1 - t);
existence
ex b1 being Path of b,a st
for t being Point of I[01] holds b1 . t = P . (1 - t)
proof end;
uniqueness
for b1, b2 being Path of b,a st ( for t being Point of I[01] holds b1 . t = P . (1 - t) ) & ( for t being Point of I[01] holds b2 . t = P . (1 - t) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def6 defines - BORSUK_2:def 6 :
for T being non empty TopSpace
for a, b being Point of T
for P being Path of a,b st a,b are_connected holds
for b5 being Path of b,a holds
( b5 = - P iff for t being Point of I[01] holds b5 . t = P . (1 - t) );

Lm4: for r being Real st 0 <= r & r <= 1 holds
( 0 <= 1 - r & 1 - r <= 1 )
proof end;

Lm5: for r being Real st r in the carrier of I[01] holds
1 - r in the carrier of I[01]
proof end;

theorem Th6: :: BORSUK_2:7
for T being non empty TopSpace
for a being Point of T
for P being constant Path of a,a holds - P = P
proof end;

registration
let T be non empty TopSpace;
let a be Point of T;
let P be constant Path of a,a;
cluster - P -> constant ;
coherence
- P is constant by Th6;
end;

theorem Th7: :: BORSUK_2:8
for X, Y being non empty TopSpace
for A being Subset-Family of Y
for f being Function of X,Y holds f " (union A) = union (f " A)
proof end;

definition
let S1, S2, T1, T2 be non empty TopSpace;
let f be Function of S1,S2;
let g be Function of T1,T2;
:: original: [:
redefine func [:f,g:] -> Function of [:S1,T1:],[:S2,T2:];
coherence
[:f,g:] is Function of [:S1,T1:],[:S2,T2:]
proof end;
end;

theorem Th8: :: BORSUK_2:9
for S1, S2, T1, T2 being non empty TopSpace
for f being continuous Function of S1,T1
for g being continuous Function of S2,T2
for P1, P2 being Subset of [:T1,T2:] st P2 in Base-Appr P1 holds
[:f,g:] " P2 is open
proof end;

theorem Th9: :: BORSUK_2:10
for S1, S2, T1, T2 being non empty TopSpace
for f being continuous Function of S1,T1
for g being continuous Function of S2,T2
for P2 being Subset of [:T1,T2:] st P2 is open holds
[:f,g:] " P2 is open
proof end;

registration
let S1, S2, T1, T2 be non empty TopSpace;
let f be continuous Function of S1,T1;
let g be continuous Function of S2,T2;
cluster [:f,g:] -> continuous for Function of [:S1,S2:],[:T1,T2:];
coherence
for b1 being Function of [:S1,S2:],[:T1,T2:] st b1 = [:f,g:] holds
b1 is continuous
proof end;
end;

registration
let T1, T2 be T_0 TopSpace;
cluster [:T1,T2:] -> T_0 ;
coherence
[:T1,T2:] is T_0
proof end;
end;

registration
let T1, T2 be T_1 TopSpace;
cluster [:T1,T2:] -> T_1 ;
coherence
[:T1,T2:] is T_1
proof end;
end;

registration
let T1, T2 be T_2 TopSpace;
cluster [:T1,T2:] -> T_2 ;
coherence
[:T1,T2:] is T_2
proof end;
end;

registration
cluster I[01] -> T_2 compact ;
coherence
( I[01] is compact & I[01] is T_2 )
proof end;
end;

definition
let T be non empty TopStruct ;
let a, b be Point of T;
let P, Q be Path of a,b;
pred P,Q are_homotopic means :: BORSUK_2:def 7
 ex f being Function of [:I[01],I[01]:],T st
( f is continuous & ( for t being Point of I[01] holds
( f . (t,0) = P . t & f . (t,1) = Q . t & f . (0,t) = a & f . (1,t) = b ) ) );
symmetry
for P, Q being Path of a,b st ex f being Function of [:I[01],I[01]:],T st
( f is continuous & ( for t being Point of I[01] holds
( f . (t,0) = P . t & f . (t,1) = Q . t & f . (0,t) = a & f . (1,t) = b ) ) ) holds
ex f being Function of [:I[01],I[01]:],T st
( f is continuous & ( for t being Point of I[01] holds
( f . (t,0) = Q . t & f . (t,1) = P . t & f . (0,t) = a & f . (1,t) = b ) ) )
proof end;
end;

:: deftheorem defines are_homotopic BORSUK_2:def 7 :
for T being non empty TopStruct
for a, b being Point of T
for P, Q being Path of a,b holds
( P,Q are_homotopic iff ex f being Function of [:I[01],I[01]:],T st
( f is continuous & ( for t being Point of I[01] holds
( f . (t,0) = P . t & f . (t,1) = Q . t & f . (0,t) = a & f . (1,t) = b ) ) ) );

theorem :: BORSUK_2:11
canceled;

::$CT
theorem Th10: :: BORSUK_2:12
for T being non empty TopSpace
for a, b being Point of T
for P being Path of a,b st a,b are_connected holds
P,P are_homotopic
proof end;

definition
let T be non empty pathwise_connected TopSpace;
let a, b be Point of T;
let P, Q be Path of a,b;
:: original: are_homotopic
redefine pred P,Q are_homotopic ;
reflexivity
for P being Path of a,b holds (T,a,b,b1,b1) by Th10, Def3;
end;

theorem :: BORSUK_2:13
for G being non empty TopSpace
for w1, w2, w3 being Point of G
for h1, h2 being Function of I[01],G st h1 is continuous & w1 = h1 . 0 & w2 = h1 . 1 & h2 is continuous & w2 = h2 . 0 & w3 = h2 . 1 holds
ex h3 being Function of I[01],G st
( h3 is continuous & w1 = h3 . 0 & w3 = h3 . 1 & rng h3 c= (rng h1) \/ (rng h2) ) by Lm3;

theorem :: BORSUK_2:14
for T being non empty TopSpace
for a, b, c being Point of T
for G1 being Path of a,b
for G2 being Path of b,c st G1 is continuous & G2 is continuous & G1 . 0 = a & G1 . 1 = b & G2 . 0 = b & G2 . 1 = c holds
( G1 + G2 is continuous & (G1 + G2) . 0 = a & (G1 + G2) . 1 = c )
proof end;

registration
let T be non empty TopSpace;
cluster non empty connected compact for Element of bool the carrier of T;
existence
ex b1 being Subset of T st
( not b1 is empty & b1 is compact & b1 is connected )
proof end;
end;

:: Moved from BORSUK_5:11, AK, 20.02.2006
theorem Th13: :: BORSUK_2:15
for T being non empty TopSpace
for a, b being Point of T st ex f being Function of I[01],T st
( f is continuous & f . 0 = a & f . 1 = b ) holds
ex g being Function of I[01],T st
( g is continuous & g . 0 = b & g . 1 = a )
proof end;

registration
cluster I[01] -> pathwise_connected ;
coherence
I[01] is pathwise_connected
proof end;
end;