:: by Adam Grabowski

::

:: Received September 10, 1997

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

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 )

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

registration

let T be TopStruct ;

ex b_{1} being Function of T,T st

( b_{1} is continuous & b_{1} is one-to-one )

end;
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 b

( b

proof 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

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 )

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;

end;
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 );

ex f being Function of I[01],T st

( f is continuous & f . 0 = a & f . 1 = b );

:: 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 ) );

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,b_{1},b_{1})
by Th3;

end;
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,b

definition

let T be TopStruct ;

let a, b be Point of T;

assume A1: a,b are_connected ;

ex b_{1} being Function of I[01],T st

( b_{1} is continuous & b_{1} . 0 = a & b_{1} . 1 = b )
by A1;

end;
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 ( it is continuous & it . 0 = a & it . 1 = b );

ex b

( b

:: 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_{4} being Function of I[01],T holds

( b_{4} is Path of a,b iff ( b_{4} is continuous & b_{4} . 0 = a & b_{4} . 1 = b ) );

for T being TopStruct

for a, b being Point of T st a,b are_connected holds

for b

( b

registration

let T be non empty TopSpace;

let a be Point of T;

ex b_{1} being Path of a,a st b_{1} is continuous

end;
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 b

proof end;

definition

let T be TopStruct ;

;

end;
attr T is pathwise_connected means :Def3: :: BORSUK_2:def 3

for a, b being Point of T holds a,b are_connected ;

correctness for a, b being Point of T holds a,b are_connected ;

;

:: 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 );

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 b_{1} being TopSpace st

( b_{1} is strict & b_{1} is pathwise_connected & not b_{1} is empty )

end;
ex b

( b

proof end;

definition

let T be pathwise_connected TopStruct ;

let a, b be Point of T;

for b_{1} being Function of I[01],T holds

( b_{1} is Path of a,b iff ( b_{1} is continuous & b_{1} . 0 = a & b_{1} . 1 = b ) )

end;
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 ( it is continuous & it . 0 = a & it . 1 = b );

for b

( b

proof end;

:: deftheorem Def4 defines Path BORSUK_2:def 4 :

for T being pathwise_connected TopStruct

for a, b being Point of T

for b_{4} being Function of I[01],T holds

( b_{4} is Path of a,b iff ( b_{4} is continuous & b_{4} . 0 = a & b_{4} . 1 = b ) );

for T being pathwise_connected TopStruct

for a, b being Point of T

for b

( b

registration

let T be pathwise_connected TopStruct ;

let a, b be Point of T;

coherence

for b_{1} being Path of a,b holds b_{1} is continuous
by Def4;

end;
let a, b be Point of T;

coherence

for b

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

by XXREAL_1:1;

registration

coherence

for b_{1} being non empty TopSpace st b_{1} is pathwise_connected holds

b_{1} is connected

end;
for b

b

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

ex b_{1} being Path of a,c st

for t being Point of I[01] holds

( ( t <= 1 / 2 implies b_{1} . t = P . (2 * t) ) & ( 1 / 2 <= t implies b_{1} . t = Q . ((2 * t) - 1) ) )

for b_{1}, b_{2} being Path of a,c st ( for t being Point of I[01] holds

( ( t <= 1 / 2 implies b_{1} . t = P . (2 * t) ) & ( 1 / 2 <= t implies b_{1} . t = Q . ((2 * t) - 1) ) ) ) & ( for t being Point of I[01] holds

( ( t <= 1 / 2 implies b_{2} . t = P . (2 * t) ) & ( 1 / 2 <= t implies b_{2} . t = Q . ((2 * t) - 1) ) ) ) holds

b_{1} = b_{2}

end;
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 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) ) );

ex b

for t being Point of I[01] holds

( ( t <= 1 / 2 implies b

proof end;

uniqueness for b

( ( t <= 1 / 2 implies b

( ( t <= 1 / 2 implies b

b

proof 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_{7} being Path of a,c holds

( b_{7} = P + Q iff for t being Point of I[01] holds

( ( t <= 1 / 2 implies b_{7} . t = P . (2 * t) ) & ( 1 / 2 <= t implies b_{7} . t = Q . ((2 * t) - 1) ) ) );

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

( b

( ( t <= 1 / 2 implies b

registration

let T be non empty TopSpace;

let a be Point of T;

ex b_{1} being Path of a,a st b_{1} is constant

end;
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 b

proof end;

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

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

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;

coherence

P + P is constant by Th5;

end;
let a be Point of T;

let P be constant Path of a,a;

coherence

P + P is constant by Th5;

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 ;

ex b_{1} being Path of b,a st

for t being Point of I[01] holds b_{1} . t = P . (1 - t)

for b_{1}, b_{2} being Path of b,a st ( for t being Point of I[01] holds b_{1} . t = P . (1 - t) ) & ( for t being Point of I[01] holds b_{2} . t = P . (1 - t) ) holds

b_{1} = b_{2}

end;
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 for t being Point of I[01] holds it . t = P . (1 - t);

ex b

for t being Point of I[01] holds b

proof end;

uniqueness for b

b

proof 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_{5} being Path of b,a holds

( b_{5} = - P iff for t being Point of I[01] holds b_{5} . t = P . (1 - t) );

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

( b

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

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;

coherence

- P is constant by Th6;

end;
let a be Point of T;

let P be constant Path of a,a;

coherence

- P is constant by Th6;

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)

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

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

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

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

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;

coherence

for b_{1} being Function of [:S1,S2:],[:T1,T2:] st b_{1} = [:f,g:] holds

b_{1} is continuous

end;
let f be continuous Function of S1,T1;

let g be continuous Function of S2,T2;

coherence

for b

b

proof end;

registration
end;

registration
end;

registration
end;

registration
end;

definition

let T be non empty TopStruct ;

let a, b be Point of T;

let P, Q be Path of a,b;

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 ) ) )

end;
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 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 ) ) );

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;

:: 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 ) ) ) );

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

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

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,b_{1},b_{1})
by Th10, Def3;

end;
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,b

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;

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 )

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;

existence

ex b_{1} being Subset of T st

( not b_{1} is empty & b_{1} is compact & b_{1} is connected )

end;
existence

ex b

( not b

proof 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 )

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