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

begin

Lm1: for r being real number holds
( ( 0 <= r & r <= 1 ) iff r in the carrier of I[01] )

proof end;

scheme :: BORSUK_2:sch 1
FrCard{ F₁() -> non empty set , F₂() -> set , F₃( set ) -> set , P₁[ set ] } :

card { F₃(w) where w is Element of F₁() : ( w in F₂() & P₁[w] ) } c= card F₂()

proof end;

theorem :: BORSUK_2:1

for T1, S, T2, T 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 )

proof end;

end;

registration

let T be TopStruct ;
cluster Relation-like Function-like one-to-one V18( the carrier of T, the carrier of T) continuous Element of bool [: the carrier of T, the carrier of T:];
existence
ex b₁ being Function of T,T st
( b₁ is continuous & b₁ is one-to-one )

proof end;

end;

theorem :: BORSUK_2:2

canceled;

theorem :: BORSUK_2:3

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;

begin

theorem Th4: :: BORSUK_2:4

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 :Def1: :: BORSUK_2:def 1
ex f being Function of I[01],T st
( f is continuous & f . 0 = a & f . 1 = b );

end;

:: deftheorem Def1 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 a,a are_connected

proof end;

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 b₁ being Function of I[01],T st
( b₁ is continuous & b₁ . 0 = a & b₁ . 1 = b ) by A1, Def1;

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 b₄ being Function of I[01],T holds
( b₄ is Path of a,b iff ( b₄ is continuous & b₄ . 0 = a & b₄ . 1 = b ) );

registration

let T be non empty TopSpace;
let a be Point of T;
cluster non empty Relation-like Function-like V17( the carrier of I[01]) V18( the carrier of I[01], the carrier of T) continuous Path of a,a;
existence
ex b₁ being Path of a,a st b₁ 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 TopStruct ;
existence
ex b₁ being TopSpace st
( b₁ is strict & b₁ is pathwise_connected & not b₁ 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 b₁ being Function of I[01],T holds
( b₁ is Path of a,b iff ( b₁ is continuous & b₁ . 0 = a & b₁ . 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 b₄ being Function of I[01],T holds
( b₄ is Path of a,b iff ( b₄ is continuous & b₄ . 0 = a & b₄ . 1 = b ) );

registration

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

end;

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

proof end;

theorem Th5: :: BORSUK_2:5

for GX being non empty TopSpace st GX is pathwise_connected holds
GX is connected

proof end;

registration

cluster non empty TopSpace-like pathwise_connected -> non empty connected TopStruct ;
coherence
for b₁ being non empty TopSpace st b₁ is pathwise_connected holds
b₁ is connected by Th5;

end;

begin

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 b₁ being Path of a,c st
for t being Point of I[01] holds
( ( t <= 1 / 2 implies b₁ . t = P . (2 * t) ) & ( 1 / 2 <= t implies b₁ . t = Q . ((2 * t) - 1) ) )

proof end;

uniqueness
for b₁, b₂ being Path of a,c st ( for t being Point of I[01] holds
( ( t <= 1 / 2 implies b₁ . t = P . (2 * t) ) & ( 1 / 2 <= t implies b₁ . t = Q . ((2 * t) - 1) ) ) ) & ( for t being Point of I[01] holds
( ( t <= 1 / 2 implies b₂ . t = P . (2 * t) ) & ( 1 / 2 <= t implies b₂ . t = Q . ((2 * t) - 1) ) ) ) holds
b₁ = b₂

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 b₇ being Path of a,c holds
( b₇ = P + Q iff for t being Point of I[01] holds
( ( t <= 1 / 2 implies b₇ . t = P . (2 * t) ) & ( 1 / 2 <= t implies b₇ . t = Q . ((2 * t) - 1) ) ) );

registration

let T be non empty TopSpace;
let a be Point of T;
cluster non empty Relation-like Function-like constant V17( the carrier of I[01]) V18( the carrier of I[01], the carrier of T) Path of a,a;
existence
ex b₁ being Path of a,a st b₁ is constant

proof end;

end;

theorem :: 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 = I[01] --> a

proof end;

theorem Th7: :: 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 = 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 Th7;

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 b₁ being Path of b,a st
for t being Point of I[01] holds b₁ . t = P . (1 - t)

proof end;

uniqueness
for b₁, b₂ being Path of b,a st ( for t being Point of I[01] holds b₁ . t = P . (1 - t) ) & ( for t being Point of I[01] holds b₂ . t = P . (1 - t) ) holds
b₁ = b₂

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 b₅ being Path of b,a holds
( b₅ = - P iff for t being Point of I[01] holds b₅ . 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 Th8: :: BORSUK_2:8

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 Th8;

end;

begin

theorem Th9: :: BORSUK_2:9

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 Th10: :: 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 P1, P2 being Subset of [:T1,T2:] st P2 in Base-Appr P1 holds
[:f,g:] " P2 is open

proof end;

theorem Th11: :: BORSUK_2:11

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;

theorem :: BORSUK_2:12

canceled;

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 Function of [:S1,S2:],[:T1,T2:];
coherence
for b₁ being Function of [:S1,S2:],[:T1,T2:] st b₁ = [:f,g:] holds
b₁ is continuous

proof end;

end;

registration

cluster empty -> T_0 TopStruct ;
coherence
for b₁ being TopStruct st b₁ is empty holds
b₁ is T_0 ;

end;

registration

let T1, T2 be non empty T_0 TopSpace;
cluster [:T1,T2:] -> T_0 ;
coherence
[:T1,T2:] is T_0

proof end;

end;

theorem :: BORSUK_2:13

canceled;

theorem Th14: :: BORSUK_2:14

for T1, T2 being non empty TopSpace st T1 is T_1 & T2 is T_1 holds
[:T1,T2:] is T_1

proof end;

registration

let T1, T2 be non empty T_1 TopSpace;
cluster [:T1,T2:] -> T_1 ;
coherence
[:T1,T2:] is T_1 by Th14;

end;

Lm6: for T1, T2 being non empty TopSpace st T1 is T_2 & T2 is T_2 holds
[:T1,T2:] is T_2

proof end;

registration

let T1, T2 be non empty T_2 TopSpace;
cluster [:T1,T2:] -> T_2 ;
coherence
[:T1,T2:] is T_2 by Lm6;

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 Th15: :: BORSUK_2:15

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 P,P are_homotopic

proof end;

end;

theorem :: BORSUK_2:16

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:17

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 Element of bool the carrier of T;
existence
ex b₁ being Subset of T st
( not b₁ is empty & b₁ is compact & b₁ is connected )

proof end;

end;

theorem Th18: :: BORSUK_2:18

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;