:: Introduction to Homotopy Theory
::
:: Copyright (c) 1997-2018 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 ;
coherence
( id T is open & id T is continuous )
by ;
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 Function of ,;
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
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
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 (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 K113(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 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 ,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 ,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 ,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 ,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 ;
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 Subset 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
coherence
proof end;
end;