:: by Adam Grabowski

::

:: Received September 10, 1997

:: Copyright (c) 1997 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_{1}() -> non empty set , F_{2}() -> set , F_{3}( set ) -> set , P_{1}[ set ] } :

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

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 )

end;
cluster id T -> continuous open ;

coherence

( id T is open & id T is continuous )

proof 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_{1} being Function of T,T st

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

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

( b

proof 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

for f being Function of S,T st f is being_homeomorphism holds

f " is open

proof end;

begin

registration

cluster -> real Element of the carrier of I[01];

coherence

for b_{1} being Element of I[01] holds b_{1} is real
by BORSUK_1:83;

end;
coherence

for b

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 )

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

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

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 a,a are_connected

proof 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_{1} being Function of I[01],T st

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

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

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

( 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_{1} being Path of a,a st b_{1} is continuous

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

proof 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;
attr T is pathwise_connected means :Def3: :: BORSUK_2:def 3

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

correctness

;

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

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

end;
existence

ex b

( b

proof 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_{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

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

( b

registration

let T be pathwise_connected TopStruct ;

let a, b be Point of T;

cluster -> continuous Path of a,b;

coherence

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

end;
let a, b be Point of T;

cluster -> continuous Path of a,b;

coherence

for b

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

proof end;

theorem Th5: :: BORSUK_2:5

proof end;

registration

cluster non empty TopSpace-like pathwise_connected -> non empty connected TopStruct ;

coherence

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

b_{1} is connected
by Th5;

end;
coherence

for b

b

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_{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

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

( b

( ( t <= 1 / 2 implies b

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_{1} being Path of a,a st b_{1} is constant

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

proof 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

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

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

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_{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

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

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

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;
let a be Point of T;

let P be constant Path of a,a;

cluster - P -> constant ;

coherence

- P is constant by Th8;

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)

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

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

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_{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;

cluster [:f,g:] -> continuous Function of [:S1,S2:],[:T1,T2:];

coherence

for b

b

proof end;

registration

cluster empty -> T_0 TopStruct ;

coherence

for b_{1} being TopStruct st b_{1} is empty holds

b_{1} is T_0
;

end;
coherence

for b

b

registration

let T1, T2 be non empty T_0 TopSpace;

cluster [:T1,T2:] -> T_0 ;

coherence

[:T1,T2:] is T_0

end;
cluster [:T1,T2:] -> T_0 ;

coherence

[:T1,T2:] is T_0

proof end;

theorem :: BORSUK_2:13

canceled;

theorem Th14: :: BORSUK_2:14

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;
cluster [:T1,T2:] -> T_1 ;

coherence

[:T1,T2:] is T_1 by Th14;

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

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

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

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

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

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

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

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

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 )

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_{1} being Subset of T st

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

end;
cluster non empty connected compact Element of bool the carrier of T;

existence

ex b

( not b

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

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;