:: BORSUK_2 semantic presentation
begin
Lm1: for r being real number holds
( ( 0 <= r & r <= 1 ) iff r in the carrier of I[01] )
proof
let r be real number ; ::_thesis: ( ( 0 <= r & r <= 1 ) iff r in the carrier of I[01] )
A1: [.0,1.] = { r1 where r1 is Real : ( 0 <= r1 & r1 <= 1 ) } by RCOMP_1:def_1;
r is Real by XREAL_0:def_1;
hence ( 0 <= r & r <= 1 implies r in the carrier of I[01] ) by A1, BORSUK_1:40; ::_thesis: ( r in the carrier of I[01] implies ( 0 <= r & r <= 1 ) )
assume r in the carrier of I[01] ; ::_thesis: ( 0 <= r & r <= 1 )
then ex r2 being Real st
( r2 = r & 0 <= r2 & r2 <= 1 ) by A1, BORSUK_1:40;
hence ( 0 <= r & r <= 1 ) ; ::_thesis: verum
end;
scheme :: BORSUK_2:sch 1
FrCard{ F1() -> non empty set , F2() -> set , F3( set ) -> set , P1[ set ] } :
card { F3(w) where w is Element of F1() : ( w in F2() & P1[w] ) } c= card F2()
proof
consider f being Function such that
A1: ( dom f = F2() & ( for x being set st x in F2() holds
f . x = F3(x) ) ) from FUNCT_1:sch_3();
{ F3(w) where w is Element of F1() : ( w in F2() & P1[w] ) } c= rng f
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { F3(w) where w is Element of F1() : ( w in F2() & P1[w] ) } or x in rng f )
assume x in { F3(w) where w is Element of F1() : ( w in F2() & P1[w] ) } ; ::_thesis: x in rng f
then consider w being Element of F1() such that
A2: x = F3(w) and
A3: w in F2() and
P1[w] ;
f . w = x by A1, A2, A3;
hence x in rng f by A1, A3, FUNCT_1:def_3; ::_thesis: verum
end;
hence card { F3(w) where w is Element of F1() : ( w in F2() & P1[w] ) } c= card F2() by A1, CARD_1:12; ::_thesis: verum
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
let T1, S, T2, T be non empty TopSpace; ::_thesis: 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 )
let f be Function of T1,S; ::_thesis: 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 )
let g be Function of T2,S; ::_thesis: ( 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 ) implies ex h being Function of T,S st
( h = f +* g & h is continuous ) )
assume that
A1: T1 is SubSpace of T and
A2: T2 is SubSpace of T and
A3: ([#] T1) \/ ([#] T2) = [#] T and
A4: T1 is compact and
A5: T2 is compact and
A6: T is T_2 and
A7: f is continuous and
A8: g is continuous and
A9: for p being set st p in ([#] T1) /\ ([#] T2) holds
f . p = g . p ; ::_thesis: ex h being Function of T,S st
( h = f +* g & h is continuous )
set h = f +* g;
A10: dom g = [#] T2 by FUNCT_2:def_1;
A11: dom f = [#] T1 by FUNCT_2:def_1;
then A12: dom (f +* g) = the carrier of T by A3, A10, FUNCT_4:def_1;
rng (f +* g) c= (rng f) \/ (rng g) by FUNCT_4:17;
then reconsider h = f +* g as Function of T,S by A12, FUNCT_2:2, XBOOLE_1:1;
take h ; ::_thesis: ( h = f +* g & h is continuous )
thus h = f +* g ; ::_thesis: h is continuous
for P being Subset of S st P is closed holds
h " P is closed
proof
let P be Subset of S; ::_thesis: ( P is closed implies h " P is closed )
reconsider P3 = f " P as Subset of T1 ;
reconsider P4 = g " P as Subset of T2 ;
[#] T1 c= [#] T by A3, XBOOLE_1:7;
then reconsider P1 = f " P as Subset of T by XBOOLE_1:1;
[#] T2 c= [#] T by A3, XBOOLE_1:7;
then reconsider P2 = g " P as Subset of T by XBOOLE_1:1;
A13: dom h = (dom f) \/ (dom g) by FUNCT_4:def_1;
A14: now__::_thesis:_for_x_being_set_holds_
(_(_x_in_(h_"_P)_/\_([#]_T2)_implies_x_in_g_"_P_)_&_(_x_in_g_"_P_implies_x_in_(h_"_P)_/\_([#]_T2)_)_)
let x be set ; ::_thesis: ( ( x in (h " P) /\ ([#] T2) implies x in g " P ) & ( x in g " P implies x in (h " P) /\ ([#] T2) ) )
thus ( x in (h " P) /\ ([#] T2) implies x in g " P ) ::_thesis: ( x in g " P implies x in (h " P) /\ ([#] T2) )
proof
assume A15: x in (h " P) /\ ([#] T2) ; ::_thesis: x in g " P
then x in h " P by XBOOLE_0:def_4;
then A16: h . x in P by FUNCT_1:def_7;
g . x = h . x by A10, A15, FUNCT_4:13;
hence x in g " P by A10, A15, A16, FUNCT_1:def_7; ::_thesis: verum
end;
assume A17: x in g " P ; ::_thesis: x in (h " P) /\ ([#] T2)
then A18: x in dom g by FUNCT_1:def_7;
g . x in P by A17, FUNCT_1:def_7;
then A19: h . x in P by A18, FUNCT_4:13;
x in dom h by A13, A18, XBOOLE_0:def_3;
then x in h " P by A19, FUNCT_1:def_7;
hence x in (h " P) /\ ([#] T2) by A17, XBOOLE_0:def_4; ::_thesis: verum
end;
A20: for x being set st x in [#] T1 holds
h . x = f . x
proof
let x be set ; ::_thesis: ( x in [#] T1 implies h . x = f . x )
assume A21: x in [#] T1 ; ::_thesis: h . x = f . x
now__::_thesis:_h_._x_=_f_._x
percases ( x in [#] T2 or not x in [#] T2 ) ;
supposeA22: x in [#] T2 ; ::_thesis: h . x = f . x
then x in ([#] T1) /\ ([#] T2) by A21, XBOOLE_0:def_4;
then f . x = g . x by A9;
hence h . x = f . x by A10, A22, FUNCT_4:13; ::_thesis: verum
end;
suppose not x in [#] T2 ; ::_thesis: h . x = f . x
hence h . x = f . x by A10, FUNCT_4:11; ::_thesis: verum
end;
end;
end;
hence h . x = f . x ; ::_thesis: verum
end;
now__::_thesis:_for_x_being_set_holds_
(_(_x_in_(h_"_P)_/\_([#]_T1)_implies_x_in_f_"_P_)_&_(_x_in_f_"_P_implies_x_in_(h_"_P)_/\_([#]_T1)_)_)
let x be set ; ::_thesis: ( ( x in (h " P) /\ ([#] T1) implies x in f " P ) & ( x in f " P implies x in (h " P) /\ ([#] T1) ) )
thus ( x in (h " P) /\ ([#] T1) implies x in f " P ) ::_thesis: ( x in f " P implies x in (h " P) /\ ([#] T1) )
proof
assume A23: x in (h " P) /\ ([#] T1) ; ::_thesis: x in f " P
then x in h " P by XBOOLE_0:def_4;
then A24: h . x in P by FUNCT_1:def_7;
f . x = h . x by A20, A23;
hence x in f " P by A11, A23, A24, FUNCT_1:def_7; ::_thesis: verum
end;
assume A25: x in f " P ; ::_thesis: x in (h " P) /\ ([#] T1)
then x in dom f by FUNCT_1:def_7;
then A26: x in dom h by A13, XBOOLE_0:def_3;
f . x in P by A25, FUNCT_1:def_7;
then h . x in P by A20, A25;
then x in h " P by A26, FUNCT_1:def_7;
hence x in (h " P) /\ ([#] T1) by A25, XBOOLE_0:def_4; ::_thesis: verum
end;
then A27: (h " P) /\ ([#] T1) = f " P by TARSKI:1;
assume A28: P is closed ; ::_thesis: h " P is closed
then P3 is closed by A7, PRE_TOPC:def_6;
then P3 is compact by A4, COMPTS_1:8;
then A29: P1 is compact by A1, COMPTS_1:19;
P4 is closed by A8, A28, PRE_TOPC:def_6;
then P4 is compact by A5, COMPTS_1:8;
then A30: P2 is compact by A2, COMPTS_1:19;
h " P = (h " P) /\ (([#] T1) \/ ([#] T2)) by A11, A10, A13, RELAT_1:132, XBOOLE_1:28
.= ((h " P) /\ ([#] T1)) \/ ((h " P) /\ ([#] T2)) by XBOOLE_1:23 ;
then h " P = (f " P) \/ (g " P) by A27, A14, TARSKI:1;
hence h " P is closed by A6, A29, A30; ::_thesis: verum
end;
hence h is continuous by PRE_TOPC:def_6; ::_thesis: verum
end;
registration
let T be TopStruct ;
cluster id T -> continuous open ;
coherence
( id T is open & id T is continuous )
proof
thus id T is open ::_thesis: id T is continuous
proof
let A be Subset of T; :: according to T_0TOPSP:def_2 ::_thesis: ( not A is open or (id T) .: A is open )
assume A is open ; ::_thesis: (id T) .: A is open
hence (id T) .: A is open by FUNCT_1:92; ::_thesis: verum
end;
let V be Subset of T; :: according to PRE_TOPC:def_6 ::_thesis: ( not V is closed or (id T) " V is closed )
assume V is closed ; ::_thesis: (id T) " V is closed
hence (id T) " V is closed by FUNCT_2:94; ::_thesis: verum
end;
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
take id T ; ::_thesis: ( id T is continuous & id T is one-to-one )
thus ( id T is continuous & id T is one-to-one ) ; ::_thesis: verum
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
let S, T be non empty TopSpace; ::_thesis: for f being Function of S,T st f is being_homeomorphism holds
f " is open
let f be Function of S,T; ::_thesis: ( f is being_homeomorphism implies f " is open )
assume f is being_homeomorphism ; ::_thesis: f " is open
then A1: ( rng f = [#] T & f is one-to-one & f is continuous ) by TOPS_2:def_5;
let P be Subset of T; :: according to T_0TOPSP:def_2 ::_thesis: ( not P is open or (f ") .: P is open )
f " P = (f ") .: P by A1, TOPS_2:55;
hence ( not P is open or (f ") .: P is open ) by A1, TOPS_2:43; ::_thesis: verum
end;
begin
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
let T be non empty TopSpace; ::_thesis: for a being Point of T ex f being Function of I[01],T st
( f is continuous & f . 0 = a & f . 1 = a )
let a be Point of T; ::_thesis: ex f being Function of I[01],T st
( f is continuous & f . 0 = a & f . 1 = a )
take I[01] --> a ; ::_thesis: ( I[01] --> a is continuous & (I[01] --> a) . 0 = a & (I[01] --> a) . 1 = a )
thus ( I[01] --> a is continuous & (I[01] --> a) . 0 = a & (I[01] --> a) . 1 = a ) by BORSUK_1:def_14, BORSUK_1:def_15, FUNCOP_1:7; ::_thesis: verum
end;
definition
let T be TopStruct ;
let a, b be Point of T;
preda,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 preda,b are_connected ;
reflexivity
for a being Point of T holds (T,b1,b1)
proof
let a be Point of T; ::_thesis: (T,a,a)
thus ex f being Function of I[01],T st
( f is continuous & f . 0 = a & f . 1 = a ) by Th3; :: according to BORSUK_2:def_1 ::_thesis: verum
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 b1 being Function of I[01],T st
( b1 is continuous & b1 . 0 = a & b1 . 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 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
set IT = I[01] --> a;
A1: a,a are_connected ;
( (I[01] --> a) . 0 = a & (I[01] --> a) . 1 = a ) by BORSUK_1:def_14, BORSUK_1:def_15, FUNCOP_1:7;
then I[01] --> a is Path of a,a by A1, Def2;
hence ex b1 being Path of a,a st b1 is continuous ; ::_thesis: verum
end;
end;
definition
let T be TopStruct ;
attrT 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
set T = I[01] | {0[01]};
0[01] in {0[01]} by TARSKI:def_1;
then reconsider nl = 0[01] as Point of (I[01] | {0[01]}) by PRE_TOPC:8;
A1: the carrier of (I[01] | {0[01]}) = {0[01]} by PRE_TOPC:8;
for a, b being Point of (I[01] | {0[01]}) holds a,b are_connected
proof
reconsider f = I[01] --> nl as Function of I[01],(I[01] | {0[01]}) ;
let a, b be Point of (I[01] | {0[01]}); ::_thesis: a,b are_connected
take f ; :: according to BORSUK_2:def_1 ::_thesis: ( f is continuous & f . 0 = a & f . 1 = b )
thus f is continuous ; ::_thesis: ( f . 0 = a & f . 1 = b )
( a = nl & b = nl ) by A1, TARSKI:def_1;
hence ( f . 0 = a & f . 1 = b ) by BORSUK_1:def_15, FUNCOP_1:7; ::_thesis: verum
end;
then I[01] | {0[01]} is pathwise_connected by Def3;
hence ex b1 being TopSpace st
( b1 is strict & b1 is pathwise_connected & not b1 is empty ) ; ::_thesis: verum
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
a,b are_connected by Def3;
hence 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 ) ) by Def2; ::_thesis: verum
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
let GX be non empty TopSpace; ::_thesis: ( GX is pathwise_connected implies GX is connected )
assume A1: for x, y being Point of GX holds x,y are_connected ; :: according to BORSUK_2:def_3 ::_thesis: GX is connected
for x, y being Point of GX ex GY being non empty TopSpace st
( GY is connected & ex f being Function of GY,GX st
( f is continuous & x in rng f & y in rng f ) )
proof
let x, y be Point of GX; ::_thesis: ex GY being non empty TopSpace st
( GY is connected & ex f being Function of GY,GX st
( f is continuous & x in rng f & y in rng f ) )
x,y are_connected by A1;
then consider h being Function of I[01],GX such that
A2: h is continuous and
A3: x = h . 0 and
A4: y = h . 1 by Def1;
1 in dom h by Lm2, BORSUK_1:40, FUNCT_2:def_1;
then A5: y in rng h by A4, FUNCT_1:def_3;
0 in dom h by Lm2, BORSUK_1:40, FUNCT_2:def_1;
then x in rng h by A3, FUNCT_1:def_3;
hence ex GY being non empty TopSpace st
( GY is connected & ex f being Function of GY,GX st
( f is continuous & x in rng f & y in rng f ) ) by A2, A5, TREAL_1:19; ::_thesis: verum
end;
hence GX is connected by TOPS_2:63; ::_thesis: verum
end;
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
let G be non empty TopSpace; ::_thesis: 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) )
let w1, w2, w3 be Point of G; ::_thesis: 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) )
let h1, h2 be Function of I[01],G; ::_thesis: ( h1 is continuous & w1 = h1 . 0 & w2 = h1 . 1 & h2 is continuous & w2 = h2 . 0 & w3 = h2 . 1 implies 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) ) )
assume that
A1: h1 is continuous and
A2: w1 = h1 . 0 and
A3: w2 = h1 . 1 and
A4: h2 is continuous and
A5: w2 = h2 . 0 and
A6: w3 = h2 . 1 ; ::_thesis: 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) )
w2,w3 are_connected by A4, A5, A6, Def1;
then reconsider g2 = h2 as Path of w2,w3 by A4, A5, A6, Def2;
w1,w2 are_connected by A1, A2, A3, Def1;
then reconsider g1 = h1 as Path of w1,w2 by A1, A2, A3, Def2;
set P1 = g1;
set P2 = g2;
set p1 = w1;
set p3 = w3;
ex P0 being Path of w1,w3 st
( P0 is continuous & P0 . 0 = w1 & P0 . 1 = w3 & ( for t being Point of I[01]
for t9 being Real st t = t9 holds
( ( 0 <= t9 & t9 <= 1 / 2 implies P0 . t = g1 . (2 * t9) ) & ( 1 / 2 <= t9 & t9 <= 1 implies P0 . t = g2 . ((2 * t9) - 1) ) ) ) )
proof
1 / 2 in { r where r is Real : ( 0 <= r & r <= 1 ) } ;
then reconsider pol = 1 / 2 as Point of I[01] by BORSUK_1:40, RCOMP_1:def_1;
reconsider T1 = Closed-Interval-TSpace (0,(1 / 2)), T2 = Closed-Interval-TSpace ((1 / 2),1) as SubSpace of I[01] by TOPMETR:20, TREAL_1:3;
set e2 = P[01] ((1 / 2),1,((#) (0,1)),((0,1) (#)));
set e1 = P[01] (0,(1 / 2),((#) (0,1)),((0,1) (#)));
set E1 = g1 * (P[01] (0,(1 / 2),((#) (0,1)),((0,1) (#))));
set E2 = g2 * (P[01] ((1 / 2),1,((#) (0,1)),((0,1) (#))));
set f = (g1 * (P[01] (0,(1 / 2),((#) (0,1)),((0,1) (#))))) +* (g2 * (P[01] ((1 / 2),1,((#) (0,1)),((0,1) (#)))));
A7: dom (P[01] (0,(1 / 2),((#) (0,1)),((0,1) (#)))) = the carrier of (Closed-Interval-TSpace (0,(1 / 2))) by FUNCT_2:def_1
.= [.0,(1 / 2).] by TOPMETR:18 ;
A8: dom (P[01] ((1 / 2),1,((#) (0,1)),((0,1) (#)))) = the carrier of (Closed-Interval-TSpace ((1 / 2),1)) by FUNCT_2:def_1
.= [.(1 / 2),1.] by TOPMETR:18 ;
reconsider gg = g2 * (P[01] ((1 / 2),1,((#) (0,1)),((0,1) (#)))) as Function of T2,G by TOPMETR:20;
reconsider ff = g1 * (P[01] (0,(1 / 2),((#) (0,1)),((0,1) (#)))) as Function of T1,G by TOPMETR:20;
A9: for t9 being Real st 1 / 2 <= t9 & t9 <= 1 holds
(g2 * (P[01] ((1 / 2),1,((#) (0,1)),((0,1) (#))))) . t9 = g2 . ((2 * t9) - 1)
proof
reconsider r1 = (#) (0,1), r2 = (0,1) (#) as Real by TREAL_1:5;
dom (P[01] ((1 / 2),1,((#) (0,1)),((0,1) (#)))) = the carrier of (Closed-Interval-TSpace ((1 / 2),1)) by FUNCT_2:def_1;
then A10: dom (P[01] ((1 / 2),1,((#) (0,1)),((0,1) (#)))) = [.(1 / 2),1.] by TOPMETR:18
.= { r where r is Real : ( 1 / 2 <= r & r <= 1 ) } by RCOMP_1:def_1 ;
let t9 be Real; ::_thesis: ( 1 / 2 <= t9 & t9 <= 1 implies (g2 * (P[01] ((1 / 2),1,((#) (0,1)),((0,1) (#))))) . t9 = g2 . ((2 * t9) - 1) )
assume ( 1 / 2 <= t9 & t9 <= 1 ) ; ::_thesis: (g2 * (P[01] ((1 / 2),1,((#) (0,1)),((0,1) (#))))) . t9 = g2 . ((2 * t9) - 1)
then A11: t9 in dom (P[01] ((1 / 2),1,((#) (0,1)),((0,1) (#)))) by A10;
then reconsider s = t9 as Point of (Closed-Interval-TSpace ((1 / 2),1)) ;
(P[01] ((1 / 2),1,((#) (0,1)),((0,1) (#)))) . s = (((r2 - r1) / (1 - (1 / 2))) * t9) + (((1 * r1) - ((1 / 2) * r2)) / (1 - (1 / 2))) by TREAL_1:11
.= (2 * t9) - 1 by TREAL_1:5 ;
hence (g2 * (P[01] ((1 / 2),1,((#) (0,1)),((0,1) (#))))) . t9 = g2 . ((2 * t9) - 1) by A11, FUNCT_1:13; ::_thesis: verum
end;
A12: for t9 being Real st 0 <= t9 & t9 <= 1 / 2 holds
(g1 * (P[01] (0,(1 / 2),((#) (0,1)),((0,1) (#))))) . t9 = g1 . (2 * t9)
proof
reconsider r1 = (#) (0,1), r2 = (0,1) (#) as Real by TREAL_1:5;
dom (P[01] (0,(1 / 2),((#) (0,1)),((0,1) (#)))) = the carrier of (Closed-Interval-TSpace (0,(1 / 2))) by FUNCT_2:def_1;
then A13: dom (P[01] (0,(1 / 2),((#) (0,1)),((0,1) (#)))) = [.0,(1 / 2).] by TOPMETR:18
.= { r where r is Real : ( 0 <= r & r <= 1 / 2 ) } by RCOMP_1:def_1 ;
let t9 be Real; ::_thesis: ( 0 <= t9 & t9 <= 1 / 2 implies (g1 * (P[01] (0,(1 / 2),((#) (0,1)),((0,1) (#))))) . t9 = g1 . (2 * t9) )
assume ( 0 <= t9 & t9 <= 1 / 2 ) ; ::_thesis: (g1 * (P[01] (0,(1 / 2),((#) (0,1)),((0,1) (#))))) . t9 = g1 . (2 * t9)
then A14: t9 in dom (P[01] (0,(1 / 2),((#) (0,1)),((0,1) (#)))) by A13;
then reconsider s = t9 as Point of (Closed-Interval-TSpace (0,(1 / 2))) ;
(P[01] (0,(1 / 2),((#) (0,1)),((0,1) (#)))) . s = (((r2 - r1) / ((1 / 2) - 0)) * t9) + ((((1 / 2) * r1) - (0 * r2)) / ((1 / 2) - 0)) by TREAL_1:11
.= 2 * t9 by TREAL_1:5 ;
hence (g1 * (P[01] (0,(1 / 2),((#) (0,1)),((0,1) (#))))) . t9 = g1 . (2 * t9) by A14, FUNCT_1:13; ::_thesis: verum
end;
then A15: ff . (1 / 2) = g2 . ((2 * (1 / 2)) - 1) by A3, A5
.= gg . pol by A9 ;
( [#] T1 = [.0,(1 / 2).] & [#] T2 = [.(1 / 2),1.] ) by TOPMETR:18;
then A16: ( ([#] T1) \/ ([#] T2) = [#] I[01] & ([#] T1) /\ ([#] T2) = {pol} ) by BORSUK_1:40, XXREAL_1:174, XXREAL_1:418;
A17: T2 is compact by HEINE:4;
dom g1 = the carrier of I[01] by FUNCT_2:def_1;
then A18: rng (P[01] (0,(1 / 2),((#) (0,1)),((0,1) (#)))) c= dom g1 by TOPMETR:20;
( dom g2 = the carrier of I[01] & rng (P[01] ((1 / 2),1,((#) (0,1)),((0,1) (#)))) c= the carrier of (Closed-Interval-TSpace (0,1)) ) by FUNCT_2:def_1;
then A19: dom (g2 * (P[01] ((1 / 2),1,((#) (0,1)),((0,1) (#))))) = dom (P[01] ((1 / 2),1,((#) (0,1)),((0,1) (#)))) by RELAT_1:27, TOPMETR:20;
not 0 in { r where r is Real : ( 1 / 2 <= r & r <= 1 ) }
proof
assume 0 in { r where r is Real : ( 1 / 2 <= r & r <= 1 ) } ; ::_thesis: contradiction
then ex rr being Real st
( rr = 0 & 1 / 2 <= rr & rr <= 1 ) ;
hence contradiction ; ::_thesis: verum
end;
then not 0 in dom (g2 * (P[01] ((1 / 2),1,((#) (0,1)),((0,1) (#))))) by A8, A19, RCOMP_1:def_1;
then A20: ((g1 * (P[01] (0,(1 / 2),((#) (0,1)),((0,1) (#))))) +* (g2 * (P[01] ((1 / 2),1,((#) (0,1)),((0,1) (#)))))) . 0 = (g1 * (P[01] (0,(1 / 2),((#) (0,1)),((0,1) (#))))) . 0 by FUNCT_4:11
.= g1 . (2 * 0) by A12
.= w1 by A2 ;
A21: dom ((g1 * (P[01] (0,(1 / 2),((#) (0,1)),((0,1) (#))))) +* (g2 * (P[01] ((1 / 2),1,((#) (0,1)),((0,1) (#)))))) = (dom (g1 * (P[01] (0,(1 / 2),((#) (0,1)),((0,1) (#)))))) \/ (dom (g2 * (P[01] ((1 / 2),1,((#) (0,1)),((0,1) (#)))))) by FUNCT_4:def_1
.= [.0,(1 / 2).] \/ [.(1 / 2),1.] by A7, A8, A18, A19, RELAT_1:27
.= the carrier of I[01] by BORSUK_1:40, XXREAL_1:174 ;
rng ((g1 * (P[01] (0,(1 / 2),((#) (0,1)),((0,1) (#))))) +* (g2 * (P[01] ((1 / 2),1,((#) (0,1)),((0,1) (#)))))) c= (rng (g1 * (P[01] (0,(1 / 2),((#) (0,1)),((0,1) (#)))))) \/ (rng (g2 * (P[01] ((1 / 2),1,((#) (0,1)),((0,1) (#)))))) by FUNCT_4:17;
then A22: rng ((g1 * (P[01] (0,(1 / 2),((#) (0,1)),((0,1) (#))))) +* (g2 * (P[01] ((1 / 2),1,((#) (0,1)),((0,1) (#)))))) c= the carrier of G by XBOOLE_1:1;
A23: ( R^1 is T_2 & T1 is compact ) by HEINE:4, PCOMPS_1:34, TOPMETR:def_6;
reconsider f = (g1 * (P[01] (0,(1 / 2),((#) (0,1)),((0,1) (#))))) +* (g2 * (P[01] ((1 / 2),1,((#) (0,1)),((0,1) (#))))) as Function of I[01],G by A21, A22, FUNCT_2:def_1, RELSET_1:4;
( P[01] (0,(1 / 2),((#) (0,1)),((0,1) (#))) is continuous & P[01] ((1 / 2),1,((#) (0,1)),((0,1) (#))) is continuous ) by TREAL_1:12;
then reconsider f = f as continuous Function of I[01],G by A1, A4, A15, A16, A23, A17, COMPTS_1:20, TOPMETR:20;
1 in { r where r is Real : ( 1 / 2 <= r & r <= 1 ) } ;
then 1 in dom (g2 * (P[01] ((1 / 2),1,((#) (0,1)),((0,1) (#))))) by A8, A19, RCOMP_1:def_1;
then A24: f . 1 = (g2 * (P[01] ((1 / 2),1,((#) (0,1)),((0,1) (#))))) . 1 by FUNCT_4:13
.= g2 . ((2 * 1) - 1) by A9
.= w3 by A6 ;
then w1,w3 are_connected by A20, Def1;
then reconsider f = f as Path of w1,w3 by A20, A24, Def2;
for t being Point of I[01]
for t9 being Real st t = t9 holds
( ( 0 <= t9 & t9 <= 1 / 2 implies f . t = g1 . (2 * t9) ) & ( 1 / 2 <= t9 & t9 <= 1 implies f . t = g2 . ((2 * t9) - 1) ) )
proof
let t be Point of I[01]; ::_thesis: for t9 being Real st t = t9 holds
( ( 0 <= t9 & t9 <= 1 / 2 implies f . t = g1 . (2 * t9) ) & ( 1 / 2 <= t9 & t9 <= 1 implies f . t = g2 . ((2 * t9) - 1) ) )
let t9 be Real; ::_thesis: ( t = t9 implies ( ( 0 <= t9 & t9 <= 1 / 2 implies f . t = g1 . (2 * t9) ) & ( 1 / 2 <= t9 & t9 <= 1 implies f . t = g2 . ((2 * t9) - 1) ) ) )
assume A25: t = t9 ; ::_thesis: ( ( 0 <= t9 & t9 <= 1 / 2 implies f . t = g1 . (2 * t9) ) & ( 1 / 2 <= t9 & t9 <= 1 implies f . t = g2 . ((2 * t9) - 1) ) )
thus ( 0 <= t9 & t9 <= 1 / 2 implies f . t = g1 . (2 * t9) ) ::_thesis: ( 1 / 2 <= t9 & t9 <= 1 implies f . t = g2 . ((2 * t9) - 1) )
proof
assume A26: ( 0 <= t9 & t9 <= 1 / 2 ) ; ::_thesis: f . t = g1 . (2 * t9)
then t9 in { r where r is Real : ( 0 <= r & r <= 1 / 2 ) } ;
then A27: t9 in [.0,(1 / 2).] by RCOMP_1:def_1;
percases ( t9 <> 1 / 2 or t9 = 1 / 2 ) ;
supposeA28: t9 <> 1 / 2 ; ::_thesis: f . t = g1 . (2 * t9)
not t9 in dom (g2 * (P[01] ((1 / 2),1,((#) (0,1)),((0,1) (#)))))
proof
assume t9 in dom (g2 * (P[01] ((1 / 2),1,((#) (0,1)),((0,1) (#))))) ; ::_thesis: contradiction
then t9 in [.0,(1 / 2).] /\ [.(1 / 2),1.] by A8, A19, A27, XBOOLE_0:def_4;
then t9 in {(1 / 2)} by XXREAL_1:418;
hence contradiction by A28, TARSKI:def_1; ::_thesis: verum
end;
then f . t = (g1 * (P[01] (0,(1 / 2),((#) (0,1)),((0,1) (#))))) . t by A25, FUNCT_4:11
.= g1 . (2 * t9) by A12, A25, A26 ;
hence f . t = g1 . (2 * t9) ; ::_thesis: verum
end;
supposeA29: t9 = 1 / 2 ; ::_thesis: f . t = g1 . (2 * t9)
1 / 2 in { r where r is Real : ( 1 / 2 <= r & r <= 1 ) } ;
then 1 / 2 in [.(1 / 2),1.] by RCOMP_1:def_1;
then 1 / 2 in the carrier of (Closed-Interval-TSpace ((1 / 2),1)) by TOPMETR:18;
then t in dom (g2 * (P[01] ((1 / 2),1,((#) (0,1)),((0,1) (#))))) by A25, A29, FUNCT_2:def_1, TOPMETR:20;
then f . t = (g2 * (P[01] ((1 / 2),1,((#) (0,1)),((0,1) (#))))) . (1 / 2) by A25, A29, FUNCT_4:13
.= g1 . (2 * t9) by A12, A15, A29 ;
hence f . t = g1 . (2 * t9) ; ::_thesis: verum
end;
end;
end;
thus ( 1 / 2 <= t9 & t9 <= 1 implies f . t = g2 . ((2 * t9) - 1) ) ::_thesis: verum
proof
assume A30: ( 1 / 2 <= t9 & t9 <= 1 ) ; ::_thesis: f . t = g2 . ((2 * t9) - 1)
then t9 in { r where r is Real : ( 1 / 2 <= r & r <= 1 ) } ;
then t9 in [.(1 / 2),1.] by RCOMP_1:def_1;
then f . t = (g2 * (P[01] ((1 / 2),1,((#) (0,1)),((0,1) (#))))) . t by A8, A19, A25, FUNCT_4:13
.= g2 . ((2 * t9) - 1) by A9, A25, A30 ;
hence f . t = g2 . ((2 * t9) - 1) ; ::_thesis: verum
end;
end;
hence ex P0 being Path of w1,w3 st
( P0 is continuous & P0 . 0 = w1 & P0 . 1 = w3 & ( for t being Point of I[01]
for t9 being Real st t = t9 holds
( ( 0 <= t9 & t9 <= 1 / 2 implies P0 . t = g1 . (2 * t9) ) & ( 1 / 2 <= t9 & t9 <= 1 implies P0 . t = g2 . ((2 * t9) - 1) ) ) ) ) by A20, A24; ::_thesis: verum
end;
then consider P0 being Path of w1,w3 such that
A31: ( P0 is continuous & P0 . 0 = w1 & P0 . 1 = w3 ) and
A32: for t being Point of I[01]
for t9 being Real st t = t9 holds
( ( 0 <= t9 & t9 <= 1 / 2 implies P0 . t = g1 . (2 * t9) ) & ( 1 / 2 <= t9 & t9 <= 1 implies P0 . t = g2 . ((2 * t9) - 1) ) ) ;
rng P0 c= (rng g1) \/ (rng g2)
proof
A33: dom g2 = the carrier of I[01] by FUNCT_2:def_1;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng P0 or x in (rng g1) \/ (rng g2) )
A34: dom g1 = the carrier of I[01] by FUNCT_2:def_1;
assume x in rng P0 ; ::_thesis: x in (rng g1) \/ (rng g2)
then consider z being set such that
A35: z in dom P0 and
A36: x = P0 . z by FUNCT_1:def_3;
dom P0 = the carrier of I[01] by FUNCT_2:def_1;
then reconsider r = z as Real by A35, BORSUK_1:40;
A37: 0 <= r by A35, BORSUK_1:40, XXREAL_1:1;
A38: r <= 1 by A35, BORSUK_1:40, XXREAL_1:1;
percases ( r <= 1 / 2 or r > 1 / 2 ) ;
supposeA39: r <= 1 / 2 ; ::_thesis: x in (rng g1) \/ (rng g2)
then A40: 2 * r <= 2 * (1 / 2) by XREAL_1:64;
0 <= 2 * r by A37, XREAL_1:127;
then A41: 2 * r in the carrier of I[01] by A40, BORSUK_1:40, XXREAL_1:1;
P0 . z = g1 . (2 * r) by A32, A35, A37, A39;
then P0 . z in rng g1 by A34, A41, FUNCT_1:def_3;
hence x in (rng g1) \/ (rng g2) by A36, XBOOLE_0:def_3; ::_thesis: verum
end;
supposeA42: r > 1 / 2 ; ::_thesis: x in (rng g1) \/ (rng g2)
2 * r <= 2 * 1 by A38, XREAL_1:64;
then 2 * r <= 1 + 1 ;
then A43: (2 * r) - 1 <= 1 by XREAL_1:20;
2 * (1 / 2) = 1 ;
then 0 + 1 <= 2 * r by A42, XREAL_1:64;
then 0 <= (2 * r) - 1 by XREAL_1:19;
then A44: (2 * r) - 1 in the carrier of I[01] by A43, BORSUK_1:40, XXREAL_1:1;
P0 . z = g2 . ((2 * r) - 1) by A32, A35, A38, A42;
then P0 . z in rng g2 by A33, A44, FUNCT_1:def_3;
hence x in (rng g1) \/ (rng g2) by A36, XBOOLE_0:def_3; ::_thesis: verum
end;
end;
end;
hence 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 A31; ::_thesis: verum
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
B1: a,b are_connected and
B2: b,c are_connected ;
funcP + 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
1 / 2 in { r where r is Real : ( 0 <= r & r <= 1 ) } ;
then reconsider pol = 1 / 2 as Point of I[01] by BORSUK_1:40, RCOMP_1:def_1;
reconsider T1 = Closed-Interval-TSpace (0,(1 / 2)), T2 = Closed-Interval-TSpace ((1 / 2),1) as SubSpace of I[01] by TOPMETR:20, TREAL_1:3;
set e2 = P[01] ((1 / 2),1,((#) (0,1)),((0,1) (#)));
set e1 = P[01] (0,(1 / 2),((#) (0,1)),((0,1) (#)));
set E1 = P * (P[01] (0,(1 / 2),((#) (0,1)),((0,1) (#))));
set E2 = Q * (P[01] ((1 / 2),1,((#) (0,1)),((0,1) (#))));
set f = (P * (P[01] (0,(1 / 2),((#) (0,1)),((0,1) (#))))) +* (Q * (P[01] ((1 / 2),1,((#) (0,1)),((0,1) (#)))));
A1: dom (P[01] (0,(1 / 2),((#) (0,1)),((0,1) (#)))) = the carrier of (Closed-Interval-TSpace (0,(1 / 2))) by FUNCT_2:def_1
.= [.0,(1 / 2).] by TOPMETR:18 ;
A2: dom (P[01] ((1 / 2),1,((#) (0,1)),((0,1) (#)))) = the carrier of (Closed-Interval-TSpace ((1 / 2),1)) by FUNCT_2:def_1
.= [.(1 / 2),1.] by TOPMETR:18 ;
A3: for t9 being Real st 1 / 2 <= t9 & t9 <= 1 holds
(Q * (P[01] ((1 / 2),1,((#) (0,1)),((0,1) (#))))) . t9 = Q . ((2 * t9) - 1)
proof
reconsider r1 = (#) (0,1), r2 = (0,1) (#) as Real by TREAL_1:5;
dom (P[01] ((1 / 2),1,((#) (0,1)),((0,1) (#)))) = the carrier of (Closed-Interval-TSpace ((1 / 2),1)) by FUNCT_2:def_1;
then A4: dom (P[01] ((1 / 2),1,((#) (0,1)),((0,1) (#)))) = [.(1 / 2),1.] by TOPMETR:18
.= { r where r is Real : ( 1 / 2 <= r & r <= 1 ) } by RCOMP_1:def_1 ;
let t9 be Real; ::_thesis: ( 1 / 2 <= t9 & t9 <= 1 implies (Q * (P[01] ((1 / 2),1,((#) (0,1)),((0,1) (#))))) . t9 = Q . ((2 * t9) - 1) )
assume ( 1 / 2 <= t9 & t9 <= 1 ) ; ::_thesis: (Q * (P[01] ((1 / 2),1,((#) (0,1)),((0,1) (#))))) . t9 = Q . ((2 * t9) - 1)
then A5: t9 in dom (P[01] ((1 / 2),1,((#) (0,1)),((0,1) (#)))) by A4;
then reconsider s = t9 as Point of (Closed-Interval-TSpace ((1 / 2),1)) ;
(P[01] ((1 / 2),1,((#) (0,1)),((0,1) (#)))) . s = (((r2 - r1) / (1 - (1 / 2))) * t9) + (((1 * r1) - ((1 / 2) * r2)) / (1 - (1 / 2))) by TREAL_1:11
.= (2 * t9) - 1 by TREAL_1:5 ;
hence (Q * (P[01] ((1 / 2),1,((#) (0,1)),((0,1) (#))))) . t9 = Q . ((2 * t9) - 1) by A5, FUNCT_1:13; ::_thesis: verum
end;
reconsider gg = Q * (P[01] ((1 / 2),1,((#) (0,1)),((0,1) (#)))) as Function of T2,T by TOPMETR:20;
reconsider ff = P * (P[01] (0,(1 / 2),((#) (0,1)),((0,1) (#)))) as Function of T1,T by TOPMETR:20;
A6: ( P[01] (0,(1 / 2),((#) (0,1)),((0,1) (#))) is continuous Function of (Closed-Interval-TSpace (0,(1 / 2))),(Closed-Interval-TSpace (0,1)) & P[01] ((1 / 2),1,((#) (0,1)),((0,1) (#))) is continuous ) by TREAL_1:12;
rng ((P * (P[01] (0,(1 / 2),((#) (0,1)),((0,1) (#))))) +* (Q * (P[01] ((1 / 2),1,((#) (0,1)),((0,1) (#)))))) c= (rng (P * (P[01] (0,(1 / 2),((#) (0,1)),((0,1) (#)))))) \/ (rng (Q * (P[01] ((1 / 2),1,((#) (0,1)),((0,1) (#)))))) by FUNCT_4:17;
then A7: rng ((P * (P[01] (0,(1 / 2),((#) (0,1)),((0,1) (#))))) +* (Q * (P[01] ((1 / 2),1,((#) (0,1)),((0,1) (#)))))) c= the carrier of T by XBOOLE_1:1;
A8: ( R^1 is T_2 & T1 is compact ) by HEINE:4, PCOMPS_1:34, TOPMETR:def_6;
A9: for t9 being Real st 0 <= t9 & t9 <= 1 / 2 holds
(P * (P[01] (0,(1 / 2),((#) (0,1)),((0,1) (#))))) . t9 = P . (2 * t9)
proof
reconsider r1 = (#) (0,1), r2 = (0,1) (#) as Real by TREAL_1:5;
dom (P[01] (0,(1 / 2),((#) (0,1)),((0,1) (#)))) = the carrier of (Closed-Interval-TSpace (0,(1 / 2))) by FUNCT_2:def_1;
then A10: dom (P[01] (0,(1 / 2),((#) (0,1)),((0,1) (#)))) = [.0,(1 / 2).] by TOPMETR:18
.= { r where r is Real : ( 0 <= r & r <= 1 / 2 ) } by RCOMP_1:def_1 ;
let t9 be Real; ::_thesis: ( 0 <= t9 & t9 <= 1 / 2 implies (P * (P[01] (0,(1 / 2),((#) (0,1)),((0,1) (#))))) . t9 = P . (2 * t9) )
assume ( 0 <= t9 & t9 <= 1 / 2 ) ; ::_thesis: (P * (P[01] (0,(1 / 2),((#) (0,1)),((0,1) (#))))) . t9 = P . (2 * t9)
then A11: t9 in dom (P[01] (0,(1 / 2),((#) (0,1)),((0,1) (#)))) by A10;
then reconsider s = t9 as Point of (Closed-Interval-TSpace (0,(1 / 2))) ;
(P[01] (0,(1 / 2),((#) (0,1)),((0,1) (#)))) . s = (((r2 - r1) / ((1 / 2) - 0)) * t9) + ((((1 / 2) * r1) - (0 * r2)) / (1 / 2)) by TREAL_1:11
.= 2 * t9 by TREAL_1:5 ;
hence (P * (P[01] (0,(1 / 2),((#) (0,1)),((0,1) (#))))) . t9 = P . (2 * t9) by A11, FUNCT_1:13; ::_thesis: verum
end;
then A12: ff . (1 / 2) = P . (2 * (1 / 2))
.= b by B1, Def2
.= Q . ((2 * (1 / 2)) - 1) by B2, Def2
.= gg . pol by A3 ;
dom P = the carrier of I[01] by FUNCT_2:def_1;
then A13: rng (P[01] (0,(1 / 2),((#) (0,1)),((0,1) (#)))) c= dom P by TOPMETR:20;
( dom Q = the carrier of I[01] & rng (P[01] ((1 / 2),1,((#) (0,1)),((0,1) (#)))) c= the carrier of (Closed-Interval-TSpace (0,1)) ) by FUNCT_2:def_1;
then A14: dom (Q * (P[01] ((1 / 2),1,((#) (0,1)),((0,1) (#))))) = dom (P[01] ((1 / 2),1,((#) (0,1)),((0,1) (#)))) by RELAT_1:27, TOPMETR:20;
not 0 in { r where r is Real : ( 1 / 2 <= r & r <= 1 ) }
proof
assume 0 in { r where r is Real : ( 1 / 2 <= r & r <= 1 ) } ; ::_thesis: contradiction
then ex rr being Real st
( rr = 0 & 1 / 2 <= rr & rr <= 1 ) ;
hence contradiction ; ::_thesis: verum
end;
then not 0 in dom (Q * (P[01] ((1 / 2),1,((#) (0,1)),((0,1) (#))))) by A2, A14, RCOMP_1:def_1;
then A15: ((P * (P[01] (0,(1 / 2),((#) (0,1)),((0,1) (#))))) +* (Q * (P[01] ((1 / 2),1,((#) (0,1)),((0,1) (#)))))) . 0 = (P * (P[01] (0,(1 / 2),((#) (0,1)),((0,1) (#))))) . 0 by FUNCT_4:11
.= P . (2 * 0) by A9
.= a by B1, Def2 ;
A16: dom ((P * (P[01] (0,(1 / 2),((#) (0,1)),((0,1) (#))))) +* (Q * (P[01] ((1 / 2),1,((#) (0,1)),((0,1) (#)))))) = (dom (P * (P[01] (0,(1 / 2),((#) (0,1)),((0,1) (#)))))) \/ (dom (Q * (P[01] ((1 / 2),1,((#) (0,1)),((0,1) (#)))))) by FUNCT_4:def_1
.= [.0,(1 / 2).] \/ [.(1 / 2),1.] by A1, A2, A13, A14, RELAT_1:27
.= the carrier of I[01] by BORSUK_1:40, XXREAL_1:174 ;
( [#] T1 = [.0,(1 / 2).] & [#] T2 = [.(1 / 2),1.] ) by TOPMETR:18;
then A17: ( ([#] T1) \/ ([#] T2) = [#] I[01] & ([#] T1) /\ ([#] T2) = {pol} ) by BORSUK_1:40, XXREAL_1:174, XXREAL_1:418;
A18: T2 is compact by HEINE:4;
reconsider f = (P * (P[01] (0,(1 / 2),((#) (0,1)),((0,1) (#))))) +* (Q * (P[01] ((1 / 2),1,((#) (0,1)),((0,1) (#))))) as Function of I[01],T by A16, A7, FUNCT_2:def_1, RELSET_1:4;
( P is continuous & Q is continuous ) by B1, B2, Def2;
then reconsider f = f as continuous Function of I[01],T by A6, A12, A17, A8, A18, COMPTS_1:20, TOPMETR:20;
1 in { r where r is Real : ( 1 / 2 <= r & r <= 1 ) } ;
then 1 in dom (Q * (P[01] ((1 / 2),1,((#) (0,1)),((0,1) (#))))) by A2, A14, RCOMP_1:def_1;
then A19: f . 1 = (Q * (P[01] ((1 / 2),1,((#) (0,1)),((0,1) (#))))) . 1 by FUNCT_4:13
.= Q . ((2 * 1) - 1) by A3
.= c by B2, Def2 ;
then a,c are_connected by A15, Def1;
then reconsider f = f as Path of a,c by A15, A19, Def2;
for t being Point of I[01] holds
( ( t <= 1 / 2 implies f . t = P . (2 * t) ) & ( 1 / 2 <= t implies f . t = Q . ((2 * t) - 1) ) )
proof
let t be Point of I[01]; ::_thesis: ( ( t <= 1 / 2 implies f . t = P . (2 * t) ) & ( 1 / 2 <= t implies f . t = Q . ((2 * t) - 1) ) )
A20: t is Real by XREAL_0:def_1;
A21: 0 <= t by Lm1;
thus ( t <= 1 / 2 implies f . t = P . (2 * t) ) ::_thesis: ( 1 / 2 <= t implies f . t = Q . ((2 * t) - 1) )
proof
assume A22: t <= 1 / 2 ; ::_thesis: f . t = P . (2 * t)
then t in { r where r is Real : ( 0 <= r & r <= 1 / 2 ) } by A21, A20;
then A23: t in [.0,(1 / 2).] by RCOMP_1:def_1;
percases ( t <> 1 / 2 or t = 1 / 2 ) ;
supposeA24: t <> 1 / 2 ; ::_thesis: f . t = P . (2 * t)
not t in dom (Q * (P[01] ((1 / 2),1,((#) (0,1)),((0,1) (#)))))
proof
assume t in dom (Q * (P[01] ((1 / 2),1,((#) (0,1)),((0,1) (#))))) ; ::_thesis: contradiction
then t in [.0,(1 / 2).] /\ [.(1 / 2),1.] by A2, A14, A23, XBOOLE_0:def_4;
then t in {(1 / 2)} by XXREAL_1:418;
hence contradiction by A24, TARSKI:def_1; ::_thesis: verum
end;
then f . t = (P * (P[01] (0,(1 / 2),((#) (0,1)),((0,1) (#))))) . t by FUNCT_4:11
.= P . (2 * t) by A9, A21, A20, A22 ;
hence f . t = P . (2 * t) ; ::_thesis: verum
end;
supposeA25: t = 1 / 2 ; ::_thesis: f . t = P . (2 * t)
1 / 2 in { r where r is Real : ( 1 / 2 <= r & r <= 1 ) } ;
then 1 / 2 in [.(1 / 2),1.] by RCOMP_1:def_1;
then 1 / 2 in the carrier of (Closed-Interval-TSpace ((1 / 2),1)) by TOPMETR:18;
then t in dom (Q * (P[01] ((1 / 2),1,((#) (0,1)),((0,1) (#))))) by A25, FUNCT_2:def_1, TOPMETR:20;
then f . t = (P * (P[01] (0,(1 / 2),((#) (0,1)),((0,1) (#))))) . t by A12, A25, FUNCT_4:13
.= P . (2 * t) by A9, A21, A20, A22 ;
hence f . t = P . (2 * t) ; ::_thesis: verum
end;
end;
end;
A26: t <= 1 by Lm1;
thus ( 1 / 2 <= t implies f . t = Q . ((2 * t) - 1) ) ::_thesis: verum
proof
assume A27: 1 / 2 <= t ; ::_thesis: f . t = Q . ((2 * t) - 1)
then t in { r where r is Real : ( 1 / 2 <= r & r <= 1 ) } by A26, A20;
then t in [.(1 / 2),1.] by RCOMP_1:def_1;
then f . t = (Q * (P[01] ((1 / 2),1,((#) (0,1)),((0,1) (#))))) . t by A2, A14, FUNCT_4:13
.= Q . ((2 * t) - 1) by A3, A26, A20, A27 ;
hence f . t = Q . ((2 * t) - 1) ; ::_thesis: verum
end;
end;
hence 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) ) ) ; ::_thesis: verum
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
let A, B be Path of a,c; ::_thesis: ( ( for t being Point of I[01] holds
( ( t <= 1 / 2 implies A . t = P . (2 * t) ) & ( 1 / 2 <= t implies A . 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) ) ) ) implies A = B )
assume that
A28: for t being Point of I[01] holds
( ( t <= 1 / 2 implies A . t = P . (2 * t) ) & ( 1 / 2 <= t implies A . t = Q . ((2 * t) - 1) ) ) and
A29: 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) ) ) ; ::_thesis: A = B
A30: for x being set st x in dom A holds
A . x = B . x
proof
let x be set ; ::_thesis: ( x in dom A implies A . x = B . x )
assume A31: x in dom A ; ::_thesis: A . x = B . x
then reconsider y = x as Point of I[01] ;
x in the carrier of I[01] by A31;
then x in { r where r is Real : ( 0 <= r & r <= 1 ) } by BORSUK_1:40, RCOMP_1:def_1;
then consider r9 being Real such that
A32: r9 = x and
0 <= r9 and
r9 <= 1 ;
percases ( r9 <= 1 / 2 or 1 / 2 < r9 ) ;
supposeA33: r9 <= 1 / 2 ; ::_thesis: A . x = B . x
then A . y = P . (2 * r9) by A28, A32
.= B . y by A29, A32, A33 ;
hence A . x = B . x ; ::_thesis: verum
end;
supposeA34: 1 / 2 < r9 ; ::_thesis: A . x = B . x
then A . y = Q . ((2 * r9) - 1) by A28, A32
.= B . y by A29, A32, A34 ;
hence A . x = B . x ; ::_thesis: verum
end;
end;
end;
dom B = the carrier of I[01] by FUNCT_2:def_1;
then dom A = dom B by FUNCT_2:def_1;
hence A = B by A30, FUNCT_1:2; ::_thesis: verum
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
set IT = I[01] --> a;
A1: ( (I[01] --> a) . 0 = a & (I[01] --> a) . 1 = a ) by BORSUK_1:def_14, BORSUK_1:def_15, FUNCOP_1:7;
a,a are_connected ;
then reconsider IT = I[01] --> a as Path of a,a by A1, Def2;
for n1, n2 being set st n1 in dom IT & n2 in dom IT holds
IT . n1 = IT . n2
proof
let n1, n2 be set ; ::_thesis: ( n1 in dom IT & n2 in dom IT implies IT . n1 = IT . n2 )
assume that
A2: n1 in dom IT and
A3: n2 in dom IT ; ::_thesis: IT . n1 = IT . n2
IT . n1 = a by A2, FUNCOP_1:7
.= IT . n2 by A3, FUNCOP_1:7 ;
hence IT . n1 = IT . n2 ; ::_thesis: verum
end;
then IT is constant by FUNCT_1:def_10;
hence ex b1 being Path of a,a st b1 is constant ; ::_thesis: verum
end;
end;
theorem :: BORSUK_2:4
canceled;
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
let T be non empty TopSpace; ::_thesis: for a being Point of T
for P being constant Path of a,a holds P = I[01] --> a
let a be Point of T; ::_thesis: for P being constant Path of a,a holds P = I[01] --> a
let P be constant Path of a,a; ::_thesis: P = I[01] --> a
set IT = I[01] --> a;
A1: dom P = the carrier of I[01] by FUNCT_2:def_1;
A2: a,a are_connected ;
A3: for x being set st x in the carrier of I[01] holds
P . x = (I[01] --> a) . x
proof
0 in { r where r is Real : ( 0 <= r & r <= 1 ) } ;
then A4: 0 in the carrier of I[01] by BORSUK_1:40, RCOMP_1:def_1;
let x be set ; ::_thesis: ( x in the carrier of I[01] implies P . x = (I[01] --> a) . x )
assume A5: x in the carrier of I[01] ; ::_thesis: P . x = (I[01] --> a) . x
P . 0 = a by A2, Def2;
then P . x = a by A1, A5, A4, FUNCT_1:def_10
.= (I[01] --> a) . x by A5, FUNCOP_1:7 ;
hence P . x = (I[01] --> a) . x ; ::_thesis: verum
end;
dom (I[01] --> a) = the carrier of I[01] by FUNCT_2:def_1;
hence P = I[01] --> a by A1, A3, FUNCT_1:2; ::_thesis: verum
end;
theorem Th6: :: 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
let T be non empty TopSpace; ::_thesis: for a being Point of T
for P being constant Path of a,a holds P + P = P
let a be Point of T; ::_thesis: for P being constant Path of a,a holds P + P = P
let P be constant Path of a,a; ::_thesis: P + P = P
A1: the carrier of I[01] = dom P by FUNCT_2:def_1;
A2: for x being set st x in the carrier of I[01] holds
P . x = (P + P) . x
proof
let x be set ; ::_thesis: ( x in the carrier of I[01] implies P . x = (P + P) . x )
assume A3: x in the carrier of I[01] ; ::_thesis: P . x = (P + P) . x
then reconsider p = x as Point of I[01] ;
x in { r where r is Real : ( 0 <= r & r <= 1 ) } by A3, BORSUK_1:40, RCOMP_1:def_1;
then consider r being Real such that
A4: r = x and
A5: 0 <= r and
A6: r <= 1 ;
percases ( r < 1 / 2 or r >= 1 / 2 ) ;
supposeA7: r < 1 / 2 ; ::_thesis: P . x = (P + P) . x
then A8: r * 2 < (1 / 2) * 2 by XREAL_1:68;
2 * r >= 0 by A5, XREAL_1:127;
then 2 * r in { e where e is Real : ( 0 <= e & e <= 1 ) } by A8;
then 2 * r in the carrier of I[01] by BORSUK_1:40, RCOMP_1:def_1;
then P . (2 * r) = P . p by A1, FUNCT_1:def_10;
hence P . x = (P + P) . x by A4, A7, Def5; ::_thesis: verum
end;
supposeA9: r >= 1 / 2 ; ::_thesis: P . x = (P + P) . x
then r * 2 >= (1 / 2) * 2 by XREAL_1:64;
then 2 * r >= 1 + 0 ;
then A10: (2 * r) - 1 >= 0 by XREAL_1:19;
r * 2 <= 1 * 2 by A6, XREAL_1:64;
then (2 * r) - 1 <= 2 - 1 by XREAL_1:13;
then (2 * r) - 1 in { e where e is Real : ( 0 <= e & e <= 1 ) } by A10;
then (2 * r) - 1 in the carrier of I[01] by BORSUK_1:40, RCOMP_1:def_1;
then P . ((2 * r) - 1) = P . p by A1, FUNCT_1:def_10;
hence P . x = (P + P) . x by A4, A9, Def5; ::_thesis: verum
end;
end;
end;
dom (P + P) = the carrier of I[01] by FUNCT_2:def_1;
hence P + P = P by A1, A2, FUNCT_1:2; ::_thesis: verum
end;
registration
let T be non empty TopSpace;
let a be Point of T;
let P be constant Path of a,a;
clusterP + P -> constant ;
coherence
P + P is constant by Th6;
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
set e = L[01] (((0,1) (#)),((#) (0,1)));
reconsider f = P * (L[01] (((0,1) (#)),((#) (0,1)))) as Function of I[01],T by TOPMETR:20;
A2: for t being Point of I[01] holds f . t = P . (1 - t)
proof
let t be Point of I[01]; ::_thesis: f . t = P . (1 - t)
reconsider ee = t as Point of (Closed-Interval-TSpace (0,1)) by TOPMETR:20;
A3: ( (0,1) (#) = 1 & (#) (0,1) = 0 ) by TREAL_1:def_1, TREAL_1:def_2;
t in the carrier of (Closed-Interval-TSpace (0,1)) by TOPMETR:20;
then t in dom (L[01] (((0,1) (#)),((#) (0,1)))) by FUNCT_2:def_1;
then f . t = P . ((L[01] (((0,1) (#)),((#) (0,1)))) . ee) by FUNCT_1:13
.= P . (((0 - 1) * t) + 1) by A3, TREAL_1:7
.= P . (1 - (1 * t)) ;
hence f . t = P . (1 - t) ; ::_thesis: verum
end;
0 in { r where r is Real : ( 0 <= r & r <= 1 ) } ;
then 0 in [.0,1.] by RCOMP_1:def_1;
then 0 in the carrier of (Closed-Interval-TSpace (0,1)) by TOPMETR:18;
then A4: 0 in dom (L[01] (((0,1) (#)),((#) (0,1)))) by FUNCT_2:def_1;
(L[01] (((0,1) (#)),((#) (0,1)))) . 0 = (L[01] (((0,1) (#)),((#) (0,1)))) . ((#) (0,1)) by TREAL_1:def_1
.= (0,1) (#) by TREAL_1:9
.= 1 by TREAL_1:def_2 ;
then A5: f . 0 = P . 1 by A4, FUNCT_1:13
.= b by A1, Def2 ;
1 in { r where r is Real : ( 0 <= r & r <= 1 ) } ;
then 1 in [.0,1.] by RCOMP_1:def_1;
then 1 in the carrier of (Closed-Interval-TSpace (0,1)) by TOPMETR:18;
then A6: 1 in dom (L[01] (((0,1) (#)),((#) (0,1)))) by FUNCT_2:def_1;
(L[01] (((0,1) (#)),((#) (0,1)))) . 1 = (L[01] (((0,1) (#)),((#) (0,1)))) . ((0,1) (#)) by TREAL_1:def_2
.= (#) (0,1) by TREAL_1:9
.= 0 by TREAL_1:def_1 ;
then A7: f . 1 = P . 0 by A6, FUNCT_1:13
.= a by A1, Def2 ;
A8: ( P is continuous & L[01] (((0,1) (#)),((#) (0,1))) is continuous Function of (Closed-Interval-TSpace (0,1)),(Closed-Interval-TSpace (0,1)) ) by A1, Def2, TREAL_1:8;
then b,a are_connected by A5, A7, Def1, TOPMETR:20;
then reconsider f = f as Path of b,a by A5, A7, A8, Def2, TOPMETR:20;
take f ; ::_thesis: for t being Point of I[01] holds f . t = P . (1 - t)
thus for t being Point of I[01] holds f . t = P . (1 - t) by A2; ::_thesis: verum
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
let R, Q be Path of b,a; ::_thesis: ( ( for t being Point of I[01] holds R . t = P . (1 - t) ) & ( for t being Point of I[01] holds Q . t = P . (1 - t) ) implies R = Q )
assume that
A9: for t being Point of I[01] holds R . t = P . (1 - t) and
A10: for t being Point of I[01] holds Q . t = P . (1 - t) ; ::_thesis: R = Q
A11: for x being set st x in the carrier of I[01] holds
R . x = Q . x
proof
let x be set ; ::_thesis: ( x in the carrier of I[01] implies R . x = Q . x )
assume x in the carrier of I[01] ; ::_thesis: R . x = Q . x
then reconsider x9 = x as Point of I[01] ;
R . x9 = P . (1 - x9) by A9
.= Q . x9 by A10 ;
hence R . x = Q . x ; ::_thesis: verum
end;
( dom R = the carrier of I[01] & the carrier of I[01] = dom Q ) by FUNCT_2:def_1;
hence R = Q by A11, FUNCT_1:2; ::_thesis: verum
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
let r be Real; ::_thesis: ( 0 <= r & r <= 1 implies ( 0 <= 1 - r & 1 - r <= 1 ) )
assume ( 0 <= r & r <= 1 ) ; ::_thesis: ( 0 <= 1 - r & 1 - r <= 1 )
then ( 1 - 1 <= 1 - r & 1 - r <= 1 - 0 ) by XREAL_1:13;
hence ( 0 <= 1 - r & 1 - r <= 1 ) ; ::_thesis: verum
end;
Lm5: for r being Real st r in the carrier of I[01] holds
1 - r in the carrier of I[01]
proof
let r be Real; ::_thesis: ( r in the carrier of I[01] implies 1 - r in the carrier of I[01] )
assume r in the carrier of I[01] ; ::_thesis: 1 - r in the carrier of I[01]
then ( 0 <= r & r <= 1 ) by Lm1;
then ( 0 <= 1 - r & 1 - r <= 1 ) by Lm4;
hence 1 - r in the carrier of I[01] by Lm1; ::_thesis: verum
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
proof
let T be non empty TopSpace; ::_thesis: for a being Point of T
for P being constant Path of a,a holds - P = P
let a be Point of T; ::_thesis: for P being constant Path of a,a holds - P = P
let P be constant Path of a,a; ::_thesis: - P = P
A1: dom P = the carrier of I[01] by FUNCT_2:def_1;
A2: for x being set st x in the carrier of I[01] holds
P . x = (- P) . x
proof
let x be set ; ::_thesis: ( x in the carrier of I[01] implies P . x = (- P) . x )
assume A3: x in the carrier of I[01] ; ::_thesis: P . x = (- P) . x
then reconsider x2 = x as Real by BORSUK_1:40;
reconsider x3 = 1 - x2 as Point of I[01] by A3, Lm5;
(- P) . x = P . x3 by A3, Def6
.= P . x by A1, A3, FUNCT_1:def_10 ;
hence P . x = (- P) . x ; ::_thesis: verum
end;
dom (- P) = the carrier of I[01] by FUNCT_2:def_1;
hence - P = P by A1, A2, FUNCT_1:2; ::_thesis: verum
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 Th7;
end;
begin
theorem Th8: :: 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
let X, Y be non empty TopSpace; ::_thesis: for A being Subset-Family of Y
for f being Function of X,Y holds f " (union A) = union (f " A)
let A be Subset-Family of Y; ::_thesis: for f being Function of X,Y holds f " (union A) = union (f " A)
let f be Function of X,Y; ::_thesis: f " (union A) = union (f " A)
thus f " (union A) c= union (f " A) :: according to XBOOLE_0:def_10 ::_thesis: union (f " A) c= f " (union A)
proof
reconsider uA = union A as Subset of Y ;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in f " (union A) or x in union (f " A) )
assume A1: x in f " (union A) ; ::_thesis: x in union (f " A)
then f . x in uA by FUNCT_2:38;
then consider YY being set such that
A2: f . x in YY and
A3: YY in A by TARSKI:def_4;
reconsider fY = f " YY as Subset of X ;
A4: fY in f " A by A3, FUNCT_2:def_9;
x in f " YY by A1, A2, FUNCT_2:38;
hence x in union (f " A) by A4, TARSKI:def_4; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in union (f " A) or x in f " (union A) )
assume x in union (f " A) ; ::_thesis: x in f " (union A)
then consider YY being set such that
A5: x in YY and
A6: YY in f " A by TARSKI:def_4;
x in the carrier of X by A5, A6;
then A7: x in dom f by FUNCT_2:def_1;
reconsider B1 = YY as Subset of X by A6;
consider B being Subset of Y such that
A8: B in A and
A9: B1 = f " B by A6, FUNCT_2:def_9;
f . x in B by A5, A9, FUNCT_1:def_7;
then f . x in union A by A8, TARSKI:def_4;
hence x in f " (union A) by A7, FUNCT_1:def_7; ::_thesis: verum
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
set h = [:f,g:];
rng [:f,g:] c= [: the carrier of S2, the carrier of T2:] ;
then A1: rng [:f,g:] c= the carrier of [:S2,T2:] by BORSUK_1:def_2;
dom [:f,g:] = [: the carrier of S1, the carrier of T1:] by FUNCT_2:def_1
.= the carrier of [:S1,T1:] by BORSUK_1:def_2 ;
hence [:f,g:] is Function of [:S1,T1:],[:S2,T2:] by A1, FUNCT_2:def_1, RELSET_1:4; ::_thesis: verum
end;
end;
theorem Th9: :: 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
let S1, S2, T1, T2 be non empty TopSpace; ::_thesis: 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
let f be continuous Function of S1,T1; ::_thesis: 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
let g be continuous Function of S2,T2; ::_thesis: for P1, P2 being Subset of [:T1,T2:] st P2 in Base-Appr P1 holds
[:f,g:] " P2 is open
let P1, P2 be Subset of [:T1,T2:]; ::_thesis: ( P2 in Base-Appr P1 implies [:f,g:] " P2 is open )
assume P2 in Base-Appr P1 ; ::_thesis: [:f,g:] " P2 is open
then consider X11 being Subset of T1, Y11 being Subset of T2 such that
A1: P2 = [:X11,Y11:] and
[:X11,Y11:] c= P1 and
A2: X11 is open and
A3: Y11 is open ;
[#] T1 <> {} ;
then A4: f " X11 is open by A2, TOPS_2:43;
[#] T2 <> {} ;
then A5: g " Y11 is open by A3, TOPS_2:43;
[:f,g:] " P2 = [:(f " X11),(g " Y11):] by A1, FUNCT_3:73;
hence [:f,g:] " P2 is open by A4, A5, BORSUK_1:6; ::_thesis: verum
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 P2 being Subset of [:T1,T2:] st P2 is open holds
[:f,g:] " P2 is open
proof
let S1, S2, T1, T2 be non empty TopSpace; ::_thesis: 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
let f be continuous Function of S1,T1; ::_thesis: 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
let g be continuous Function of S2,T2; ::_thesis: for P2 being Subset of [:T1,T2:] st P2 is open holds
[:f,g:] " P2 is open
let P2 be Subset of [:T1,T2:]; ::_thesis: ( P2 is open implies [:f,g:] " P2 is open )
reconsider Kill = [:f,g:] " (Base-Appr P2) as Subset-Family of [:S1,S2:] ;
for P being Subset of [:S1,S2:] st P in Kill holds
P is open
proof
let P be Subset of [:S1,S2:]; ::_thesis: ( P in Kill implies P is open )
assume P in Kill ; ::_thesis: P is open
then ex B being Subset of [:T1,T2:] st
( B in Base-Appr P2 & P = [:f,g:] " B ) by FUNCT_2:def_9;
hence P is open by Th9; ::_thesis: verum
end;
then A1: Kill is open by TOPS_2:def_1;
assume P2 is open ; ::_thesis: [:f,g:] " P2 is open
then P2 = union (Base-Appr P2) by BORSUK_1:13;
then [:f,g:] " P2 = union ([:f,g:] " (Base-Appr P2)) by Th8;
hence [:f,g:] " P2 is open by A1, TOPS_2:19; ::_thesis: verum
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
( [#] [:T1,T2:] <> {} & ( for P1 being Subset of [:T1,T2:] st P1 is open holds
[:f,g:] " P1 is open ) ) by Th10;
hence for b1 being Function of [:S1,S2:],[:T1,T2:] st b1 = [:f,g:] holds
b1 is continuous by TOPS_2:43; ::_thesis: verum
end;
end;
registration
let T1, T2 be T_0 TopSpace;
cluster[:T1,T2:] -> T_0 ;
coherence
[:T1,T2:] is T_0
proof
set T = [:T1,T2:];
percases ( T1 is empty or T2 is empty or ( not T1 is empty & not T2 is empty ) ) ;
suppose ( T1 is empty or T2 is empty ) ; ::_thesis: [:T1,T2:] is T_0
hence [:T1,T2:] is T_0 ; ::_thesis: verum
end;
supposethat A1: not T1 is empty and
A2: not T2 is empty ; ::_thesis: [:T1,T2:] is T_0
A3: not the carrier of [:T1,T2:] is empty by A1, A2;
now__::_thesis:_for_p,_q_being_Point_of_[:T1,T2:]_st_p_<>_q_holds_
ex_X_being_Subset_of_[:T1,T2:]_st_
(_X_is_open_&_(_(_p_in_X_&_not_q_in_X_)_or_(_q_in_X_&_not_p_in_X_)_)_)
let p, q be Point of [:T1,T2:]; ::_thesis: ( p <> q implies ex X being Subset of [:T1,T2:] st
( b3 is open & ( ( X in b3 & not b2 in b3 ) or ( b2 in b3 & not X in b3 ) ) ) )
assume A4: p <> q ; ::_thesis: ex X being Subset of [:T1,T2:] st
( b3 is open & ( ( X in b3 & not b2 in b3 ) or ( b2 in b3 & not X in b3 ) ) )
q in the carrier of [:T1,T2:] by A3;
then q in [: the carrier of T1, the carrier of T2:] by BORSUK_1:def_2;
then consider z, v being set such that
A5: z in the carrier of T1 and
A6: v in the carrier of T2 and
A7: q = [z,v] by ZFMISC_1:def_2;
p in the carrier of [:T1,T2:] by A3;
then p in [: the carrier of T1, the carrier of T2:] by BORSUK_1:def_2;
then consider x, y being set such that
A8: x in the carrier of T1 and
A9: y in the carrier of T2 and
A10: p = [x,y] by ZFMISC_1:def_2;
reconsider y = y, v = v as Point of T2 by A9, A6;
reconsider x = x, z = z as Point of T1 by A8, A5;
percases ( x <> z or x = z ) ;
suppose x <> z ; ::_thesis: ex X being Subset of [:T1,T2:] st
( b3 is open & ( ( X in b3 & not b2 in b3 ) or ( b2 in b3 & not X in b3 ) ) )
then consider V1 being Subset of T1 such that
A11: V1 is open and
A12: ( ( x in V1 & not z in V1 ) or ( z in V1 & not x in V1 ) ) by T_0TOPSP:def_7, A1;
set X = [:V1,([#] T2):];
A13: now__::_thesis:_(_(_p_in_[:V1,([#]_T2):]_&_not_q_in_[:V1,([#]_T2):]_)_or_(_q_in_[:V1,([#]_T2):]_&_not_p_in_[:V1,([#]_T2):]_)_)
percases ( ( x in V1 & not z in V1 ) or ( z in V1 & not x in V1 ) ) by A12;
suppose ( x in V1 & not z in V1 ) ; ::_thesis: ( ( p in [:V1,([#] T2):] & not q in [:V1,([#] T2):] ) or ( q in [:V1,([#] T2):] & not p in [:V1,([#] T2):] ) )
hence ( ( p in [:V1,([#] T2):] & not q in [:V1,([#] T2):] ) or ( q in [:V1,([#] T2):] & not p in [:V1,([#] T2):] ) ) by A9, A10, A7, ZFMISC_1:87; ::_thesis: verum
end;
suppose ( z in V1 & not x in V1 ) ; ::_thesis: ( ( p in [:V1,([#] T2):] & not q in [:V1,([#] T2):] ) or ( q in [:V1,([#] T2):] & not p in [:V1,([#] T2):] ) )
hence ( ( p in [:V1,([#] T2):] & not q in [:V1,([#] T2):] ) or ( q in [:V1,([#] T2):] & not p in [:V1,([#] T2):] ) ) by A10, A6, A7, ZFMISC_1:87; ::_thesis: verum
end;
end;
end;
[:V1,([#] T2):] is open by A11, BORSUK_1:6;
hence ex X being Subset of [:T1,T2:] st
( X is open & ( ( p in X & not q in X ) or ( q in X & not p in X ) ) ) by A13; ::_thesis: verum
end;
suppose x = z ; ::_thesis: ex X being Subset of [:T1,T2:] st
( b3 is open & ( ( X in b3 & not b2 in b3 ) or ( b2 in b3 & not X in b3 ) ) )
then consider V1 being Subset of T2 such that
A14: V1 is open and
A15: ( ( y in V1 & not v in V1 ) or ( v in V1 & not y in V1 ) ) by A4, A10, A7, T_0TOPSP:def_7, A2;
set X = [:([#] T1),V1:];
A16: now__::_thesis:_(_(_p_in_[:([#]_T1),V1:]_&_not_q_in_[:([#]_T1),V1:]_)_or_(_q_in_[:([#]_T1),V1:]_&_not_p_in_[:([#]_T1),V1:]_)_)
percases ( ( y in V1 & not v in V1 ) or ( v in V1 & not y in V1 ) ) by A15;
suppose ( y in V1 & not v in V1 ) ; ::_thesis: ( ( p in [:([#] T1),V1:] & not q in [:([#] T1),V1:] ) or ( q in [:([#] T1),V1:] & not p in [:([#] T1),V1:] ) )
hence ( ( p in [:([#] T1),V1:] & not q in [:([#] T1),V1:] ) or ( q in [:([#] T1),V1:] & not p in [:([#] T1),V1:] ) ) by A8, A10, A7, ZFMISC_1:87; ::_thesis: verum
end;
suppose ( v in V1 & not y in V1 ) ; ::_thesis: ( ( p in [:([#] T1),V1:] & not q in [:([#] T1),V1:] ) or ( q in [:([#] T1),V1:] & not p in [:([#] T1),V1:] ) )
hence ( ( p in [:([#] T1),V1:] & not q in [:([#] T1),V1:] ) or ( q in [:([#] T1),V1:] & not p in [:([#] T1),V1:] ) ) by A10, A5, A7, ZFMISC_1:87; ::_thesis: verum
end;
end;
end;
[:([#] T1),V1:] is open by A14, BORSUK_1:6;
hence ex X being Subset of [:T1,T2:] st
( X is open & ( ( p in X & not q in X ) or ( q in X & not p in X ) ) ) by A16; ::_thesis: verum
end;
end;
end;
hence [:T1,T2:] is T_0 by T_0TOPSP:def_7; ::_thesis: verum
end;
end;
end;
end;
registration
let T1, T2 be T_1 TopSpace;
cluster[:T1,T2:] -> T_1 ;
coherence
[:T1,T2:] is T_1
proof
set T = [:T1,T2:];
percases ( T1 is empty or T2 is empty or ( not T1 is empty & not T2 is empty ) ) ;
suppose ( T1 is empty or T2 is empty ) ; ::_thesis: [:T1,T2:] is T_1
hence [:T1,T2:] is T_1 ; ::_thesis: verum
end;
suppose ( not T1 is empty & not T2 is empty ) ; ::_thesis: [:T1,T2:] is T_1
then A1: not the carrier of [:T1,T2:] is empty ;
let p, q be Point of [:T1,T2:]; :: according to URYSOHN1:def_7 ::_thesis: ( p = q or ex b1, b2 being Element of bool the carrier of [:T1,T2:] st
( b1 is open & b2 is open & p in b1 & not q in b1 & q in b2 & not p in b2 ) )
assume A2: p <> q ; ::_thesis: ex b1, b2 being Element of bool the carrier of [:T1,T2:] st
( b1 is open & b2 is open & p in b1 & not q in b1 & q in b2 & not p in b2 )
q in the carrier of [:T1,T2:] by A1;
then q in [: the carrier of T1, the carrier of T2:] by BORSUK_1:def_2;
then consider z, v being set such that
A3: z in the carrier of T1 and
A4: v in the carrier of T2 and
A5: q = [z,v] by ZFMISC_1:def_2;
p in the carrier of [:T1,T2:] by A1;
then p in [: the carrier of T1, the carrier of T2:] by BORSUK_1:def_2;
then consider x, y being set such that
A6: x in the carrier of T1 and
A7: y in the carrier of T2 and
A8: p = [x,y] by ZFMISC_1:def_2;
reconsider y = y, v = v as Point of T2 by A7, A4;
reconsider x = x, z = z as Point of T1 by A6, A3;
percases ( x <> z or x = z ) ;
suppose x <> z ; ::_thesis: ex b1, b2 being Element of bool the carrier of [:T1,T2:] st
( b1 is open & b2 is open & p in b1 & not q in b1 & q in b2 & not p in b2 )
then consider Y, V being Subset of T1 such that
A9: ( Y is open & V is open ) and
A10: x in Y and
A11: not z in Y and
A12: z in V and
A13: not x in V by URYSOHN1:def_7;
set X = [:Y,([#] T2):];
set Z = [:V,([#] T2):];
A14: ( not q in [:Y,([#] T2):] & not p in [:V,([#] T2):] ) by A8, A5, A11, A13, ZFMISC_1:87;
A15: ( [:Y,([#] T2):] is open & [:V,([#] T2):] is open ) by A9, BORSUK_1:6;
( p in [:Y,([#] T2):] & q in [:V,([#] T2):] ) by A7, A8, A4, A5, A10, A12, ZFMISC_1:87;
hence ex b1, b2 being Element of bool the carrier of [:T1,T2:] st
( b1 is open & b2 is open & p in b1 & not q in b1 & q in b2 & not p in b2 ) by A15, A14; ::_thesis: verum
end;
suppose x = z ; ::_thesis: ex b1, b2 being Element of bool the carrier of [:T1,T2:] st
( b1 is open & b2 is open & p in b1 & not q in b1 & q in b2 & not p in b2 )
then consider Y, V being Subset of T2 such that
A16: ( Y is open & V is open ) and
A17: y in Y and
A18: not v in Y and
A19: v in V and
A20: not y in V by A2, A8, A5, URYSOHN1:def_7;
reconsider Y = Y, V = V as Subset of T2 ;
set X = [:([#] T1),Y:];
set Z = [:([#] T1),V:];
A21: ( not p in [:([#] T1),V:] & not q in [:([#] T1),Y:] ) by A8, A5, A18, A20, ZFMISC_1:87;
A22: ( [:([#] T1),Y:] is open & [:([#] T1),V:] is open ) by A16, BORSUK_1:6;
( p in [:([#] T1),Y:] & q in [:([#] T1),V:] ) by A6, A8, A3, A5, A17, A19, ZFMISC_1:87;
hence ex b1, b2 being Element of bool the carrier of [:T1,T2:] st
( b1 is open & b2 is open & p in b1 & not q in b1 & q in b2 & not p in b2 ) by A22, A21; ::_thesis: verum
end;
end;
end;
end;
end;
end;
registration
let T1, T2 be T_2 TopSpace;
cluster[:T1,T2:] -> T_2 ;
coherence
[:T1,T2:] is T_2
proof
set T = [:T1,T2:];
percases ( T1 is empty or T2 is empty or ( not T1 is empty & not T2 is empty ) ) ;
suppose ( T1 is empty or T2 is empty ) ; ::_thesis: [:T1,T2:] is T_2
hence [:T1,T2:] is T_2 ; ::_thesis: verum
end;
suppose ( not T1 is empty & not T2 is empty ) ; ::_thesis: [:T1,T2:] is T_2
then A1: not the carrier of [:T1,T2:] is empty ;
let p, q be Point of [:T1,T2:]; :: according to PRE_TOPC:def_10 ::_thesis: ( p = q or ex b1, b2 being Element of bool the carrier of [:T1,T2:] st
( b1 is open & b2 is open & p in b1 & q in b2 & b1 misses b2 ) )
assume A2: p <> q ; ::_thesis: ex b1, b2 being Element of bool the carrier of [:T1,T2:] st
( b1 is open & b2 is open & p in b1 & q in b2 & b1 misses b2 )
q in the carrier of [:T1,T2:] by A1;
then q in [: the carrier of T1, the carrier of T2:] by BORSUK_1:def_2;
then consider z, v being set such that
A3: z in the carrier of T1 and
A4: v in the carrier of T2 and
A5: q = [z,v] by ZFMISC_1:def_2;
p in the carrier of [:T1,T2:] by A1;
then p in [: the carrier of T1, the carrier of T2:] by BORSUK_1:def_2;
then consider x, y being set such that
A6: x in the carrier of T1 and
A7: y in the carrier of T2 and
A8: p = [x,y] by ZFMISC_1:def_2;
reconsider y = y, v = v as Point of T2 by A7, A4;
reconsider x = x, z = z as Point of T1 by A6, A3;
percases ( x <> z or x = z ) ;
suppose x <> z ; ::_thesis: ex b1, b2 being Element of bool the carrier of [:T1,T2:] st
( b1 is open & b2 is open & p in b1 & q in b2 & b1 misses b2 )
then consider Y, V being Subset of T1 such that
A9: ( Y is open & V is open ) and
A10: ( x in Y & z in V ) and
A11: Y misses V by PRE_TOPC:def_10;
reconsider Y = Y, V = V as Subset of T1 ;
reconsider X = [:Y,([#] T2):], Z = [:V,([#] T2):] as Subset of [:T1,T2:] ;
A12: X misses Z by A11, ZFMISC_1:104;
A13: ( X is open & Z is open ) by A9, BORSUK_1:6;
( p in X & q in Z ) by A7, A8, A4, A5, A10, ZFMISC_1:87;
hence ex b1, b2 being Element of bool the carrier of [:T1,T2:] st
( b1 is open & b2 is open & p in b1 & q in b2 & b1 misses b2 ) by A13, A12; ::_thesis: verum
end;
suppose x = z ; ::_thesis: ex b1, b2 being Element of bool the carrier of [:T1,T2:] st
( b1 is open & b2 is open & p in b1 & q in b2 & b1 misses b2 )
then consider Y, V being Subset of T2 such that
A14: ( Y is open & V is open ) and
A15: ( y in Y & v in V ) and
A16: Y misses V by A2, A8, A5, PRE_TOPC:def_10;
reconsider Y = Y, V = V as Subset of T2 ;
reconsider X = [:([#] T1),Y:], Z = [:([#] T1),V:] as Subset of [:T1,T2:] ;
A17: X misses Z by A16, ZFMISC_1:104;
A18: ( X is open & Z is open ) by A14, BORSUK_1:6;
( p in X & q in Z ) by A6, A8, A3, A5, A15, ZFMISC_1:87;
hence ex b1, b2 being Element of bool the carrier of [:T1,T2:] st
( b1 is open & b2 is open & p in b1 & q in b2 & b1 misses b2 ) by A18, A17; ::_thesis: verum
end;
end;
end;
end;
end;
end;
registration
cluster I[01] -> T_2 compact ;
coherence
( I[01] is compact & I[01] is T_2 )
proof
I[01] = TopSpaceMetr (Closed-Interval-MSpace (0,1)) by TOPMETR:20, TOPMETR:def_7;
hence ( I[01] is compact & I[01] is T_2 ) by HEINE:4, PCOMPS_1:34, TOPMETR:20; ::_thesis: verum
end;
end;
definition
let T be non empty TopStruct ;
let a, b be Point of T;
let P, Q be Path of a,b;
predP,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
id the carrier of I[01] = id I[01] ;
then reconsider fA = id the carrier of I[01] as continuous Function of I[01],I[01] ;
set LL = L[01] (((0,1) (#)),((#) (0,1)));
reconsider fB = L[01] (((0,1) (#)),((#) (0,1))) as continuous Function of I[01],I[01] by TOPMETR:20, TREAL_1:8;
let P, Q be Path of a,b; ::_thesis: ( 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 ) ) ) implies 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 ) ) ) )
given f being Function of [:I[01],I[01]:],T such that A1: f is continuous and
A2: for s being Point of I[01] holds
( f . (s,0) = P . s & f . (s,1) = Q . s & f . (0,s) = a & f . (1,s) = b ) ; ::_thesis: 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 ) ) )
set F = [:fA,fB:];
reconsider ff = f * [:fA,fB:] as Function of [:I[01],I[01]:],T ;
A3: dom (L[01] (((0,1) (#)),((#) (0,1)))) = the carrier of I[01] by FUNCT_2:def_1, TOPMETR:20;
A4: for s being Point of I[01] holds
( ff . (s,0) = Q . s & ff . (s,1) = P . s )
proof
let s be Point of I[01]; ::_thesis: ( ff . (s,0) = Q . s & ff . (s,1) = P . s )
A5: for t being Point of I[01]
for t9 being Real st t = t9 holds
(L[01] (((0,1) (#)),((#) (0,1)))) . t = 1 - t9
proof
let t be Point of I[01]; ::_thesis: for t9 being Real st t = t9 holds
(L[01] (((0,1) (#)),((#) (0,1)))) . t = 1 - t9
let t9 be Real; ::_thesis: ( t = t9 implies (L[01] (((0,1) (#)),((#) (0,1)))) . t = 1 - t9 )
assume A6: t = t9 ; ::_thesis: (L[01] (((0,1) (#)),((#) (0,1)))) . t = 1 - t9
reconsider ee = t as Point of (Closed-Interval-TSpace (0,1)) by TOPMETR:20;
A7: ( (0,1) (#) = 1 & (#) (0,1) = 0 ) by TREAL_1:def_1, TREAL_1:def_2;
(L[01] (((0,1) (#)),((#) (0,1)))) . t = (L[01] (((0,1) (#)),((#) (0,1)))) . ee
.= ((0 - 1) * t9) + 1 by A6, A7, TREAL_1:7
.= 1 - (1 * t9) ;
hence (L[01] (((0,1) (#)),((#) (0,1)))) . t = 1 - t9 ; ::_thesis: verum
end;
A8: dom (id the carrier of I[01]) = the carrier of I[01] ;
A9: dom [:fA,fB:] = [:(dom (id the carrier of I[01])),(dom (L[01] (((0,1) (#)),((#) (0,1))))):] by FUNCT_3:def_8;
A10: 1 in dom (L[01] (((0,1) (#)),((#) (0,1)))) by A3, Lm1;
then A11: [s,1] in dom [:fA,fB:] by A9, ZFMISC_1:87;
A12: 0 in dom (L[01] (((0,1) (#)),((#) (0,1)))) by A3, Lm1;
then A13: [s,0] in dom [:fA,fB:] by A9, ZFMISC_1:87;
[:fA,fB:] . (s,1) = [((id the carrier of I[01]) . s),((L[01] (((0,1) (#)),((#) (0,1)))) . 1)] by A8, A10, FUNCT_3:def_8
.= [s,((L[01] (((0,1) (#)),((#) (0,1)))) . 1[01])] by FUNCT_1:18
.= [s,(1 - 1)] by A5
.= [s,0] ;
then A14: ff . (s,1) = f . (s,0) by A11, FUNCT_1:13
.= P . s by A2 ;
[:fA,fB:] . (s,0) = [((id the carrier of I[01]) . s),((L[01] (((0,1) (#)),((#) (0,1)))) . 0)] by A8, A12, FUNCT_3:def_8
.= [s,((L[01] (((0,1) (#)),((#) (0,1)))) . 0[01])] by FUNCT_1:18
.= [s,(1 - 0)] by A5
.= [s,1] ;
then ff . (s,0) = f . (s,1) by A13, FUNCT_1:13
.= Q . s by A2 ;
hence ( ff . (s,0) = Q . s & ff . (s,1) = P . s ) by A14; ::_thesis: verum
end;
A15: for t being Point of I[01] holds
( ff . (0,t) = a & ff . (1,t) = b )
proof
let t be Point of I[01]; ::_thesis: ( ff . (0,t) = a & ff . (1,t) = b )
t in the carrier of I[01] ;
then reconsider tt = t as Real by BORSUK_1:40;
for t being Point of I[01]
for t9 being Real st t = t9 holds
(L[01] (((0,1) (#)),((#) (0,1)))) . t = 1 - t9
proof
let t be Point of I[01]; ::_thesis: for t9 being Real st t = t9 holds
(L[01] (((0,1) (#)),((#) (0,1)))) . t = 1 - t9
let t9 be Real; ::_thesis: ( t = t9 implies (L[01] (((0,1) (#)),((#) (0,1)))) . t = 1 - t9 )
assume A16: t = t9 ; ::_thesis: (L[01] (((0,1) (#)),((#) (0,1)))) . t = 1 - t9
reconsider ee = t as Point of (Closed-Interval-TSpace (0,1)) by TOPMETR:20;
A17: ( (0,1) (#) = 1 & (#) (0,1) = 0 ) by TREAL_1:def_1, TREAL_1:def_2;
(L[01] (((0,1) (#)),((#) (0,1)))) . t = (L[01] (((0,1) (#)),((#) (0,1)))) . ee
.= ((0 - 1) * t9) + 1 by A16, A17, TREAL_1:7
.= 1 - (1 * t9) ;
hence (L[01] (((0,1) (#)),((#) (0,1)))) . t = 1 - t9 ; ::_thesis: verum
end;
then A18: (L[01] (((0,1) (#)),((#) (0,1)))) . t = 1 - tt ;
reconsider t9 = 1 - tt as Point of I[01] by Lm5;
A19: dom (L[01] (((0,1) (#)),((#) (0,1)))) = the carrier of I[01] by FUNCT_2:def_1, TOPMETR:20;
A20: 0 in dom (id the carrier of I[01]) by Lm1;
A21: dom [:fA,fB:] = [:(dom (id the carrier of I[01])),(dom (L[01] (((0,1) (#)),((#) (0,1))))):] by FUNCT_3:def_8;
then A22: [0,t] in dom [:fA,fB:] by A19, A20, ZFMISC_1:87;
A23: 1 in dom (id the carrier of I[01]) by Lm1;
then A24: [1,t] in dom [:fA,fB:] by A19, A21, ZFMISC_1:87;
[:fA,fB:] . (1,t) = [((id the carrier of I[01]) . 1),((L[01] (((0,1) (#)),((#) (0,1)))) . t)] by A19, A23, FUNCT_3:def_8
.= [1,(1 - tt)] by A18, A23, FUNCT_1:18 ;
then A25: ff . (1,t) = f . (1,t9) by A24, FUNCT_1:13
.= b by A2 ;
[:fA,fB:] . (0,t) = [((id the carrier of I[01]) . 0),((L[01] (((0,1) (#)),((#) (0,1)))) . t)] by A19, A20, FUNCT_3:def_8
.= [0,(1 - tt)] by A18, A20, FUNCT_1:18 ;
then ff . (0,t) = f . (0,t9) by A22, FUNCT_1:13
.= a by A2 ;
hence ( ff . (0,t) = a & ff . (1,t) = b ) by A25; ::_thesis: verum
end;
ff is continuous by A1, TOPS_2:46;
hence 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 ) ) ) by A4, A15; ::_thesis: verum
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;
theorem Th12: :: 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
let T be non empty TopSpace; ::_thesis: for a, b being Point of T
for P being Path of a,b st a,b are_connected holds
P,P are_homotopic
let a, b be Point of T; ::_thesis: for P being Path of a,b st a,b are_connected holds
P,P are_homotopic
let P be Path of a,b; ::_thesis: ( a,b are_connected implies P,P are_homotopic )
defpred S1[ set , set ] means $2 = P . ($1 `1);
A1: for x being set st x in [: the carrier of I[01], the carrier of I[01]:] holds
ex y being set st
( y in the carrier of T & S1[x,y] )
proof
let x be set ; ::_thesis: ( x in [: the carrier of I[01], the carrier of I[01]:] implies ex y being set st
( y in the carrier of T & S1[x,y] ) )
assume x in [: the carrier of I[01], the carrier of I[01]:] ; ::_thesis: ex y being set st
( y in the carrier of T & S1[x,y] )
then x `1 in the carrier of I[01] by MCART_1:10;
hence ex y being set st
( y in the carrier of T & S1[x,y] ) by FUNCT_2:5; ::_thesis: verum
end;
consider f being Function of [: the carrier of I[01], the carrier of I[01]:], the carrier of T such that
A2: for x being set st x in [: the carrier of I[01], the carrier of I[01]:] holds
S1[x,f . x] from FUNCT_2:sch_1(A1);
the carrier of [:I[01],I[01]:] = [: the carrier of I[01], the carrier of I[01]:] by BORSUK_1:def_2;
then reconsider f = f as Function of the carrier of [:I[01],I[01]:], the carrier of T ;
reconsider f = f as Function of [:I[01],I[01]:],T ;
assume A3: a,b are_connected ; ::_thesis: P,P are_homotopic
A4: for t being Point of I[01] holds
( f . (0,t) = a & f . (1,t) = b )
proof
let t be Point of I[01]; ::_thesis: ( f . (0,t) = a & f . (1,t) = b )
set t0 = [0,t];
set t1 = [1,t];
0 in the carrier of I[01] by Lm1;
then [0,t] in [: the carrier of I[01], the carrier of I[01]:] by ZFMISC_1:87;
then A5: f . [0,t] = P . ([0,t] `1) by A2;
1 in the carrier of I[01] by Lm1;
then [1,t] in [: the carrier of I[01], the carrier of I[01]:] by ZFMISC_1:87;
then A6: f . [1,t] = P . ([1,t] `1) by A2;
( P . 0 = a & P . 1 = b ) by A3, Def2;
hence ( f . (0,t) = a & f . (1,t) = b ) by A5, A6; ::_thesis: verum
end;
A7: for W being Point of [:I[01],I[01]:]
for G being a_neighborhood of f . W ex H being a_neighborhood of W st f .: H c= G
proof
let W be Point of [:I[01],I[01]:]; ::_thesis: for G being a_neighborhood of f . W ex H being a_neighborhood of W st f .: H c= G
let G be a_neighborhood of f . W; ::_thesis: ex H being a_neighborhood of W st f .: H c= G
W in the carrier of [:I[01],I[01]:] ;
then A8: W in [: the carrier of I[01], the carrier of I[01]:] by BORSUK_1:def_2;
then reconsider W1 = W `1 as Point of I[01] by MCART_1:10;
A9: ex x, y being set st [x,y] = W by A8, RELAT_1:def_1;
reconsider G9 = G as a_neighborhood of P . W1 by A2, A8;
the carrier of I[01] c= the carrier of I[01] ;
then reconsider AI = the carrier of I[01] as Subset of I[01] ;
AI = [#] I[01] ;
then Int AI = the carrier of I[01] by TOPS_1:15;
then A10: W `2 in Int AI by A8, MCART_1:10;
P is continuous by A3, Def2;
then consider H being a_neighborhood of W1 such that
A11: P .: H c= G9 by BORSUK_1:def_1;
set HH = [:H, the carrier of I[01]:];
[:H, the carrier of I[01]:] c= [: the carrier of I[01], the carrier of I[01]:] by ZFMISC_1:95;
then reconsider HH = [:H, the carrier of I[01]:] as Subset of [:I[01],I[01]:] by BORSUK_1:def_2;
( W1 in Int H & Int HH = [:(Int H),(Int AI):] ) by BORSUK_1:7, CONNSP_2:def_1;
then W in Int HH by A9, A10, MCART_1:11;
then reconsider HH = HH as a_neighborhood of W by CONNSP_2:def_1;
take HH ; ::_thesis: f .: HH c= G
f .: HH c= G
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in f .: HH or a in G )
assume a in f .: HH ; ::_thesis: a in G
then consider b being set such that
A12: b in dom f and
A13: b in HH and
A14: a = f . b by FUNCT_1:def_6;
reconsider b = b as Point of [:I[01],I[01]:] by A12;
A15: ( dom P = the carrier of I[01] & b `1 in H ) by A13, FUNCT_2:def_1, MCART_1:10;
dom f = [: the carrier of I[01], the carrier of I[01]:] by FUNCT_2:def_1;
then f . b = P . (b `1) by A2, A12;
then f . b in P .: H by A15, FUNCT_1:def_6;
hence a in G by A11, A14; ::_thesis: verum
end;
hence f .: HH c= G ; ::_thesis: verum
end;
take f ; :: according to BORSUK_2:def_7 ::_thesis: ( f is continuous & ( for t being Point of I[01] holds
( f . (t,0) = P . t & f . (t,1) = P . t & f . (0,t) = a & f . (1,t) = b ) ) )
for s being Point of I[01] holds
( f . (s,0) = P . s & f . (s,1) = P . s )
proof
let s be Point of I[01]; ::_thesis: ( f . (s,0) = P . s & f . (s,1) = P . s )
reconsider s0 = [s,0], s1 = [s,1] as set ;
1 in the carrier of I[01] by Lm1;
then s1 in [: the carrier of I[01], the carrier of I[01]:] by ZFMISC_1:87;
then A16: S1[s1,f . s1] by A2;
0 in the carrier of I[01] by Lm1;
then s0 in [: the carrier of I[01], the carrier of I[01]:] by ZFMISC_1:87;
then S1[s0,f . s0] by A2;
hence ( f . (s,0) = P . s & f . (s,1) = P . s ) by A16, MCART_1:7; ::_thesis: verum
end;
hence ( f is continuous & ( for t being Point of I[01] holds
( f . (t,0) = P . t & f . (t,1) = P . t & f . (0,t) = a & f . (1,t) = b ) ) ) by A7, A4, BORSUK_1:def_1; ::_thesis: verum
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 predP,Q are_homotopic ;
reflexivity
for P being Path of a,b holds (T,a,b,b1,b1)
proof
a,b are_connected by Def3;
hence for P being Path of a,b holds (T,a,b,b1,b1) by Th12; ::_thesis: verum
end;
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
let T be non empty TopSpace; ::_thesis: 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 )
let a, b, c be Point of T; ::_thesis: 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 )
let G1 be Path of a,b; ::_thesis: 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 )
let G2 be Path of b,c; ::_thesis: ( G1 is continuous & G2 is continuous & G1 . 0 = a & G1 . 1 = b & G2 . 0 = b & G2 . 1 = c implies ( G1 + G2 is continuous & (G1 + G2) . 0 = a & (G1 + G2) . 1 = c ) )
assume ( G1 is continuous & G2 is continuous & G1 . 0 = a & G1 . 1 = b & G2 . 0 = b & G2 . 1 = c ) ; ::_thesis: ( G1 + G2 is continuous & (G1 + G2) . 0 = a & (G1 + G2) . 1 = c )
then ex h being Function of I[01],T st
( h is continuous & h . 0 = a & h . 1 = c & rng h c= (rng G1) \/ (rng G2) ) by Lm3;
then a,c are_connected by Def1;
hence ( G1 + G2 is continuous & (G1 + G2) . 0 = a & (G1 + G2) . 1 = c ) by Def2; ::_thesis: verum
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
take { the Element of T} ; ::_thesis: ( not { the Element of T} is empty & { the Element of T} is compact & { the Element of T} is connected )
thus ( not { the Element of T} is empty & { the Element of T} is compact & { the Element of T} is connected ) ; ::_thesis: verum
end;
end;
theorem Th15: :: 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
set e = L[01] (((0,1) (#)),((#) (0,1)));
let T be non empty TopSpace; ::_thesis: 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 )
let a, b be Point of T; ::_thesis: ( ex f being Function of I[01],T st
( f is continuous & f . 0 = a & f . 1 = b ) implies ex g being Function of I[01],T st
( g is continuous & g . 0 = b & g . 1 = a ) )
given P being Function of I[01],T such that A1: P is continuous and
A2: ( P . 0 = a & P . 1 = b ) ; ::_thesis: ex g being Function of I[01],T st
( g is continuous & g . 0 = b & g . 1 = a )
set f = P * (L[01] (((0,1) (#)),((#) (0,1))));
reconsider f = P * (L[01] (((0,1) (#)),((#) (0,1)))) as Function of I[01],T by TOPMETR:20;
take f ; ::_thesis: ( f is continuous & f . 0 = b & f . 1 = a )
L[01] (((0,1) (#)),((#) (0,1))) is continuous Function of (Closed-Interval-TSpace (0,1)),(Closed-Interval-TSpace (0,1)) by TREAL_1:8;
hence f is continuous by A1, TOPMETR:20; ::_thesis: ( f . 0 = b & f . 1 = a )
A3: (L[01] (((0,1) (#)),((#) (0,1)))) . 1 = (L[01] (((0,1) (#)),((#) (0,1)))) . ((0,1) (#)) by TREAL_1:def_2
.= (#) (0,1) by TREAL_1:9
.= 0 by TREAL_1:def_1 ;
1 in [.0,1.] by XXREAL_1:1;
then 1 in the carrier of (Closed-Interval-TSpace (0,1)) by TOPMETR:18;
then A4: 1 in dom (L[01] (((0,1) (#)),((#) (0,1)))) by FUNCT_2:def_1;
0 in [.0,1.] by XXREAL_1:1;
then 0 in the carrier of (Closed-Interval-TSpace (0,1)) by TOPMETR:18;
then A5: 0 in dom (L[01] (((0,1) (#)),((#) (0,1)))) by FUNCT_2:def_1;
(L[01] (((0,1) (#)),((#) (0,1)))) . 0 = (L[01] (((0,1) (#)),((#) (0,1)))) . ((#) (0,1)) by TREAL_1:def_1
.= (0,1) (#) by TREAL_1:9
.= 1 by TREAL_1:def_2 ;
hence ( f . 0 = b & f . 1 = a ) by A2, A3, A5, A4, FUNCT_1:13; ::_thesis: verum
end;
registration
cluster I[01] -> pathwise_connected ;
coherence
I[01] is pathwise_connected
proof
let a, b be Point of I[01]; :: according to BORSUK_2:def_3 ::_thesis: a,b are_connected
percases ( a <= b or b <= a ) ;
supposeA1: a <= b ; ::_thesis: a,b are_connected
then reconsider B = [.a,b.] as non empty Subset of I[01] by BORSUK_1:40, XXREAL_1:1, XXREAL_2:def_12;
( 0 <= a & b <= 1 ) by BORSUK_1:43;
then A2: Closed-Interval-TSpace (a,b) = I[01] | B by A1, TOPMETR:24;
the carrier of (I[01] | B) c= the carrier of I[01] by BORSUK_1:1;
then reconsider g = L[01] (((#) (a,b)),((a,b) (#))) as Function of the carrier of I[01], the carrier of I[01] by A2, FUNCT_2:7, TOPMETR:20;
reconsider g = g as Function of I[01],I[01] ;
take g ; :: according to BORSUK_2:def_1 ::_thesis: ( g is continuous & g . 0 = a & g . 1 = b )
thus g is continuous by PRE_TOPC:26, A1, A2, TOPMETR:20, TREAL_1:8; ::_thesis: ( g . 0 = a & g . 1 = b )
0 = (#) (0,1) by TREAL_1:def_1;
hence g . 0 = (#) (a,b) by A1, TREAL_1:9
.= a by A1, TREAL_1:def_1 ;
::_thesis: g . 1 = b
1 = (0,1) (#) by TREAL_1:def_2;
hence g . 1 = (a,b) (#) by A1, TREAL_1:9
.= b by A1, TREAL_1:def_2 ;
::_thesis: verum
end;
supposeA3: b <= a ; ::_thesis: a,b are_connected
then reconsider B = [.b,a.] as non empty Subset of I[01] by BORSUK_1:40, XXREAL_1:1, XXREAL_2:def_12;
( 0 <= b & a <= 1 ) by BORSUK_1:43;
then A4: Closed-Interval-TSpace (b,a) = I[01] | B by A3, TOPMETR:24;
the carrier of (I[01] | B) c= the carrier of I[01] by BORSUK_1:1;
then reconsider g = L[01] (((#) (b,a)),((b,a) (#))) as Function of the carrier of I[01], the carrier of I[01] by A4, FUNCT_2:7, TOPMETR:20;
reconsider g = g as Function of I[01],I[01] ;
0 = (#) (0,1) by TREAL_1:def_1;
then A5: g . 0 = (#) (b,a) by A3, TREAL_1:9
.= b by A3, TREAL_1:def_1 ;
1 = (0,1) (#) by TREAL_1:def_2;
then A6: g . 1 = (b,a) (#) by A3, TREAL_1:9
.= a by A3, TREAL_1:def_2 ;
A7: g is continuous by PRE_TOPC:26, A3, A4, TOPMETR:20, TREAL_1:8;
then b,a are_connected by A5, A6, Def1;
then reconsider P = g as Path of b,a by A7, A5, A6, Def2;
take - P ; :: according to BORSUK_2:def_1 ::_thesis: ( - P is continuous & (- P) . 0 = a & (- P) . 1 = b )
ex t being Function of I[01],I[01] st
( t is continuous & t . 0 = a & t . 1 = b ) by A7, A5, A6, Th15;
then a,b are_connected by Def1;
hence ( - P is continuous & (- P) . 0 = a & (- P) . 1 = b ) by Def2; ::_thesis: verum
end;
end;
end;
end;