let p1, p2, p3, p4 be Point of (TOP-REAL 2); :: thesis: for P being non empty compact Subset of (TOP-REAL 2)
for C0 being Subset of (TOP-REAL 2) st P = { p where p is Point of (TOP-REAL 2) : |.p.| = 1 } & LE p1,p2,P & LE p2,p3,P & LE p3,p4,P holds
for f, g being Function of I[01] ,(TOP-REAL 2) st f is continuous & f is one-to-one & g is continuous & g is one-to-one & C0 = { p where p is Point of (TOP-REAL 2) : |.p.| >= 1 } & f . 0 = p1 & f . 1 = p3 & g . 0 = p2 & g . 1 = p4 & rng f c= C0 & rng g c= C0 holds
rng f meets rng g
let P be non empty compact Subset of (TOP-REAL 2); :: thesis: for C0 being Subset of (TOP-REAL 2) st P = { p where p is Point of (TOP-REAL 2) : |.p.| = 1 } & LE p1,p2,P & LE p2,p3,P & LE p3,p4,P holds
for f, g being Function of I[01] ,(TOP-REAL 2) st f is continuous & f is one-to-one & g is continuous & g is one-to-one & C0 = { p where p is Point of (TOP-REAL 2) : |.p.| >= 1 } & f . 0 = p1 & f . 1 = p3 & g . 0 = p2 & g . 1 = p4 & rng f c= C0 & rng g c= C0 holds
rng f meets rng g
let C0 be Subset of (TOP-REAL 2); :: thesis: ( P = { p where p is Point of (TOP-REAL 2) : |.p.| = 1 } & LE p1,p2,P & LE p2,p3,P & LE p3,p4,P implies for f, g being Function of I[01] ,(TOP-REAL 2) st f is continuous & f is one-to-one & g is continuous & g is one-to-one & C0 = { p where p is Point of (TOP-REAL 2) : |.p.| >= 1 } & f . 0 = p1 & f . 1 = p3 & g . 0 = p2 & g . 1 = p4 & rng f c= C0 & rng g c= C0 holds
rng f meets rng g )
assume A1: ( P = { p where p is Point of (TOP-REAL 2) : |.p.| = 1 } & LE p1,p2,P & LE p2,p3,P & LE p3,p4,P ) ; :: thesis: for f, g being Function of I[01] ,(TOP-REAL 2) st f is continuous & f is one-to-one & g is continuous & g is one-to-one & C0 = { p where p is Point of (TOP-REAL 2) : |.p.| >= 1 } & f . 0 = p1 & f . 1 = p3 & g . 0 = p2 & g . 1 = p4 & rng f c= C0 & rng g c= C0 holds
rng f meets rng g
let f, g be Function of I[01] ,(TOP-REAL 2); :: thesis: ( f is continuous & f is one-to-one & g is continuous & g is one-to-one & C0 = { p where p is Point of (TOP-REAL 2) : |.p.| >= 1 } & f . 0 = p1 & f . 1 = p3 & g . 0 = p2 & g . 1 = p4 & rng f c= C0 & rng g c= C0 implies rng f meets rng g )
assume A2: ( f is continuous & f is one-to-one & g is continuous & g is one-to-one & C0 = { p where p is Point of (TOP-REAL 2) : |.p.| >= 1 } & f . 0 = p1 & f . 1 = p3 & g . 0 = p2 & g . 1 = p4 & rng f c= C0 & rng g c= C0 ) ; :: thesis: rng f meets rng g
A3: dom f = the carrier of I[01] by FUNCT_2:def 1;
A4: dom g = the carrier of I[01] by FUNCT_2:def 1;
per cases ( not p1 <> p2 or not p2 <> p3 or not p3 <> p4 or ( p1 <> p2 & p2 <> p3 & p3 <> p4 ) ) ;
suppose A5: ( not p1 <> p2 or not p2 <> p3 or not p3 <> p4 ) ; :: thesis: rng f meets rng g
now
per cases ( p1 = p2 or p2 = p3 or p3 = p4 ) by A5;
end;
end;
hence rng f meets rng g ; :: thesis: verum
end;
suppose ( p1 <> p2 & p2 <> p3 & p3 <> p4 ) ; :: thesis: rng f meets rng g
then consider h being Function of (TOP-REAL 2),(TOP-REAL 2) such that
A12: ( h is being_homeomorphism & ( for q being Point of (TOP-REAL 2) holds |.(h . q).| = |.q.| ) & |[(- 1),0 ]| = h . p1 & |[0 ,1]| = h . p2 & |[1,0 ]| = h . p3 & |[0 ,(- 1)]| = h . p4 ) by A1, Th70;
A13: h is one-to-one by A12, TOPS_2:def 5;
reconsider f2 = h * f, g2 = h * g as Function of I[01] ,(TOP-REAL 2) ;
A14: dom f2 = the carrier of I[01] by FUNCT_2:def 1;
A15: dom g2 = the carrier of I[01] by FUNCT_2:def 1;
A16: f2 . 0 = |[(- 1),0 ]| by A2, A12, A14, Lm8, BORSUK_1:83, FUNCT_1:22;
A17: g2 . 0 = |[0 ,1]| by A2, A12, A15, Lm8, BORSUK_1:83, FUNCT_1:22;
A18: f2 . 1 = |[1,0 ]| by A2, A12, A14, Lm9, BORSUK_1:83, FUNCT_1:22;
A19: g2 . 1 = |[0 ,(- 1)]| by A2, A12, A15, Lm9, BORSUK_1:83, FUNCT_1:22;
A20: ( f2 is continuous & f2 is one-to-one & g2 is continuous & g2 is one-to-one & f2 . 0 = |[(- 1),0 ]| & f2 . 1 = |[1,0 ]| & g2 . 0 = |[0 ,1]| & g2 . 1 = |[0 ,(- 1)]| ) by A2, A12, A14, A15, Lm8, Lm9, Th8, Th9, BORSUK_1:83, FUNCT_1:22;
A21: rng f2 c= C0
proof
let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in rng f2 or y in C0 )
assume y in rng f2 ; :: thesis: y in C0
then consider x being set such that
A22: ( x in dom f2 & y = f2 . x ) by FUNCT_1:def 5;
A23: f2 . x = h . (f . x) by A22, FUNCT_1:22;
A24: f . x in rng f by A3, A22, FUNCT_1:def 5;
then A25: f . x in C0 by A2;
reconsider qf = f . x as Point of (TOP-REAL 2) by A24;
consider q5 being Point of (TOP-REAL 2) such that
A26: ( q5 = f . x & |.q5.| >= 1 ) by A2, A25;
|.(h . qf).| = |.qf.| by A12;
hence y in C0 by A2, A22, A23, A26; :: thesis: verum
end;
A27: rng g2 c= C0
proof
let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in rng g2 or y in C0 )
assume y in rng g2 ; :: thesis: y in C0
then consider x being set such that
A28: ( x in dom g2 & y = g2 . x ) by FUNCT_1:def 5;
A29: g2 . x = h . (g . x) by A28, FUNCT_1:22;
A30: g . x in rng g by A4, A28, FUNCT_1:def 5;
then A31: g . x in C0 by A2;
reconsider qg = g . x as Point of (TOP-REAL 2) by A30;
consider q5 being Point of (TOP-REAL 2) such that
A32: ( q5 = g . x & |.q5.| >= 1 ) by A2, A31;
|.(h . qg).| = |.qg.| by A12;
hence y in C0 by A2, A28, A29, A32; :: thesis: verum
end;
defpred S1[ Point of (TOP-REAL 2)] means ( |.$1.| = 1 & $1 `2 <= $1 `1 & $1 `2 >= - ($1 `1 ) );
{ q1 where q1 is Point of (TOP-REAL 2) : S1[q1] } is Subset of (TOP-REAL 2) from JGRAPH_2:sch 1();
then reconsider KXP = { q1 where q1 is Point of (TOP-REAL 2) : ( |.q1.| = 1 & q1 `2 <= q1 `1 & q1 `2 >= - (q1 `1 ) ) } as Subset of (TOP-REAL 2) ;
defpred S2[ Point of (TOP-REAL 2)] means ( |.$1.| = 1 & $1 `2 >= $1 `1 & $1 `2 <= - ($1 `1 ) );
{ q2 where q2 is Point of (TOP-REAL 2) : S2[q2] } is Subset of (TOP-REAL 2) from JGRAPH_2:sch 1();
then reconsider KXN = { q2 where q2 is Point of (TOP-REAL 2) : ( |.q2.| = 1 & q2 `2 >= q2 `1 & q2 `2 <= - (q2 `1 ) ) } as Subset of (TOP-REAL 2) ;
defpred S3[ Point of (TOP-REAL 2)] means ( |.$1.| = 1 & $1 `2 >= $1 `1 & $1 `2 >= - ($1 `1 ) );
{ q3 where q3 is Point of (TOP-REAL 2) : S3[q3] } is Subset of (TOP-REAL 2) from JGRAPH_2:sch 1();
then reconsider KYP = { q3 where q3 is Point of (TOP-REAL 2) : ( |.q3.| = 1 & q3 `2 >= q3 `1 & q3 `2 >= - (q3 `1 ) ) } as Subset of (TOP-REAL 2) ;
defpred S4[ Point of (TOP-REAL 2)] means ( |.$1.| = 1 & $1 `2 <= $1 `1 & $1 `2 <= - ($1 `1 ) );
{ q4 where q4 is Point of (TOP-REAL 2) : S4[q4] } is Subset of (TOP-REAL 2) from JGRAPH_2:sch 1();
then reconsider KYN = { q4 where q4 is Point of (TOP-REAL 2) : ( |.q4.| = 1 & q4 `2 <= q4 `1 & q4 `2 <= - (q4 `1 ) ) } as Subset of (TOP-REAL 2) ;
reconsider O = 0 , I = 1 as Point of I[01] by BORSUK_1:83, XXREAL_1:1;
- (|[(- 1),0 ]| `1 ) = 1 by Lm6;
then A33: f2 . O in KXN by A16, Lm6, Lm7;
A34: f2 . I in KXP by A18, Lm6, Lm7;
- (|[0 ,(- 1)]| `1 ) = 0 by Lm6;
then A35: g2 . I in KYN by A19, Lm6, Lm7;
- (|[0 ,1]| `1 ) = 0 by Lm6;
then g2 . O in KYP by A17, Lm6, Lm7;
then rng f2 meets rng g2 by A2, A20, A21, A27, A33, A34, A35, Th18;
then consider x2 being set such that
A36: ( x2 in rng f2 & x2 in rng g2 ) by XBOOLE_0:3;
consider z2 being set such that
A37: ( z2 in dom f2 & x2 = f2 . z2 ) by A36, FUNCT_1:def 5;
consider z3 being set such that
A38: ( z3 in dom g2 & x2 = g2 . z3 ) by A36, FUNCT_1:def 5;
A39: dom h = the carrier of (TOP-REAL 2) by FUNCT_2:def 1;
A40: g . z3 in rng g by A4, A38, FUNCT_1:def 5;
A41: f . z2 in rng f by A3, A37, FUNCT_1:def 5;
reconsider h1 = h as Function ;
A42: (h1 " ) . x2 = (h1 " ) . (h . (f . z2)) by A37, FUNCT_1:22
.= f . z2 by A13, A39, A41, FUNCT_1:56 ;
(h1 " ) . x2 = (h1 " ) . (h . (g . z3)) by A38, FUNCT_1:22
.= g . z3 by A13, A39, A40, FUNCT_1:56 ;
then ( (h1 " ) . x2 in rng f & (h1 " ) . x2 in rng g ) by A3, A4, A37, A38, A42, FUNCT_1:def 5;
hence rng f meets rng g by XBOOLE_0:3; :: thesis: verum
end;
end;