:: The {F}ashoda Meet Theorem for Continuous Mappings
:: by Yatsuka Nakamura , Andrzej Trybulec and Artur Korni{\l}owicz
::
:: Received September 14, 2005
:: Copyright (c) 2005-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies NUMBERS, SUBSET_1, PRE_TOPC, EUCLID, BORSUK_1, PCOMPS_1, TOPMETR,
CARD_1, FINSEQ_1, XXREAL_0, ORDINAL4, FUNCT_1, ARYTM_3, RELAT_1,
PARTFUN1, ORDINAL2, ARYTM_1, JGRAPH_6, CONVEX1, MCART_1, RLTOPSP1,
REAL_1, TOPREALA, TARSKI, STRUCT_0, XXREAL_1, MEASURE5, XBOOLE_0,
FCONT_2, METRIC_1, NAT_1, INT_1, COMPLEX1, XXREAL_2, RELAT_2, RCOMP_1,
CONNSP_1, GRAPH_1, WEIERSTR, PSCOMP_1, GOBOARD1, GOBOARD4, TOPREAL1,
BORSUK_2;
notations TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XXREAL_0, XCMPLX_0,
XREAL_0, COMPLEX1, REAL_1, FUNCT_1, RELSET_1, PARTFUN1, FUNCT_2,
FINSEQ_1, NAT_1, NAT_D, SEQM_3, STRUCT_0, TOPREAL1, PRE_TOPC, GOBOARD1,
GOBOARD4, TOPMETR, PCOMPS_1, COMPTS_1, WEIERSTR, METRIC_1, TBSP_1,
RCOMP_1, UNIFORM1, INT_1, CONNSP_1, PSCOMP_1, RLVECT_1, RLTOPSP1, EUCLID,
BORSUK_1, BORSUK_2, JGRAPH_6, TOPREALA, TOPALG_2;
constructors REAL_1, RCOMP_1, CONNSP_1, COMPTS_1, TBSP_1, TOPREAL1, GOBOARD1,
GOBOARD4, PSCOMP_1, WEIERSTR, UNIFORM1, JGRAPH_6, TOPALG_2, TOPREALA,
BORSUK_2, NAT_D, XXREAL_2, FUNCSDOM, CONVEX1, BINOP_2, NUMBERS;
registrations RELAT_1, XREAL_0, INT_1, FINSEQ_1, STRUCT_0, PRE_TOPC, BORSUK_1,
EUCLID, TOPREAL1, BORSUK_2, JORDAN5A, TOPALG_2, MEMBERED, VALUED_0,
FUNCT_2, XXREAL_2, RELSET_1, SPPOL_1, TOPMETR, FUNCT_1, NAT_1, ORDINAL1;
requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM;
definitions TARSKI, XBOOLE_0, JORDAN1;
equalities XBOOLE_0, RLTOPSP1, EUCLID, TOPREALA, STRUCT_0;
expansions TARSKI, XBOOLE_0, TOPALG_2;
theorems TARSKI, FUNCT_1, FINSEQ_1, NAT_1, FINSEQ_4, RELAT_1, FINSEQ_3,
TOPREAL1, GOBOARD4, TOPREAL3, EUCLID, UNIFORM1, WEIERSTR, PRE_TOPC,
TBSP_1, HEINE, COMPTS_1, TOPMETR, PSCOMP_1, BORSUK_1, RCOMP_1, FUNCT_2,
XBOOLE_0, XBOOLE_1, TOPRNS_1, XCMPLX_1, JGRAPH_1, INT_1, XREAL_0,
CONNSP_1, XREAL_1, BORSUK_2, TSEP_1, JGRAPH_6, JORDAN5B, FINSEQ_2,
XXREAL_0, TOPS_2, PARTFUN1, XXREAL_1, XXREAL_2, SEQM_3, RLTOPSP1,
RELSET_1, ORDINAL1;
schemes FINSEQ_1, NAT_1;
begin
reserve x, y for set;
reserve i, j, n for Nat;
reserve p1, p2 for Point of TOP-REAL n;
reserve a, b, c, d for Real;
Lm1: I[01]=TopSpaceMetr(Closed-Interval-MSpace(0,1)) by TOPMETR:20,def 7;
Lm2: for x being set,f being FinSequence st 1<=len f holds (f^<*x*>).1=f.1 & (
<*x*>^f).(len f +1)=f.len f
proof
let x be set,f be FinSequence;
assume
A1: 1<=len f;
then
A2: len f in dom f by FINSEQ_3:25;
A3: (<*x*>^f).(len f +1)=(<*x*>^f).(len <*x*>+len f) by FINSEQ_1:39
.=f.len f by A2,FINSEQ_1:def 7;
1 in dom f by A1,FINSEQ_3:25;
hence thesis by A3,FINSEQ_1:def 7;
end;
Lm3: for f being FinSequence of REAL st (for k being Nat st 1<=k &
k<len f holds f/.k<f/.(k+1)) holds f is increasing
proof
let f be FinSequence of REAL;
assume
A1: for k being Nat st 1<=k & k<len f holds f/.k<f/.(k+1);
now
let i,j;
now
defpred P[Nat] means i+(1+$1)<=len f implies f/.i<f/.(i+(1+$1
));
assume that
A2: i in dom f and
A3: j in dom f and
A4: i<j;
A5: 1<=i by A2,FINSEQ_3:25;
A6: for k being Nat st P[k] holds P[(k+1)]
proof
let k be Nat;
assume
A7: i+(1+k)<=len f implies f/.i<f/.(i+(1+k));
now
1<=i+1 & i+1<=i+1+k by NAT_1:11;
then
A8: 1<=i+1+k by XXREAL_0:2;
A9: i+(1+(k+1))=i+(1+k)+1;
1+k<1+(k+1) by NAT_1:13;
then
A10: i+(1+k)<i+(1+(k+1)) by XREAL_1:6;
assume
A11: i+(1+(k+1))<=len f;
then i+(1+k)<len f by A10,XXREAL_0:2;
then f/.(i+(1+k))<f/.(i+(1+(k+1))) by A1,A8,A9;
hence f/.i<f/.(i+(1+(k+1))) by A7,A11,A10,XXREAL_0:2;
end;
hence thesis;
end;
i+1<=j by A4,NAT_1:13;
then j-'(i+1)=j-(i+1) by XREAL_1:233;
then
A12: i+(1+(j-'(i+1))) = j;
A13: f/.i=f.i by A2,PARTFUN1:def 6;
A14: j<=len f by A3,FINSEQ_3:25;
then i<len f by A4,XXREAL_0:2;
then
A15: P[0] by A1,A5;
for k being Nat holds P[k] from NAT_1:sch 2(A15,A6);
then f/.i<f/.j by A14,A12;
hence f.i<f.j by A3,A13,PARTFUN1:def 6;
end;
hence i in dom f & j in dom f & i<j implies f.i<f.j;
end;
hence thesis by SEQM_3:def 1;
end;
registration
let a, b, c, d;
cluster closed_inside_of_rectangle(a,b,c,d) -> convex;
coherence
proof
set P = closed_inside_of_rectangle(a,b,c,d);
A1: P = {p where p is Point of TOP-REAL 2: a <= p`1 & p`1 <= b & c <= p`2
& p`2 <= d} by JGRAPH_6:def 2;
let w1, w2 be Point of TOP-REAL 2;
assume w1 in P & w2 in P;
then
A2: ( ex p3 being Point of TOP-REAL 2 st p3 = w1 & a <= p3`1 & p3`1 <= b &
c <= p3 `2 & p3`2 <= d)& ex p4 being Point of TOP-REAL 2 st p4 = w2 & a <= p4`1
& p4`1 <= b & c <= p4`2 & p4`2 <= d by A1;
let x be object;
assume x in LSeg(w1,w2);
then consider l being Real such that
A3: x = (1-l)*w1 + l*w2 and
A4: 0 <= l & l <= 1;
set w = (1-l)*w1 + l*w2;
A5: w = |[((1-l)*w1)`1+(l*w2)`1,((1-l)*w1)`2+ (l*w2)`2]| by EUCLID:55;
A6: l*w2=|[ l*w2`1 ,l*w2`2 ]| by EUCLID:57;
then
A7: (l*w2)`2=l*w2`2;
A8: (1-l)*w1=|[ (1-l)*w1`1 ,(1-l)*w1`2 ]| by EUCLID:57;
then ((1-l)*w1)`2= (1-l)*w1`2;
then w`2=(1-l)* w1`2+ l* w2`2 by A5,A7;
then
A9: c <= w`2 & w`2 <= d by A2,A4,XREAL_1:173,174;
A10: (l*w2)`1=l*w2`1 by A6;
((1-l)*w1)`1= (1-l)*w1`1 by A8;
then w`1=(1-l)* w1`1+ l* w2`1 by A5,A10;
then a <= w`1 & w`1 <= b by A2,A4,XREAL_1:173,174;
hence thesis by A1,A3,A9;
end;
end;
registration
let a, b, c, d;
cluster Trectangle(a,b,c,d) -> convex;
coherence
by PRE_TOPC:8;
end;
theorem Th1:
for e being positive Real, g being continuous Function
of I[01],TOP-REAL n ex h being FinSequence of REAL st h.1=0 & h.len h=1 & 5<=
len h & rng h c= the carrier of I[01] & h is increasing &
(for i being Nat,Q being Subset of I[01], W being Subset of Euclid n
st 1<=i & i<len h &
Q=[.h/.i,h/.(i+1).] & W=g.:(Q) holds diameter(W)<e)
proof
1 in {r where r is Real:0<=r & r<=1};
then
A1: 1 in [.0,1.] by RCOMP_1:def 1;
{1} c= [.0,1.]
by A1,TARSKI:def 1;
then
A2: [.0,1.] \/ {1} =[.0,1.] by XBOOLE_1:12;
Closed-Interval-TSpace(0,1) =TopSpaceMetr(Closed-Interval-MSpace(0,1))
by TOPMETR:def 7;
then
A3: the carrier of I[01] =the carrier of Closed-Interval-MSpace(0,1) by
TOPMETR:12,20
.= [.0,1.] by TOPMETR:10;
let e be positive Real, g be continuous Function of I[01],TOP-REAL
n;
reconsider e as positive Real;
A4: n in NAT by ORDINAL1:def 12;
then
reconsider f=g as Function of Closed-Interval-MSpace(0,1),Euclid n by
UNIFORM1:10;
A5: e/2<e by XREAL_1:216;
A6: e/2>0 by XREAL_1:215;
f is uniformly_continuous by UNIFORM1:8,A4;
then consider s1 being Real such that
A7: 0<s1 and
A8: for u1,u2 being Element of (Closed-Interval-MSpace(0,1)) st dist(u1,
u2) < s1 holds dist((f/.u1),(f/.u2)) < e/2 by A6,UNIFORM1:def 1;
set s=min(s1,1/2);
defpred P[Nat,object] means $2=s/2*($1-1);
A9: 0<=s by A7,XXREAL_0:20;
then reconsider j= [/ (2/s) \] as Nat by INT_1:53;
A10: 2/s<=j by INT_1:def 7;
A11: s<=s1 by XXREAL_0:17;
A12: for u1,u2 being Element of (Closed-Interval-MSpace(0,1)) st dist(u1,u2)
< s holds dist((f/.u1),(f/.u2)) < e/2
proof
let u1,u2 be Element of (Closed-Interval-MSpace(0,1));
assume dist(u1,u2) < s;
then dist(u1,u2) < s1 by A11,XXREAL_0:2;
hence thesis by A8;
end;
A13: 2/s <= [/ (2/s) \] by INT_1:def 7;
then 2/s-j<=0 by XREAL_1:47;
then 1+(2/s-j)<=1+0 by XREAL_1:6;
then
A14: s/2*(1+(2/s-j))<=s/2*1 by A9,XREAL_1:64;
A15: for k being Nat st k in Seg j ex x being object st P[k,x];
consider p being FinSequence such that
A16: dom p = Seg j & for k being Nat st k in Seg j holds P[k,p.k] from
FINSEQ_1:sch 1(A15);
A17: Seg len p=Seg j by A16,FINSEQ_1:def 3;
rng (p^<*1*>) c= REAL
proof
let y be object;
A18: len (p^<*1*>)=len p+1 by FINSEQ_2:16;
assume y in rng (p^<*1*>);
then consider x being object such that
A19: x in dom (p^<*1*>) and
A20: y=(p^<*1*>).x by FUNCT_1:def 3;
reconsider nx=x as Nat by A19;
A21: dom (p^<*1*>)=Seg len (p^<*1*>) by FINSEQ_1:def 3;
then
A22: 1<=nx by A19,FINSEQ_1:1;
A23: 1<=nx by A19,A21,FINSEQ_1:1;
A24: nx<=len (p^<*1*>) by A19,A21,FINSEQ_1:1;
per cases;
suppose
nx<len p+1;
then
A25: nx<=len p by NAT_1:13;
then nx in Seg j by A17,A23,FINSEQ_1:1;
then
A26: p.nx=s/2*(nx-1) by A16;
y=p.nx by A20,A22,A25,FINSEQ_1:64;
hence thesis by A26,XREAL_0:def 1;
end;
suppose
nx>=len p+1;
then nx=len p+1 by A24,A18,XXREAL_0:1;
then
A27: y=1 by A20,FINSEQ_1:42;
1 in REAL by XREAL_0:def 1;
hence thesis by A27;
end;
end;
then reconsider h1=p^<*1*> as FinSequence of REAL by FINSEQ_1:def 4;
A28: len h1 =len p+1 by FINSEQ_2:16;
j in NAT by ORDINAL1:def 12;
then
A29: len p=j by A16,FINSEQ_1:def 3;
A30: s<>0 by A7,XXREAL_0:15;
then 2/s>=2/(1/2) by A9,XREAL_1:118,XXREAL_0:17;
then 4<=j by A10,XXREAL_0:2;
then
A31: 4+1<=len p+1 by A29,XREAL_1:6;
A32: s/2>0 by A9,A30,XREAL_1:215;
A33: for i being Nat,r1,r2 being Real st 1<=i & i<len p & r1=p.i
& r2=p.(i+1) holds r1<r2 & r2-r1=s/2
proof
let i be Nat,r1,r2 be Real;
assume that
A34: 1<=i & i<len p and
A35: r1=p.i and
A36: r2=p.(i+1);
1<i+1 & i+1<=len p by A34,NAT_1:13;
then (i+1) in Seg j by A17,FINSEQ_1:1;
then
A37: r2=s/2*(i+1-1) by A16,A36;
i<i+1 by NAT_1:13;
then
A38: i-1<i+1-1 by XREAL_1:9;
A39: i in Seg j by A17,A34,FINSEQ_1:1;
then r1=s/2*(i-1) by A16,A35;
hence r1<r2 by A32,A37,A38,XREAL_1:68;
r2-r1=s/2*(i)-s/2*(i-1) by A16,A35,A39,A37;
hence thesis;
end;
0<s by A7,A30,XXREAL_0:20;
then 0<j by A13,XREAL_1:139;
then
A40: 0+1<=j by NAT_1:13;
then 1 in Seg j by FINSEQ_1:1;
then p.1=s/2*(1-1) by A16
.=0;
then
A41: h1.1=0 by A40,A29,Lm2;
2*s<>0 by A7,XXREAL_0:15;
then
A42: s/2*(2/s)=(2*s)/(2*s) & (2*s)/(2*s)=1 by XCMPLX_1:60,76;
then
A43: 1-s/2*(j-1)=s/2*(1+(2/s- [/ (2/s) \]));
A44: for r1 being Real st r1=p.len p holds 1-r1<=s/2
by A40,A29,FINSEQ_1:1,A14,A16,A43;
A45: for i being Nat st 1<=i & i<len h1 holds h1/.(i+1)-h1/.i<=s /2
proof
let i be Nat;
assume that
A46: 1<=i and
A47: i<len h1;
A48: i+1<=len h1 by A47,NAT_1:13;
A49: i<=len p by A28,A47,NAT_1:13;
A50: 1<i+1 by A46,NAT_1:13;
per cases;
suppose
A51: i<len p;
then i+1<=len p by NAT_1:13;
then
A52: h1.(i+1)=p.(i+1) by A50,FINSEQ_1:64;
A53: h1.i=p.i by A46,A51,FINSEQ_1:64;
h1.i=h1/.i & h1.(i+1)=h1/.(i+1) by A46,A47,A48,A50,FINSEQ_4:15;
hence thesis by A33,A46,A51,A53,A52;
end;
suppose
i>=len p;
then
A54: i=len p by A49,XXREAL_0:1;
A55: h1/.i=h1.i by A46,A47,FINSEQ_4:15
.=p.i by A46,A49,FINSEQ_1:64;
h1/.(i+1)=h1.(i+1) by A48,A50,FINSEQ_4:15
.=1 by A54,FINSEQ_1:42;
hence thesis by A44,A54,A55;
end;
end;
[/ (2/s) \] < 2/s+1 by INT_1:def 7;
then [/ (2/s) \] -1 < 2/s+1-1 by XREAL_1:9;
then
A56: s/2*(j-1)<s/2*(2/s) by A32,XREAL_1:68;
A57: for i being Nat,r1 being Real st 1<=i & i<=len p & r1=p.i
holds r1<1
proof
let i be Nat,r1 be Real;
assume that
A58: 1<=i and
A59: i<=len p and
A60: r1=p.i;
i-1<=j-1 by A29,A59,XREAL_1:9;
then
A61: (s/2)*(i-1)<=(s/2)*(j-1) by A9,XREAL_1:64;
i in Seg j by A17,A58,A59,FINSEQ_1:1;
then r1=s/2*(i-1) by A16,A60;
hence thesis by A56,A42,A61,XXREAL_0:2;
end;
A62: for i being Nat st 1<=i & i<len h1 holds h1/.i<h1/.(i+1)
proof
let i be Nat;
assume that
A63: 1<=i and
A64: i<len h1;
A65: i+1<=len h1 by A64,NAT_1:13;
A66: 1<i+1 by A63,NAT_1:13;
A67: i<=len p by A28,A64,NAT_1:13;
per cases;
suppose
A68: i<len p;
then i+1<=len p by NAT_1:13;
then
A69: h1.(i+1)=p.(i+1) by A66,FINSEQ_1:64;
A70: h1.i=p.i by A63,A68,FINSEQ_1:64;
h1.i=h1/.i & h1.(i+1)=h1/.(i+1) by A63,A64,A65,A66,FINSEQ_4:15;
hence thesis by A33,A63,A68,A70,A69;
end;
suppose
i>=len p;
then
A71: i=len p by A67,XXREAL_0:1;
A72: h1/.(i+1)=h1.(i+1) by A65,A66,FINSEQ_4:15
.=1 by A71,FINSEQ_1:42;
h1/.i=h1.i by A63,A64,FINSEQ_4:15
.=p.i by A63,A67,FINSEQ_1:64;
hence thesis by A57,A63,A67,A72;
end;
end;
A73: dom g=the carrier of I[01] by FUNCT_2:def 1;
A74: for i being Nat,Q being Subset of I[01], W being Subset of
Euclid n st 1<=i & i<len h1 & Q=[.h1/.i,h1/.(i+1).] & W=g.:(Q) holds diameter(W
)<e
proof
let i be Nat,Q be Subset of I[01], W be Subset of Euclid n;
assume that
A75: 1<=i & i<len h1 and
A76: Q=[.h1/.i,h1/.(i+1).] and
A77: W=g.:(Q);
h1/.i<h1/.(i+1) by A62,A75;
then
A78: Q<>{} by A76,XXREAL_1:1;
A79: for x,y being Point of Euclid n st x in W & y in W holds dist(x,y)<= e/2
proof
let x,y be Point of Euclid n;
assume that
A80: x in W and
A81: y in W;
consider x3 being object such that
A82: x3 in dom g and
A83: x3 in Q and
A84: x=g.x3 by A77,A80,FUNCT_1:def 6;
reconsider x3 as Element of Closed-Interval-MSpace(0,1) by A82,Lm1,
TOPMETR:12;
reconsider r3=x3 as Real by A83;
A85: h1/.(i+1)-h1/.i<=s/2 by A45,A75;
consider y3 being object such that
A86: y3 in dom g and
A87: y3 in Q and
A88: y=g.y3 by A77,A81,FUNCT_1:def 6;
reconsider y3 as Element of Closed-Interval-MSpace(0,1) by A86,Lm1,
TOPMETR:12;
reconsider s3=y3 as Real by A87;
A89: f.x3=(f/.x3) & f.y3=(f/.y3);
|.r3-s3.|<=h1/.(i+1)-h1/.i by A76,A83,A87,UNIFORM1:12;
then |.r3-s3.|<=s/2 by A85,XXREAL_0:2;
then
A90: dist(x3,y3)<=s/2 by HEINE:1;
s/2<s by A9,A30,XREAL_1:216;
then dist(x3,y3)<s by A90,XXREAL_0:2;
hence thesis by A12,A84,A88,A89;
end;
then W is bounded by A6,TBSP_1:def 7;
then diameter(W)<=e/2 by A73,A77,A78,A79,TBSP_1:def 8;
hence thesis by A5,XXREAL_0:2;
end;
A91: rng p c=[.0,1.]
proof
let y be object;
assume y in rng p;
then consider x being object such that
A92: x in dom p and
A93: y=p.x by FUNCT_1:def 3;
reconsider nx=x as Nat by A92;
A94: p.nx=s/2*(nx-1) by A16,A92;
then reconsider ry=p.nx as Real;
A95: x in Seg len p by A92,FINSEQ_1:def 3;
then
A96: 1<=nx by FINSEQ_1:1;
then
A97: nx-1>=1-1 by XREAL_1:9;
nx<=len p by A95,FINSEQ_1:1;
then ry<1 by A57,A96;
then y in {rs where rs is Real:0<=rs & rs<=1} by A9,A93,A94,A97;
hence thesis by RCOMP_1:def 1;
end;
rng <*1*> ={1} by FINSEQ_1:38;
then rng h1 =rng p \/ {1} by FINSEQ_1:31;
then
A98: rng h1 c=[.0,1.] \/ {1} by A91,XBOOLE_1:13;
h1.len h1=1 by A28,FINSEQ_1:42;
hence thesis by A28,A31,A41,A2,A98,A3,A62,A74,Lm3;
end;
theorem Th2:
for P being Subset of TOP-REAL n st P c= LSeg(p1,p2) & p1 in P &
p2 in P & P is connected holds P = LSeg(p1,p2)
proof
let P be Subset of TOP-REAL n;
assume that
A1: P c= LSeg(p1,p2) and
A2: p1 in P and
A3: p2 in P and
A4: P is connected;
reconsider L=LSeg(p1,p2) as non empty Subset of TOP-REAL n by A1,A2;
now
A5: the carrier of ((TOP-REAL n)|L)=[#]((TOP-REAL n)|L)
.= L by PRE_TOPC:def 5;
then reconsider PX=P as Subset of (TOP-REAL n)|L by A1;
assume not LSeg(p1,p2) c= P;
then consider x0 being object such that
A6: x0 in LSeg(p1,p2) and
A7: not x0 in P;
reconsider p0=x0 as Point of TOP-REAL n by A6;
A8: LSeg(p0,p2)\{p0} c= LSeg(p0,p2) by XBOOLE_1:36;
A9: p1 in LSeg(p1,p2) by RLTOPSP1:68;
then reconsider PX1=LSeg(p1,p0) as Subset of (TOP-REAL n)|L by A6,A5,
TOPREAL1:6;
A10: LSeg(p1,p0)\{p0} c= LSeg(p1,p0) by XBOOLE_1:36;
LSeg(p1,p0) c= L by A6,A9,TOPREAL1:6;
then reconsider R1=LSeg(p1,p0)\{p0} as Subset of (TOP-REAL n)|L by A10,A5,
XBOOLE_1:1;
A11: (TOP-REAL n)|L is T_2 by TOPMETR:2;
A12: p2 in LSeg(p1,p2) by RLTOPSP1:68;
then LSeg(p0,p2) c= L by A6,TOPREAL1:6;
then reconsider R2=LSeg(p0,p2)\{p0} as Subset of (TOP-REAL n)|L by A5,A8,
XBOOLE_1:1;
reconsider PX2=LSeg(p0,p2) as Subset of (TOP-REAL n)|L by A6,A5,A12,
TOPREAL1:6;
A13: PX1 /\ PX2 ={p0} by A6,TOPREAL1:8;
A14: R1 c= PX1 by XBOOLE_1:36;
A15: now
assume P c= R1;
then
A16: p2 in R1 by A3;
p2 in PX2 by RLTOPSP1:68;
then p2 in PX1 /\ PX2 by A14,A16,XBOOLE_0:def 4;
hence contradiction by A3,A7,A13,TARSKI:def 1;
end;
A17: {p0} c= LSeg(p1,p0)
proof
let d be object;
assume d in {p0};
then d=p0 by TARSKI:def 1;
hence thesis by RLTOPSP1:68;
end;
A18: {p0} c= LSeg(p0,p2)
proof
let d be object;
assume d in {p0};
then d=p0 by TARSKI:def 1;
hence thesis by RLTOPSP1:68;
end;
PX2 is compact by COMPTS_1:19;
then PX2 is closed by A11,COMPTS_1:7;
then
A19: Cl PX2 =PX2 by PRE_TOPC:22;
A20: Cl R2 c= Cl PX2 by PRE_TOPC:19,XBOOLE_1:36;
R1 /\ PX2 = PX1 /\ PX2 \ {p0} by XBOOLE_1:49
.= {} by A13,XBOOLE_1:37;
then R1/\ (Cl R2)={} by A19,A20,XBOOLE_1:3,27;
then
A21: R1 misses (Cl R2);
A22: PX1 /\ PX2 ={p0} by A6,TOPREAL1:8;
A23: R2 c= PX2 by XBOOLE_1:36;
A24: now
assume P c= R2;
then
A25: p1 in R2 by A2;
p1 in PX1 by RLTOPSP1:68;
then p1 in PX1 /\ PX2 by A23,A25,XBOOLE_0:def 4;
hence contradiction by A2,A7,A13,TARSKI:def 1;
end;
PX1 is compact by COMPTS_1:19;
then PX1 is closed by A11,COMPTS_1:7;
then
A26: Cl PX1 =PX1 by PRE_TOPC:22;
A27: L=LSeg(p1,p0) \/ LSeg(p0,p2) by A6,TOPREAL1:5
.=(LSeg(p1,p0)\{p0})\/{p0} \/ LSeg(p0,p2) by A17,XBOOLE_1:45
.=(LSeg(p1,p0)\{p0})\/ ({p0} \/ LSeg(p0,p2)) by XBOOLE_1:4
.= R1 \/ PX2 by A18,XBOOLE_1:12
.= R1 \/ ((PX2 \{p0}) \/ {p0}) by A18,XBOOLE_1:45
.= R1 \/ {p0} \/ R2 by XBOOLE_1:4;
A28: P c= R1 \/ R2
proof
let z be object;
assume
A29: z in P;
then z in R1 \/ {p0} or z in R2 by A1,A27,XBOOLE_0:def 3;
then z in R1 or z in {p0} or z in R2 by XBOOLE_0:def 3;
hence thesis by A7,A29,TARSKI:def 1,XBOOLE_0:def 3;
end;
A30: Cl R1 c= Cl PX1 by PRE_TOPC:19,XBOOLE_1:36;
PX1 /\ R2 =PX1 /\ PX2 \ {p0} by XBOOLE_1:49
.= {} by A22,XBOOLE_1:37;
then (Cl R1) /\ R2={} by A26,A30,XBOOLE_1:3,27;
then (Cl R1) misses R2;
then
A31: R1,R2 are_separated by A21,CONNSP_1:def 1;
PX is connected by A4,CONNSP_1:46;
hence contradiction by A31,A28,A15,A24,CONNSP_1:16;
end;
hence thesis by A1;
end;
theorem Th3:
for g being Path of p1,p2 st rng g c= LSeg(p1,p2) holds rng g = LSeg(p1,p2)
proof
let g be Path of p1,p2;
assume
A1: rng g c= LSeg(p1,p2);
A2: p2=g.1 by BORSUK_2:def 4;
A3: p1=g.0 by BORSUK_2:def 4;
now
A4: g.:([#]I[01]) c= rng g
proof
let y be object;
assume y in g.:([#]I[01]);
then ex x being object st x in dom g & x in [#]I[01] & y=g.x by
FUNCT_1:def 6;
hence thesis by FUNCT_1:def 3;
end;
1 in the carrier of I[01] by BORSUK_1:43;
then 1 in dom g by FUNCT_2:def 1;
then
A5: p2 in g.:([#]I[01]) by A2,FUNCT_1:def 6;
0 in the carrier of I[01] by BORSUK_1:43;
then 0 in dom g by FUNCT_2:def 1;
then
A6: p1 in g.:([#]I[01]) by A3,FUNCT_1:def 6;
[#]I[01] is connected by CONNSP_1:27;
then
A7: g.:([#]I[01]) is connected by TOPS_2:61;
assume not LSeg(p1,p2) c= rng g;
hence contradiction by A1,A7,A6,A5,A4,Th2,XBOOLE_1:1;
end;
hence thesis by A1;
end;
:: Goboard Theorem in continuous case
theorem Th4:
for P, Q being non empty Subset of TOP-REAL 2, p1, p2, q1, q2
being Point of TOP-REAL 2, f being Path of p1,p2, g being Path of q1,q2 st rng
f = P & rng g = Q & (for p being Point of TOP-REAL 2 st p in P holds p1`1<=p`1
& p`1<= p2`1) & (for p being Point of TOP-REAL 2 st p in Q holds p1`1<=p`1 & p
`1<= p2`1) & (for p being Point of TOP-REAL 2 st p in P holds q1`2<=p`2 & p`2<=
q2`2) & (for p being Point of TOP-REAL 2 st p in Q holds q1`2<=p`2 & p`2<= q2`2
) holds P meets Q
proof
A1: the TopStruct of TOP-REAL 2 = TopSpaceMetr Euclid 2 by EUCLID:def 8;
A2: [#](I[01]) is compact by COMPTS_1:1;
let P,Q be non empty Subset of TOP-REAL 2, p1,p2,q1,q2 be Point of TOP-REAL
2, f be Path of p1,p2, g be Path of q1,q2;
assume that
A3: rng f = P and
A4: rng g = Q and
A5: for p being Point of TOP-REAL 2 st p in P holds p1`1<=p`1 & p`1<= p2 `1 and
A6: for p being Point of TOP-REAL 2 st p in Q holds p1`1<=p`1 & p`1<= p2 `1 and
A7: for p being Point of TOP-REAL 2 st p in P holds q1`2<=p`2 & p`2<= q2 `2 and
A8: for p being Point of TOP-REAL 2 st p in Q holds q1`2<=p`2 & p`2<= q2 `2;
TopSpaceMetr(Euclid 2) = the TopStruct of TOP-REAL 2 by EUCLID:def 8;
then reconsider P9=P,Q9=Q as Subset of TopSpaceMetr(Euclid 2);
set e=min_dist_min(P9,Q9)/5;
f.:(the carrier of I[01])=rng f by RELSET_1:22;
then P is compact by A3,A2,WEIERSTR:8;
then
A9: P9 is compact by A1,COMPTS_1:23;
g.:([#](I[01]))=rng g by RELSET_1:22;
then Q is compact by A4,A2,WEIERSTR:8;
then
A10: Q9 is compact by A1,COMPTS_1:23;
assume
A11: P /\ Q= {};
then P misses Q;
then
A12: min_dist_min(P9,Q9)>0 by A10,A9,JGRAPH_1:38;
then
A13: e>0/5 by XREAL_1:74;
then consider h being FinSequence of REAL such that
A14: h.1=0 and
A15: h.len h=1 and
A16: 5<=len h and
A17: rng h c= the carrier of I[01] and
A18: h is increasing and
A19: for i being Nat,R being Subset of I[01], W being Subset
of Euclid 2 st 1<=i & i<len h & R=[.h/.i,h/.(i+1).] & W=f.:(R) holds diameter(W
)<e by Th1;
deffunc F(Nat)=f.(h.$1);
ex h19 being FinSequence st len h19=len h & for i be Nat st i in dom
h19 holds h19.i=F(i) from FINSEQ_1:sch 2;
then consider h19 being FinSequence such that
A20: len h19=len h and
A21: for i be Nat st i in dom h19 holds h19.i=f.(h.i);
A22: 1<=len h by A16,XXREAL_0:2;
then
A23: len h in dom h19 by A20,FINSEQ_3:25;
rng h19 c= the carrier of TOP-REAL 2
proof
let y be object;
A24: dom f= the carrier of I[01] by FUNCT_2:def 1;
assume y in rng h19;
then consider x being object such that
A25: x in dom h19 and
A26: y=h19.x by FUNCT_1:def 3;
reconsider i=x as Nat by A25;
dom h19=Seg len h19 by FINSEQ_1:def 3;
then i in dom h by A20,A25,FINSEQ_1:def 3;
then
A27: h.i in rng h by FUNCT_1:def 3;
h19.i=f.(h.i) by A21,A25;
then h19.i in rng f by A17,A27,A24,FUNCT_1:def 3;
hence thesis by A26;
end;
then reconsider h1=h19 as FinSequence of TOP-REAL 2 by FINSEQ_1:def 4;
A28: len h1>=1 by A16,A20,XXREAL_0:2;
then
A29: h1.1=h1/.1 by FINSEQ_4:15;
A30: f.0 = p1 by BORSUK_2:def 4;
A31: for i st 1<=i & i+1<=len h1 holds |.h1/.i-h1/.(i+1).|<e
proof
reconsider Pa=P as Subset of TOP-REAL 2;
A32: dom f =the carrier of I[01] by FUNCT_2:def 1;
reconsider W1=P as Subset of Euclid 2 by TOPREAL3:8;
let i;
assume that
A33: 1<=i and
A34: i+1<=len h1;
A35: 1<i+1 by A33,NAT_1:13;
then
A36: h.(i+1)=h/.(i+1) by A20,A34,FINSEQ_4:15;
A37: i+1 in dom h19 by A34,A35,FINSEQ_3:25;
then
A38: h19.(i+1)=f.(h.(i+1)) by A21;
then
A39: h1/.(i+1)=f.(h.(i+1)) by A34,A35,FINSEQ_4:15;
set r1=((E-bound Pa) - (W-bound Pa))+((N-bound Pa) - (S-bound Pa))+1;
[#](I[01]) is compact & f.:(the carrier of I[01])=rng f by COMPTS_1:1
,RELSET_1:22;
then
A40: Pa is compact by A3,WEIERSTR:8;
A41: for x,y being Point of Euclid 2 st x in W1 & y in W1 holds dist(x,y) <=r1
proof
let x,y be Point of Euclid 2;
assume that
A42: x in W1 and
A43: y in W1;
reconsider pw1=x,pw2=y as Point of TOP-REAL 2 by A42,A43;
A44: S-bound Pa <= pw2`2 & pw2`2 <= N-bound Pa by A40,A43,PSCOMP_1:24;
S-bound Pa <= pw1`2 & pw1`2 <= N-bound Pa by A40,A42,PSCOMP_1:24;
then
A45: |.pw1`2-pw2`2.|<=(N-bound Pa) - (S-bound Pa) by A44,JGRAPH_1:27;
A46: ((E-bound Pa) - (W-bound Pa))+((N-bound Pa) - (S-bound Pa)) <= ((
E-bound Pa) - (W-bound Pa))+((N-bound Pa) - (S-bound Pa)) +1 by XREAL_1:29;
A47: W-bound Pa <= pw2`1 & pw2`1 <= E-bound Pa by A40,A43,PSCOMP_1:24;
W-bound Pa <= pw1`1 & pw1`1 <= E-bound Pa by A40,A42,PSCOMP_1:24;
then |.pw1`1-pw2`1.|<=(E-bound Pa) - (W-bound Pa) by A47,JGRAPH_1:27;
then |.pw1`1-pw2`1.|+|.pw1`2-pw2`2.| <=((E-bound Pa) - (W-bound Pa))+
((N-bound Pa) - (S-bound Pa)) by A45,XREAL_1:7;
then
A48: |.pw1`1-pw2`1.|+|.pw1`2-pw2`2.|<=r1 by A46,XXREAL_0:2;
dist(x,y)=|.pw1-pw2.| & |.pw1-pw2.|<=|.pw1`1-pw2`1.|+|.pw1`2-pw2
`2.| by JGRAPH_1:28,32;
hence thesis by A48,XXREAL_0:2;
end;
i+1 in dom h by A20,A34,A35,FINSEQ_3:25;
then h.(i+1) in rng h by FUNCT_1:def 3;
then h19.(i+1) in rng f by A17,A38,A32,FUNCT_1:def 3;
then
A49: f.(h.(i+1)) is Element of TOP-REAL 2 by A21,A37;
A50: i<len h1 by A34,NAT_1:13;
then
A51: h.i=h/.i by A20,A33,FINSEQ_4:15;
A52: i in dom h by A20,A33,A50,FINSEQ_3:25;
then
A53: h.i in rng h by FUNCT_1:def 3;
A54: i+1 in dom h by A20,A34,A35,FINSEQ_3:25;
then h.(i+1) in rng h by FUNCT_1:def 3;
then reconsider R=[.h/.i,h/.(i+1).] as Subset of I[01] by A17,A53,A51,A36,
BORSUK_1:40,XXREAL_2:def 12;
A55: i in dom h19 by A33,A50,FINSEQ_3:25;
then
A56: h19.i=f.(h.i) by A21;
then h19.i in rng f by A17,A53,A32,FUNCT_1:def 3;
then f.(h.i) is Element of TOP-REAL 2 by A21,A55;
then reconsider w1=f.(h.i),w2=f.(h.(i+1)) as Point of Euclid 2 by A49,
TOPREAL3:8;
i<i+1 by NAT_1:13;
then
A57: h/.i <= h/.(i+1) by A18,A52,A51,A54,A36,SEQM_3:def 1;
then h.i in R by A51,XXREAL_1:1;
then
A58: w1 in f.:R by A32,FUNCT_1:def 6;
0 in the carrier of I[01] by BORSUK_1:43;
then
A59: f.0 in rng f by A32,FUNCT_1:def 3;
then S-bound Pa <= p1`2 & p1`2 <= N-bound Pa by A3,A30,A40,PSCOMP_1:24;
then (S-bound Pa)<=(N-bound Pa) by XXREAL_0:2;
then
A60: 0<=((N-bound Pa) - (S-bound Pa)) by XREAL_1:48;
W-bound Pa <= p1`1 & p1`1 <= E-bound Pa by A3,A30,A40,A59,PSCOMP_1:24;
then (W-bound Pa)<=(E-bound Pa) by XXREAL_0:2;
then 0<=((E-bound Pa) - (W-bound Pa)) by XREAL_1:48;
then
A61: W1 is bounded by A60,A41,TBSP_1:def 7;
h.(i+1) in R by A36,A57,XXREAL_1:1;
then
A62: w2 in f.:R by A32,FUNCT_1:def 6;
reconsider W=f.:R as Subset of Euclid 2 by TOPREAL3:8;
dom f=[#](I[01]) by FUNCT_2:def 1;
then P=f.:([.0,1.]) by A3,BORSUK_1:40,RELAT_1:113;
then W is bounded by A61,BORSUK_1:40,RELAT_1:123,TBSP_1:14;
then
A63: dist(w1,w2)<=diameter(W) by A58,A62,TBSP_1:def 8;
diameter W<e by A19,A20,A33,A50;
then
A64: dist(w1,w2)<e by A63,XXREAL_0:2;
h1/.i=f.(h.i) by A33,A50,A56,FINSEQ_4:15;
hence thesis by A39,A64,JGRAPH_1:28;
end;
A65: for i st i in dom h1 holds q1`2<=(h1/.i)`2 & (h1/.i)`2<=q2`2
proof
let i;
assume
A66: i in dom h1;
then h1.i=f.(h.i) by A21;
then
A67: h1/.i=f.(h.i) by A66,PARTFUN1:def 6;
i in dom h by A20,A66,FINSEQ_3:29;
then
A68: h.i in rng h by FUNCT_1:def 3;
dom f =the carrier of I[01] by FUNCT_2:def 1;
then h1/.i in rng f by A17,A67,A68,FUNCT_1:def 3;
hence thesis by A3,A7;
end;
for i st i in dom (Y_axis h1) holds q1`2<=(Y_axis h1).i & (Y_axis h1).
i<=q2`2
proof
let i;
assume i in dom (Y_axis h1);
then i in Seg len (Y_axis h1) by FINSEQ_1:def 3;
then i in Seg len h1 by A28,JGRAPH_1:42;
then
A69: i in dom h1 by FINSEQ_1:def 3;
then (Y_axis h1).i = (h1/.i)`2 by JGRAPH_1:43;
hence thesis by A65,A69;
end;
then
A70: Y_axis(h1) lies_between q1`2,q2`2 by GOBOARD4:def 2;
A71: f.1 = p2 by BORSUK_2:def 4;
A72: for i st i in dom h1 holds (h1/.1)`1<=(h1/.i)`1 & (h1/.i)`1<=(h1/.len
h1)`1
proof
len h in dom h19 by A20,A28,FINSEQ_3:25;
then h1.len h1=f.(h.len h) by A20,A21;
then
A73: h1/.len h1=f.(h.len h) by A28,FINSEQ_4:15;
1 in dom h19 by A28,FINSEQ_3:25;
then h1.1=f.(h.1) by A21;
then
A74: h1/.1=f.(h.1) by A28,FINSEQ_4:15;
let i;
assume
A75: i in dom h1;
then h1.i=f.(h.i) by A21;
then
A76: h1/.i=f.(h.i) by A75,PARTFUN1:def 6;
i in dom h by A20,A75,FINSEQ_3:29;
then
A77: h.i in rng h by FUNCT_1:def 3;
dom f =the carrier of I[01] by FUNCT_2:def 1;
then h1/.i in rng f by A17,A76,A77,FUNCT_1:def 3;
hence thesis by A3,A5,A30,A71,A14,A15,A74,A73;
end;
for i st i in dom X_axis h1 holds (X_axis h1).1<=(X_axis h1).i & (
X_axis h1).i<=(X_axis h1).len h1
proof
let i;
A78: (X_axis h1).1=(h1/.1)`1 & (X_axis h1).len h1=(h1/.len h1)`1 by A28,
JGRAPH_1:41;
assume i in dom X_axis h1;
then i in Seg len (X_axis h1) by FINSEQ_1:def 3;
then i in Seg len h1 by A28,JGRAPH_1:41;
then
A79: i in dom h1 by FINSEQ_1:def 3;
then (X_axis h1).i = (h1/.i)`1 by JGRAPH_1:43;
hence thesis by A72,A79,A78;
end;
then X_axis(h1) lies_between (X_axis(h1)).1, (X_axis(h1)).(len h1) by
GOBOARD4:def 2;
then consider f2 being FinSequence of TOP-REAL 2 such that
A80: f2 is special and
A81: f2.1=h1.1 and
A82: f2.len f2=h1.len h1 and
A83: len f2>=len h1 and
A84: X_axis(f2) lies_between (X_axis(h1)).1, (X_axis(h1)).(len h1) &
Y_axis(f2) lies_between q1`2,q2`2 and
A85: for j st j in dom f2 holds ex k being Nat st k in dom
h1 & |.(f2/.j - h1/.k).|<e and
A86: for j st 1<=j & j+1<=len f2 holds |.f2/.j - f2/.(j+1).|<e by A13,A31,A28
,A70,JGRAPH_1:39;
A87: len f2>=1 by A28,A83,XXREAL_0:2;
then
A88: f2.len f2=f2/.len f2 by FINSEQ_4:15;
consider hb being FinSequence of REAL such that
A89: hb.1=0 and
A90: hb.len hb=1 and
A91: 5<=len hb and
A92: rng hb c= the carrier of I[01] and
A93: hb is increasing and
A94: for i being Nat,R being Subset of I[01], W being Subset
of Euclid 2 st 1<=i & i<len hb & R=[.hb/.i,hb/.(i+1).] & W=g.:(R) holds
diameter(W)<e by A13,Th1;
deffunc F(Nat)=g.(hb.$1);
ex h29 being FinSequence st len h29=len hb & for i be Nat st i in dom
h29 holds h29.i=F(i) from FINSEQ_1:sch 2;
then consider h29 being FinSequence such that
A95: len h29=len hb and
A96: for i be Nat st i in dom h29 holds h29.i=g.(hb.i);
rng h29 c= the carrier of TOP-REAL 2
proof
let y be object;
A97: dom g = the carrier of I[01] by FUNCT_2:def 1;
assume y in rng h29;
then consider x being object such that
A98: x in dom h29 and
A99: y=h29.x by FUNCT_1:def 3;
reconsider i=x as Nat by A98;
dom h29=Seg len h29 by FINSEQ_1:def 3;
then i in dom hb by A95,A98,FINSEQ_1:def 3;
then
A100: hb.i in rng hb by FUNCT_1:def 3;
h29.i=g.(hb.i) by A96,A98;
then h29.i in rng g by A92,A100,A97,FUNCT_1:def 3;
hence thesis by A99;
end;
then reconsider h2=h29 as FinSequence of TOP-REAL 2 by FINSEQ_1:def 4;
A101: len h2>=1 by A91,A95,XXREAL_0:2;
1 in dom h19 by A20,A22,FINSEQ_3:25;
then
A102: h1/.1=f.(h.1) by A21,A29;
A103: 0 in the carrier of I[01] by BORSUK_1:43;
then 0 in dom f by FUNCT_2:def 1;
then
A104: p1 in P9 by A3,A30,FUNCT_1:def 3;
A105: 1<=len hb by A91,XXREAL_0:2;
then
A106: h2.len h2=h2/.len h2 by A95,FINSEQ_4:15;
A107: g.0 = q1 by BORSUK_2:def 4;
A108: for i st 1<=i & i+1<=len h2 holds |. (h2/.i)-(h2/.(i+1)) .|<e
proof
reconsider Qa=Q as Subset of TOP-REAL 2;
A109: dom g =the carrier of I[01] by FUNCT_2:def 1;
reconsider W1=Q as Subset of Euclid 2 by TOPREAL3:8;
let i;
assume that
A110: 1<=i and
A111: i+1<=len h2;
A112: i<len h2 by A111,NAT_1:13;
then
A113: hb.i=hb/.i by A95,A110,FINSEQ_4:15;
A114: 1<i+1 by A110,NAT_1:13;
then i+1 in Seg len hb by A95,A111,FINSEQ_1:1;
then i+1 in dom hb by FINSEQ_1:def 3;
then
A115: hb.(i+1) in rng hb by FUNCT_1:def 3;
A116: i+1 in dom h29 by A111,A114,FINSEQ_3:25;
then h29.(i+1)=g.(hb.(i+1)) by A96;
then h29.(i+1) in rng g by A92,A109,A115,FUNCT_1:def 3;
then
A117: g.(hb.(i+1)) is Element of TOP-REAL 2 by A96,A116;
i in dom h29 by A110,A112,FINSEQ_3:25;
then
A118: h29.i=g.(hb.i) by A96;
[#](I[01]) is compact & g.:(the carrier of I[01])=rng g by COMPTS_1:1
,RELSET_1:22;
then
A119: Qa is compact by A4,WEIERSTR:8;
reconsider Qa as non empty Subset of TOP-REAL 2;
set r1= ((E-bound Qa) - (W-bound Qa))+((N-bound Qa) - (S-bound Qa))+1;
A120: hb.(i+1)=hb/.(i+1) by A95,A111,A114,FINSEQ_4:15;
A121: for x,y being Point of Euclid 2 st x in W1 & y in W1 holds dist(x,y) <=r1
proof
let x,y be Point of Euclid 2;
assume that
A122: x in W1 and
A123: y in W1;
reconsider pw1=x,pw2=y as Point of TOP-REAL 2 by A122,A123;
A124: S-bound Qa <= pw2`2 & pw2`2 <= N-bound Qa by A119,A123,PSCOMP_1:24;
S-bound Qa <= pw1`2 & pw1`2 <= N-bound Qa by A119,A122,PSCOMP_1:24;
then
A125: |.pw1`2-pw2`2.|<=(N-bound Qa) - (S-bound Qa) by A124,JGRAPH_1:27;
A126: ((E-bound Qa) - (W-bound Qa))+((N-bound Qa) - (S-bound Qa)) <= ((
E-bound Qa) - (W-bound Qa))+((N-bound Qa) - (S-bound Qa)) +1 by XREAL_1:29;
A127: W-bound Qa <= pw2`1 & pw2`1 <= E-bound Qa by A119,A123,PSCOMP_1:24;
W-bound Qa <= pw1`1 & pw1`1 <= E-bound Qa by A119,A122,PSCOMP_1:24;
then |.pw1`1-pw2`1.|<=(E-bound Qa) - (W-bound Qa) by A127,JGRAPH_1:27;
then |.pw1`1-pw2`1.|+|.pw1`2-pw2`2.| <=((E-bound Qa) - (W-bound Qa))+
((N-bound Qa) - (S-bound Qa)) by A125,XREAL_1:7;
then
A128: |.pw1`1-pw2`1.|+|.pw1`2-pw2`2.|<=r1 by A126,XXREAL_0:2;
dist(x,y)=|.pw1-pw2.| & |.pw1-pw2.|<=|.pw1`1-pw2`1.|+|.pw1`2-
pw2`2.| by JGRAPH_1:28,32;
hence thesis by A128,XXREAL_0:2;
end;
0 in the carrier of I[01] by BORSUK_1:43;
then
A129: g.0 in rng g by A109,FUNCT_1:def 3;
then S-bound Qa <= q1`2 & q1`2 <= N-bound Qa by A4,A107,A119,PSCOMP_1:24;
then (S-bound Qa)<=(N-bound Qa) by XXREAL_0:2;
then
A130: 0<=((N-bound Qa) - (S-bound Qa)) by XREAL_1:48;
i in Seg len hb by A95,A110,A112,FINSEQ_1:1;
then
A131: i in dom hb by FINSEQ_1:def 3;
then
A132: hb.i in rng hb by FUNCT_1:def 3;
then h29.i in rng g by A92,A118,A109,FUNCT_1:def 3;
then reconsider w1=g.(hb.i),w2=g.(hb.(i+1)) as Point of Euclid 2 by A118
,A117,TOPREAL3:8;
i+1 in Seg len hb by A95,A111,A114,FINSEQ_1:1;
then
A133: i+1 in dom hb by FINSEQ_1:def 3;
then hb.(i+1) in rng hb by FUNCT_1:def 3;
then reconsider
R=[.hb/.i,hb/.(i+1).] as Subset of I[01] by A92,A132,A113,A120,BORSUK_1:40
,XXREAL_2:def 12;
i<i+1 by NAT_1:13;
then
A134: hb/.i <= hb/.(i+1) by A93,A131,A113,A133,A120,SEQM_3:def 1;
then hb.i in R by A113,XXREAL_1:1;
then
A135: w1 in g.:(R) by A109,FUNCT_1:def 6;
W-bound Qa <= q1`1 & q1`1 <= E-bound Qa by A4,A107,A119,A129,PSCOMP_1:24;
then (W-bound Qa)<=(E-bound Qa) by XXREAL_0:2;
then 0<=((E-bound Qa) - (W-bound Qa)) by XREAL_1:48;
then
A136: W1 is bounded by A130,A121,TBSP_1:def 7;
hb.(i+1) in R by A120,A134,XXREAL_1:1;
then
A137: w2 in g.:(R) by A109,FUNCT_1:def 6;
reconsider W=g.:(R) as Subset of Euclid 2 by TOPREAL3:8;
dom g=[#](I[01]) by FUNCT_2:def 1;
then Q=g.:([.0,1.]) by A4,BORSUK_1:40,RELAT_1:113;
then W is bounded by A136,BORSUK_1:40,RELAT_1:123,TBSP_1:14;
then
A138: dist(w1,w2)<=diameter(W) by A135,A137,TBSP_1:def 8;
diameter(W)<e by A94,A95,A110,A112;
then
A139: dist(w1,w2)<e by A138,XXREAL_0:2;
h2.(i+1)=h2/.(i+1) by A111,A114,FINSEQ_4:15;
then
A140: h2/.(i+1)=g.(hb.(i+1)) by A96,A116;
h2/.i=g.(hb.i) by A110,A112,A118,FINSEQ_4:15;
hence thesis by A140,A139,JGRAPH_1:28;
end;
A141: dom hb=Seg len hb by FINSEQ_1:def 3;
A142: for i st i in dom hb holds h2/.i=g.(hb.i)
proof
let i;
assume
A143: i in dom hb;
then i in dom h29 by A95,FINSEQ_3:29;
then
A144: h2.i=g.(hb.i) by A96;
1<=i & i<=len hb by A141,A143,FINSEQ_1:1;
hence thesis by A95,A144,FINSEQ_4:15;
end;
A145: for i st i in dom h2 holds p1`1<=(h2/.i)`1 & (h2/.i)`1<=p2`1
proof
let i;
assume i in dom h2;
then i in Seg len h2 by FINSEQ_1:def 3;
then i in dom hb by A95,FINSEQ_1:def 3;
then
A146: h2/.i=g.(hb.i) & hb.i in rng hb by A142,FUNCT_1:def 3;
dom g =the carrier of I[01] by FUNCT_2:def 1;
then h2/.i in rng g by A92,A146,FUNCT_1:def 3;
hence thesis by A4,A6;
end;
for i st i in dom (X_axis(h2)) holds p1`1<= (X_axis(h2)).i & (X_axis(
h2)).i<=p2`1
proof
let i;
assume i in dom (X_axis(h2));
then i in Seg len (X_axis(h2)) by FINSEQ_1:def 3;
then i in Seg len h2 by A101,JGRAPH_1:41;
then
A147: i in dom h2 by FINSEQ_1:def 3;
then (X_axis(h2)).i = (h2/.i)`1 by JGRAPH_1:43;
hence thesis by A145,A147;
end;
then
A148: X_axis(h2) lies_between p1`1, p2`1 by GOBOARD4:def 2;
A149: g.1 = q2 by BORSUK_2:def 4;
A150: for i st i in dom h2 holds (h2/.1)`2<=(h2/.i)`2 & (h2/.i)`2<=(h2/.len
h2)`2
proof
let i;
assume i in dom h2;
then i in Seg len h2 by FINSEQ_1:def 3;
then i in dom hb by A95,FINSEQ_1:def 3;
then
A151: h2/.i=g.(hb.i) & hb.i in rng hb by A142,FUNCT_1:def 3;
1 in Seg len hb by A95,A101,FINSEQ_1:1;
then 1 in dom hb by FINSEQ_1:def 3;
then
A152: h2/.1=g.(hb.1) by A142;
len hb in Seg len hb by A95,A101,FINSEQ_1:1;
then len hb in dom hb by FINSEQ_1:def 3;
then
A153: h2/.len h2=g.(hb.len hb) by A95,A142;
dom g =the carrier of I[01] by FUNCT_2:def 1;
then h2/.i in rng g by A92,A151,FUNCT_1:def 3;
hence thesis by A4,A8,A107,A149,A89,A90,A152,A153;
end;
for i st i in dom (Y_axis(h2)) holds (Y_axis(h2)).1<=(Y_axis(h2)).i &
(Y_axis(h2)).i <=(Y_axis(h2)).(len h2)
proof
let i;
A154: (Y_axis(h2)).1=(h2/.1)`2 & (Y_axis(h2)).len h2=(h2/.len h2)`2 by A101,
JGRAPH_1:42;
assume i in dom (Y_axis(h2));
then i in Seg len (Y_axis(h2)) by FINSEQ_1:def 3;
then i in Seg len h2 by A101,JGRAPH_1:42;
then
A155: i in dom h2 by FINSEQ_1:def 3;
then (Y_axis(h2)).i = (h2/.i)`2 by JGRAPH_1:43;
hence thesis by A150,A155,A154;
end;
then Y_axis(h2) lies_between (Y_axis(h2)).1, (Y_axis(h2)).(len h2) by
GOBOARD4:def 2;
then consider g2 being FinSequence of TOP-REAL 2 such that
A156: g2 is special and
A157: g2.1=h2.1 and
A158: g2.len g2=h2.len h2 and
A159: len g2>=len h2 and
A160: Y_axis(g2) lies_between (Y_axis(h2)).1, (Y_axis(h2)).(len h2) &
X_axis(g2) lies_between p1`1,p2`1 and
A161: for j st j in dom g2 holds ex k being Nat st k in dom
h2 & |.((g2/.j) - h2/.k).|<e and
A162: for j st 1<=j & j+1<=len g2 holds |.(g2/.j) - g2/.(j+1).|<e by A13,A101
,A148,A108,JGRAPH_1:40;
A163: len g2>=1 by A101,A159,XXREAL_0:2;
then
A164: g2/.len g2=g2.len g2 by FINSEQ_4:15;
1 in dom hb by A105,FINSEQ_3:25;
then
A165: (h2/.1)=q1 by A107,A89,A142;
A166: h2.1=h2/.1 by A105,A95,FINSEQ_4:15;
A167: h1.len h1=h1/.len h1 by A28,FINSEQ_4:15;
then
A168: X_axis(f2).len f2=(h1/.len h1)`1 by A82,A87,A88,JGRAPH_1:41
.=X_axis(h1).len h1 by A28,JGRAPH_1:41;
len h in dom h19 by A20,A28,FINSEQ_3:25;
then (h1/.len h1)=p2 by A71,A15,A20,A21,A167;
then
A169: X_axis(f2).len f2=p2`1 by A82,A87,A167,A88,JGRAPH_1:41;
5<=len f2 by A16,A20,A83,XXREAL_0:2;
then
A170: 2<=len f2 by XXREAL_0:2;
0 in dom g by A103,FUNCT_2:def 1;
then
A171: q1 in Q9 by A4,A107,FUNCT_1:def 3;
A172: f2.1=f2/.1 by A87,FINSEQ_4:15;
g2.1=g2/.1 by A163,FINSEQ_4:15;
then
A173: (Y_axis(g2)).1=(h2/.1)`2 by A157,A163,A166,JGRAPH_1:42
.=(Y_axis(h2)).1 by A101,JGRAPH_1:42;
g2/.1=g2.1 by A163,FINSEQ_4:15;
then
A174: Y_axis(g2).1=q1`2 by A157,A163,A165,A166,JGRAPH_1:42;
len hb in dom hb by A105,FINSEQ_3:25;
then (g2.len g2)=q2 by A149,A90,A95,A142,A158,A106;
then
A175: Y_axis(g2).len g2=q2`2 by A163,A164,JGRAPH_1:42;
g2.len g2=g2/.len g2 by A163,FINSEQ_4:15;
then
A176: Y_axis(g2).len g2=(h2/.len h2)`2 by A158,A163,A106,JGRAPH_1:42
.=Y_axis(h2).len h2 by A101,JGRAPH_1:42;
5<=len g2 by A91,A95,A159,XXREAL_0:2;
then
A177: 2<=len g2 by XXREAL_0:2;
1 in dom h19 by A28,FINSEQ_3:25;
then h1.1=f.(h.1) by A21;
then
A178: X_axis(f2).1=p1`1 by A30,A14,A81,A87,A172,JGRAPH_1:41;
A179: (X_axis f2).1=(h1/.1)`1 by A81,A87,A29,A172,JGRAPH_1:41
.=(X_axis h1).1 by A28,JGRAPH_1:41;
now
per cases;
case
A180: p1=p2;
0 in the carrier of I[01] by BORSUK_1:43;
then 0 in dom f by FUNCT_2:def 1;
then
A181: p1 in P by A3,A30,FUNCT_1:3;
0 in the carrier of I[01] by BORSUK_1:43;
then
A182: 0 in dom g by FUNCT_2:def 1;
then
A183: q1 in Q by A4,A107,FUNCT_1:3;
A184: for q being Point of TOP-REAL 2 st q in Q holds q`1=p1`1
proof
let q be Point of TOP-REAL 2;
assume q in Q;
then p1`1<=q`1 & q`1<= p2`1 by A6;
hence thesis by A180,XXREAL_0:1;
end;
A185: now
assume
A186: q1`2=q2`2;
q1`2<=p1`2 & p1`2<=q2`2 by A7,A181;
then
A187: p1`2=q1`2 by A186,XXREAL_0:1;
q1`1=p1`1 by A4,A107,A184,A182,FUNCT_1:3;
then q1=p1 by A187,TOPREAL3:6;
hence contradiction by A11,A183,A181,XBOOLE_0:def 4;
end;
A188: p1 in LSeg(q1,q2)
proof
1 in the carrier of I[01] by BORSUK_1:43;
then 1 in dom g by FUNCT_2:def 1;
then g.1 in rng g by FUNCT_1:3;
then p1`1<=q2`1 & q2`1<= p2`1 by A4,A6,A149;
then
A189: p1`1=q2`1 by A180,XXREAL_0:1;
set ln=(p1`2-q1`2)/(q2`2-q1`2);
A190: ln*q2`2=(p1`2-q1`2)*q2`2/(q2`2-q1`2) by XCMPLX_1:74
.=(p1`2*q2`2-q1`2*q2`2)/(q2`2-q1`2);
A191: q2`2-q1`2 <>0 by A185;
then 1-ln=(q2`2-q1`2)/(q2`2-q1`2)-(p1`2-q1`2)/(q2`2-q1`2) by
XCMPLX_1:60
.=((q2`2-q1`2)-(p1`2-q1`2))/(q2`2-q1`2) by XCMPLX_1:120
.=(q2`2-p1`2)/(q2`2-q1`2);
then
A192: (1-ln)*q1`2=(q2`2-p1`2)*q1`2/(q2`2-q1`2) by XCMPLX_1:74
.=(q2`2*q1`2-p1`2*q1`2)/(q2`2-q1`2);
0 in the carrier of I[01] by BORSUK_1:43;
then 0 in dom g by FUNCT_2:def 1;
then q1 in Q by A4,A107,FUNCT_1:3;
then p1`1<=q1`1 & q1`1<= p2`1 by A6;
then
A193: p1`1=q1`1 by A180,XXREAL_0:1;
0 in the carrier of I[01] by BORSUK_1:43;
then 0 in dom f by FUNCT_2:def 1;
then
A194: f.0 in rng f by FUNCT_1:3;
then
A195: q1`2<=p1`2 by A3,A7,A30;
A196: ((1-ln)*q1+ln*q2)`1= ((1-ln)*q1)`1+(ln*q2)`1 by TOPREAL3:2
.=(1-ln)*q1`1+(ln*q2)`1 by TOPREAL3:4
.=(1-ln)*p1`1+(ln)*p1`1 by A193,A189,TOPREAL3:4
.=p1`1;
((1-ln)*q1+ln*q2)`2=((1-ln)*q1)`2+(ln*q2)`2 by TOPREAL3:2
.=(1-ln)*q1`2+(ln*q2)`2 by TOPREAL3:4
.=(1-ln)*q1`2+ln*q2`2 by TOPREAL3:4
.=((q2`2*q1`2-p1`2*q1`2)+(p1`2*q2`2-q1`2*q2`2))/ (q2`2-q1`2) by A192
,A190,XCMPLX_1:62
.=p1`2*(q2`2-q1`2)/(q2`2-q1`2)
.=p1`2*((q2`2-q1`2)/(q2`2-q1`2)) by XCMPLX_1:74
.=p1`2*1 by A191,XCMPLX_1:60
.=p1`2;
then
A197: (1-ln)*q1+ln*q2=p1 by A196,TOPREAL3:6;
A198: p1`2<=q2`2 by A3,A7,A30,A194;
then q2`2>=q1`2 by A195,XXREAL_0:2;
then q2`2>q1`2 by A185,XXREAL_0:1;
then
A199: q2`2-q1`2>0 by XREAL_1:50;
p1`2-q1`2<=q2`2-q1`2 by A198,XREAL_1:13;
then ln<= (q2`2-q1`2)/(q2`2-q1`2) by A199,XREAL_1:72;
then
A200: ln <= 1 by A199,XCMPLX_1:60;
p1`2-q1`2>=0 by A195,XREAL_1:48;
hence thesis by A199,A200,A197;
end;
1 in the carrier of I[01] by BORSUK_1:43;
then 1 in dom g by FUNCT_2:def 1;
then
A201: q2 in Q by A4,A149,FUNCT_1:3;
Q c= LSeg(q1,q2)
proof
p1`1<=q2`1 & q2`1<= p2`1 by A6,A201;
then
A202: p1`1=q2`1 by A180,XXREAL_0:1;
p1`1<=q1`1 & q1`1<= p2`1 by A6,A183;
then
A203: p1`1=q1`1 by A180,XXREAL_0:1;
let z be object;
assume
A204: z in Q;
then reconsider qz=z as Point of TOP-REAL 2;
A205: qz`2<=q2`2 by A8,A204;
set ln=(qz`2-q1`2)/(q2`2-q1`2);
A206: ln*q2`2=(qz`2-q1`2)*q2`2/(q2`2-q1`2) by XCMPLX_1:74
.=(qz`2*q2`2-q1`2*q2`2)/(q2`2-q1`2);
A207: q2`2-q1`2 <>0 by A185;
then 1-ln=(q2`2-q1`2)/(q2`2-q1`2)-(qz`2-q1`2)/(q2`2-q1`2) by
XCMPLX_1:60
.=((q2`2-q1`2)-(qz`2-q1`2))/(q2`2-q1`2) by XCMPLX_1:120
.=(q2`2-qz`2)/(q2`2-q1`2);
then
A208: (1-ln)*q1`2=(q2`2-qz`2)*q1`2/(q2`2-q1`2) by XCMPLX_1:74
.=(q2`2*q1`2-qz`2*q1`2)/(q2`2-q1`2);
A209: ((1-ln)*q1+ln*q2)`2=((1-ln)*q1)`2+(ln*q2)`2 by TOPREAL3:2
.=(1-ln)*q1`2+(ln*q2)`2 by TOPREAL3:4
.=(1-ln)*q1`2+ln*q2`2 by TOPREAL3:4
.=((q2`2*q1`2-qz`2*q1`2)+(qz`2*q2`2-q1`2*q2`2))/ (q2`2-q1`2) by A208
,A206,XCMPLX_1:62
.=qz`2*(q2`2-q1`2)/(q2`2-q1`2)
.=qz`2*((q2`2-q1`2)/(q2`2-q1`2)) by XCMPLX_1:74
.=qz`2*1 by A207,XCMPLX_1:60
.=qz`2;
A210: p1`1<=qz`1 & qz`1<= p2`1 by A6,A204;
((1-ln)*q1+ln*q2)`1= ((1-ln)*q1)`1+(ln*q2)`1 by TOPREAL3:2
.=(1-ln)*q1`1+(ln*q2)`1 by TOPREAL3:4
.=(1-ln)*p1`1+(ln)*p1`1 by A203,A202,TOPREAL3:4
.=qz`1 by A180,A210,XXREAL_0:1;
then
A211: (1-ln)*q1+ln*q2=qz by A209,TOPREAL3:6;
A212: q1`2<=qz`2 by A8,A204;
then q2`2>=q1`2 by A205,XXREAL_0:2;
then q2`2>q1`2 by A185,XXREAL_0:1;
then
A213: q2`2-q1`2>0 by XREAL_1:50;
qz`2-q1`2<=q2`2-q1`2 by A205,XREAL_1:13;
then ln<= (q2`2-q1`2)/(q2`2-q1`2) by A213,XREAL_1:72;
then
A214: ln <= 1 by A213,XCMPLX_1:60;
qz`2-q1`2>=0 by A212,XREAL_1:48;
hence thesis by A213,A214,A211;
end;
then p1 in Q by A4,A188,Th3;
hence contradiction by A104,A11,XBOOLE_0:def 4;
end;
case
A215: p1<>p2;
A216: 1<=len hb by A91,XXREAL_0:2;
then 1 in dom hb by FINSEQ_3:25;
then
A217: h2/.1=g.(hb.1) by A142;
A218: now
0 in the carrier of I[01] by BORSUK_1:43;
then 0 in dom g by FUNCT_2:def 1;
then
A219: q1 in Q by A4,A107,FUNCT_1:3;
0 in the carrier of I[01] by BORSUK_1:43;
then
A220: 0 in dom f by FUNCT_2:def 1;
then
A221: p1 in P by A3,A30,FUNCT_1:3;
assume
A222: q1=q2;
A223: for p being Point of TOP-REAL 2 st p in P holds p`2=q1`2
proof
let p be Point of TOP-REAL 2;
assume p in P;
then q1`2<=p`2 & p`2<= q2`2 by A7;
hence thesis by A222,XXREAL_0:1;
end;
A224: now
assume
A225: p1`1=p2`1;
p1`1<=q1`1 & q1`1<=p2`1 by A6,A219;
then
A226: q1`1=p1`1 by A225,XXREAL_0:1;
p1`2=q1`2 by A3,A30,A223,A220,FUNCT_1:3;
then p1=q1 by A226,TOPREAL3:6;
hence contradiction by A11,A221,A219,XBOOLE_0:def 4;
end;
A227: q1 in LSeg(p1,p2)
proof
1 in the carrier of I[01] by BORSUK_1:43;
then 1 in dom f by FUNCT_2:def 1;
then f.1 in rng f by FUNCT_1:3;
then q1`2<=p2`2 & p2`2<= q2`2 by A3,A7,A71;
then
A228: q1`2=p2`2 by A222,XXREAL_0:1;
set ln=(q1`1-p1`1)/(p2`1-p1`1);
A229: ln*p2`1=(q1`1-p1`1)*p2`1/(p2`1-p1`1) by XCMPLX_1:74
.=(q1`1*p2`1-p1`1*p2`1)/(p2`1-p1`1);
A230: p2`1-p1`1 <>0 by A224;
then 1-ln=(p2`1-p1`1)/(p2`1-p1`1)-(q1`1-p1`1)/(p2`1-p1`1) by
XCMPLX_1:60
.=((p2`1-p1`1)-(q1`1-p1`1))/(p2`1-p1`1) by XCMPLX_1:120
.=(p2`1-q1`1)/(p2`1-p1`1);
then
A231: (1-ln)*p1`1=(p2`1-q1`1)*p1`1/(p2`1-p1`1) by XCMPLX_1:74
.=(p2`1*p1`1-q1`1*p1`1)/(p2`1-p1`1);
0 in the carrier of I[01] by BORSUK_1:43;
then 0 in dom f by FUNCT_2:def 1;
then f.0 in rng f by FUNCT_1:3;
then q1`2<=p1`2 & p1`2<= q2`2 by A3,A7,A30;
then
A232: q1`2=p1`2 by A222,XXREAL_0:1;
0 in the carrier of I[01] by BORSUK_1:43;
then 0 in dom g by FUNCT_2:def 1;
then
A233: g.0 in rng g by FUNCT_1:3;
then
A234: p1`1<=q1`1 by A4,A6,A107;
A235: ((1-ln)*p1+ln*p2)`2= ((1-ln)*p1)`2+(ln*p2)`2 by TOPREAL3:2
.=(1-ln)*p1`2+(ln*p2)`2 by TOPREAL3:4
.=(1-ln)*q1`2+(ln)*q1`2 by A232,A228,TOPREAL3:4;
((1-ln)*p1+ln*p2)`1=((1-ln)*p1)`1+(ln*p2)`1 by TOPREAL3:2
.=(1-ln)*p1`1+(ln*p2)`1 by TOPREAL3:4
.=(1-ln)*p1`1+ln*p2`1 by TOPREAL3:4
.=((p2`1*p1`1-q1`1*p1`1)+(q1`1*p2`1-p1`1*p2`1))/ (p2`1-p1`1) by
A231,A229,XCMPLX_1:62
.=q1`1*(p2`1-p1`1)/(p2`1-p1`1)
.=q1`1*((p2`1-p1`1)/(p2`1-p1`1)) by XCMPLX_1:74
.=q1`1*1 by A230,XCMPLX_1:60;
then
A236: (1-ln)*p1+ln*p2=q1 by A235,TOPREAL3:6;
A237: q1`1<=p2`1 by A4,A6,A107,A233;
then p2`1>=p1`1 by A234,XXREAL_0:2;
then p2`1>p1`1 by A224,XXREAL_0:1;
then
A238: p2`1-p1`1>0 by XREAL_1:50;
q1`1-p1`1<=p2`1-p1`1 by A237,XREAL_1:13;
then ln<= (p2`1-p1`1)/(p2`1-p1`1) by A238,XREAL_1:72;
then
A239: ln <= 1 by A238,XCMPLX_1:60;
q1`1-p1`1>=0 by A234,XREAL_1:48;
hence thesis by A238,A239,A236;
end;
1 in the carrier of I[01] by BORSUK_1:43;
then 1 in dom f by FUNCT_2:def 1;
then
A240: p2 in P by A3,A71,FUNCT_1:3;
P c= LSeg(p1,p2)
proof
q1`2<=p2`2 & p2`2<= q2`2 by A7,A240;
then
A241: q1`2=p2`2 by A222,XXREAL_0:1;
q1`2<=p1`2 & p1`2<= q2`2 by A7,A221;
then
A242: q1`2=p1`2 by A222,XXREAL_0:1;
let z be object;
assume
A243: z in P;
then reconsider pz=z as Point of TOP-REAL 2;
A244: pz`1<=p2`1 by A5,A243;
set ln=(pz`1-p1`1)/(p2`1-p1`1);
A245: ln*p2`1=(pz`1-p1`1)*p2`1/(p2`1-p1`1) by XCMPLX_1:74
.=(pz`1*p2`1-p1`1*p2`1)/(p2`1-p1`1);
A246: p2`1-p1`1 <>0 by A224;
then 1-ln=(p2`1-p1`1)/(p2`1-p1`1)-(pz`1-p1`1)/(p2`1-p1`1) by
XCMPLX_1:60
.=((p2`1-p1`1)-(pz`1-p1`1))/(p2`1-p1`1) by XCMPLX_1:120
.=(p2`1-pz`1)/(p2`1-p1`1);
then
A247: (1-ln)*p1`1=(p2`1-pz`1)*p1`1/(p2`1-p1`1) by XCMPLX_1:74
.=(p2`1*p1`1-pz`1*p1`1)/(p2`1-p1`1);
A248: ((1-ln)*p1+ln*p2)`1=((1-ln)*p1)`1+(ln*p2)`1 by TOPREAL3:2
.=(1-ln)*p1`1+(ln*p2)`1 by TOPREAL3:4
.=(1-ln)*p1`1+ln*p2`1 by TOPREAL3:4
.=((p2`1*p1`1-pz`1*p1`1)+(pz`1*p2`1-p1`1*p2`1))/ (p2`1-p1`1) by
A247,A245,XCMPLX_1:62
.=pz`1*(p2`1-p1`1)/(p2`1-p1`1)
.=pz`1*((p2`1-p1`1)/(p2`1-p1`1)) by XCMPLX_1:74
.=pz`1*1 by A246,XCMPLX_1:60
.=pz`1;
A249: q1`2<=pz`2 & pz`2<= q2`2 by A7,A243;
((1-ln)*p1+ln*p2)`2= ((1-ln)*p1)`2+(ln*p2)`2 by TOPREAL3:2
.=(1-ln)*p1`2+(ln*p2)`2 by TOPREAL3:4
.=(1-ln)*q1`2+(ln)*q1`2 by A242,A241,TOPREAL3:4
.=pz`2 by A222,A249,XXREAL_0:1;
then
A250: (1-ln)*p1+ln*p2=pz by A248,TOPREAL3:6;
A251: p1`1<=pz`1 by A5,A243;
then p2`1>=p1`1 by A244,XXREAL_0:2;
then p2`1>p1`1 by A224,XXREAL_0:1;
then
A252: p2`1-p1`1>0 by XREAL_1:50;
pz`1-p1`1<=p2`1-p1`1 by A244,XREAL_1:13;
then ln<= (p2`1-p1`1)/(p2`1-p1`1) by A252,XREAL_1:72;
then
A253: ln <= 1 by A252,XCMPLX_1:60;
pz`1-p1`1>=0 by A251,XREAL_1:48;
hence thesis by A252,A253,A250;
end;
then q1 in P by A3,A227,Th3;
hence contradiction by A171,A11,XBOOLE_0:def 4;
end;
len hb in dom hb by A216,FINSEQ_3:25;
then
A254: g2.1<>g2.len g2 by A107,A149,A89,A90,A95,A142,A157,A158,A166,A106,A218
,A217;
f2/.1<>f2/.len f2 by A30,A71,A14,A15,A20,A21,A81,A82,A29,A172,A88,A102
,A23,A215;
then L~f2 meets L~g2 by A80,A84,A156,A160,A172,A88,A178,A169,A174,A175
,A179,A168,A173,A176,A170,A177,A254,JGRAPH_1:26;
then consider s being object such that
A255: s in L~f2 and
A256: s in L~g2 by XBOOLE_0:3;
reconsider ps=s as Point of TOP-REAL 2 by A255;
ps in union{ LSeg(f2,i) : 1 <= i & i+1 <= len f2 } by A255,TOPREAL1:def 4
;
then consider x such that
A257: ps in x & x in { LSeg(f2,i) : 1 <= i & i+1 <= len f2 } by TARSKI:def 4;
ps in union{ LSeg(g2,j) : 1 <= j & j+1 <= len g2 } by A256,TOPREAL1:def 4
;
then consider y such that
A258: ps in y & y in { LSeg(g2,j) : 1 <= j & j+1 <= len g2 } by TARSKI:def 4;
consider i such that
A259: x=LSeg(f2,i) and
A260: 1 <= i and
A261: i+1 <= len f2 by A257;
LSeg(f2,i)=LSeg(f2/.i,f2/.(i+1)) by A260,A261,TOPREAL1:def 3;
then
A262: |.ps-f2/.i.|<=|.f2/.i-f2/.(i+1).| by A257,A259,JGRAPH_1:36;
i<len f2 by A261,NAT_1:13;
then i in dom f2 by A260,FINSEQ_3:25;
then consider k being Nat such that
A263: k in dom h1 and
A264: |.f2/.i - h1/.k.|<e by A85;
consider j such that
A265: y=LSeg(g2,j) and
A266: 1 <= j and
A267: j+1 <= len g2 by A258;
LSeg(g2,j)=LSeg((g2/.j),g2/.(j+1)) by A266,A267,TOPREAL1:def 3;
then
A268: |.ps-(g2/.j).|<=|.(g2/.j)-g2/.(j+1).| by A258,A265,JGRAPH_1:36;
reconsider p11=h1/.k as Point of TOP-REAL 2;
|.f2/.i-f2/.(i+1).|<e by A86,A260,A261;
then |.ps-f2/.i.|<e by A262,XXREAL_0:2;
then |.ps-h1/.k.|<=|.ps-f2/.i.|+|.f2/.i-h1/.k.| & |.ps-f2/.i.|+|.f2/.i-
h1/.k.|<e+ e by A264,TOPRNS_1:34,XREAL_1:8;
then |.ps-h1/.k.|<e+e by XXREAL_0:2;
then
A269: |.(p11-ps).|<e+e by TOPRNS_1:27;
A270: k in Seg len h1 by A263,FINSEQ_1:def 3;
then 1<=k & k<=len h1 by FINSEQ_1:1;
then h1.k=h1/.k by FINSEQ_4:15;
then
A271: h1/.k=f.(h.k) by A21,A263;
j<len g2 by A267,NAT_1:13;
then j in dom g2 by A266,FINSEQ_3:25;
then consider k9 being Nat such that
A272: k9 in dom h2 and
A273: |.((g2/.j) - h2/.k9).|<e by A161;
k9 in Seg len h2 by A272,FINSEQ_1:def 3;
then k9 in dom hb by A95,FINSEQ_1:def 3;
then
A274: hb.k9 in rng hb & h2/.k9=g.(hb.k9) by A142,FUNCT_1:def 3;
reconsider q11=h2/.k9 as Point of TOP-REAL 2;
reconsider x1=p11,x2=q11 as Point of Euclid 2 by EUCLID:22;
dom g =the carrier of I[01] by FUNCT_2:def 1;
then
A275: h2/.k9 in rng g by A92,A274,FUNCT_1:def 3;
k in dom h by A20,A270,FINSEQ_1:def 3;
then
A276: h.k in rng h by FUNCT_1:def 3;
dom f=the carrier of I[01] by FUNCT_2:def 1;
then h1/.k in P by A3,A17,A271,A276,FUNCT_1:def 3;
then min_dist_min(P9,Q9)<=dist(x1,x2) by A4,A10,A9,A275,WEIERSTR:34;
then
A277: min_dist_min(P9,Q9)<=|.(p11-q11).| by JGRAPH_1:28;
|.(g2/.j)-g2/.(j+1).|<e by A162,A266,A267;
then |.ps-(g2/.j).|<e by A268,XXREAL_0:2;
then |.ps-h2/.k9.|<=|.ps-(g2/.j).|+|.(g2/.j)-h2/.k9.| & |.ps-(g2/.j).|+
|.(g2/.j)- (h2/.k9).|<e+e by A273,TOPRNS_1:34,XREAL_1:8;
then |.ps-(h2/.k9).|<e+e by XXREAL_0:2;
then |.(p11-q11).|<= |.(p11-ps).|+|.(ps-q11).| & |.(p11-ps).|+|.(ps-q11
).| <e+e+( e+e) by A269,TOPRNS_1:34,XREAL_1:8;
then |.(p11-q11).|<e+e+e+e by XXREAL_0:2;
then min_dist_min(P9,Q9)<4*e by A277,XXREAL_0:2;
then 4*e-5*e>0 by XREAL_1:50;
then (4-5)*e/e>0 by A13,XREAL_1:139;
then 4-5>0 by A12;
hence contradiction;
end;
end;
hence contradiction;
end;
:: Fashoda Meet Theorem
theorem Th5:
for f,g being continuous Function of I[01],TOP-REAL 2, O,I being
Point of I[01] st O=0 & I=1 & (f.O)`1=a & (f.I)`1=b & (g.O)`2=c & (g.I)`2=d & (
for r being Point of I[01] holds a <=(f.r)`1 & (f.r)`1<=b & a <=(g.r)`1 & (g.r)
`1<=b & c <=(f.r)`2 & (f.r)`2<=d & c <=(g.r)`2 & (g.r)`2<=d) holds rng f meets
rng g
proof
let f,g be continuous Function of I[01],TOP-REAL 2, O,I be Point of I[01];
assume that
A1: O=0 & I=1 and
A2: (f.O)`1=a and
A3: (f.I)`1=b and
A4: (g.O)`2=c and
A5: (g.I)`2=d and
A6: for r being Point of I[01] holds a<=(f.r)`1 & (f.r)`1<=b & a<=(g.r)
`1 & (g.r)`1<=b & c <=(f.r)`2 & (f.r)`2<=d & c <=(g.r)`2 & (g.r)`2<=d;
reconsider Q=rng g as non empty Subset of TOP-REAL 2;
A7: the carrier of ((TOP-REAL 2)|Q)=[#]((TOP-REAL 2)|Q)
.=rng g by PRE_TOPC:def 5;
dom g=the carrier of I[01] by FUNCT_2:def 1;
then reconsider g1=g as Function of I[01],((TOP-REAL 2)|Q) by A7,FUNCT_2:1;
reconsider q2=g1.I as Point of TOP-REAL 2 by A5;
reconsider q1=g1.O as Point of TOP-REAL 2 by A4;
reconsider P=rng f as non empty Subset of TOP-REAL 2;
A8: the carrier of ((TOP-REAL 2)|P)=[#]((TOP-REAL 2)|P)
.=rng f by PRE_TOPC:def 5;
dom f=the carrier of I[01] by FUNCT_2:def 1;
then reconsider f1=f as Function of I[01],((TOP-REAL 2)|P) by A8,FUNCT_2:1;
reconsider p2=f1.I as Point of TOP-REAL 2 by A3;
reconsider p1=f1.O as Point of TOP-REAL 2 by A2;
A9: for p being Point of TOP-REAL 2 st p in P holds p1`1<=p`1 & p`1<= p2`1
proof
let p be Point of TOP-REAL 2;
assume p in P;
then ex x being object st x in dom f1 & p=f1.x by FUNCT_1:def 3;
hence thesis by A2,A3,A6;
end;
A10: for p being Point of TOP-REAL 2 st p in P holds q1`2<=p`2 & p`2<= q2`2
proof
let p be Point of TOP-REAL 2;
assume p in P;
then ex x being object st x in dom f1 & p=f1.x by FUNCT_1:def 3;
hence thesis by A4,A5,A6;
end;
A11: for p being Point of TOP-REAL 2 st p in Q holds q1`2<=p`2 & p`2<= q2`2
proof
let p be Point of TOP-REAL 2;
assume p in Q;
then ex x being object st x in dom g1 & p=g1.x by FUNCT_1:def 3;
hence thesis by A4,A5,A6;
end;
A12: for p being Point of TOP-REAL 2 st p in Q holds p1`1<=p`1 & p`1<= p2`1
proof
let p be Point of TOP-REAL 2;
assume p in Q;
then ex x being object st x in dom g1 & p=g1.x by FUNCT_1:def 3;
hence thesis by A2,A3,A6;
end;
f is Path of p1,p2 & g is Path of q1,q2 by A1,BORSUK_2:def 4;
hence thesis by A9,A12,A10,A11,Th4;
end;
theorem
for ar, br, cr, dr being Point of Trectangle(a,b,c,d) for h being Path
of ar,br, v being Path of dr,cr for Ar, Br, Cr, Dr being Point of TOP-REAL 2 st
Ar`1 = a & Br`1 = b & Cr`2 = c & Dr`2 = d & ar = Ar & br = Br & cr = Cr & dr =
Dr ex s, t being Point of I[01] st h.s = v.t
proof
let ar, br, cr, dr be Point of Trectangle(a,b,c,d);
let h be Path of ar,br;
let v be Path of dr,cr;
let Ar, Br, Cr, Dr be Point of TOP-REAL 2 such that
A1: Ar`1 = a & Br`1 = b & Cr`2 = c & Dr`2 = d & ar = Ar & br = Br & cr =
Cr & dr = Dr;
set TR = Trectangle(a,b,c,d);
per cases;
suppose
A2: TR is empty;
take 1[01], 1[01];
thus thesis by A2;
end;
suppose
TR is non empty;
then reconsider TR = Trectangle(a,b,c,d) as non empty convex SubSpace of
TOP-REAL 2;
reconsider ar, br, cr, dr as Point of TR;
reconsider h as Path of ar,br;
reconsider v as Path of dr,cr;
A3: h.0 = ar & h.1 = br by BORSUK_2:def 4;
the carrier of TR is Subset of TOP-REAL 2 by TSEP_1:1;
then reconsider f = h, g = -v as Function of I[01],TOP-REAL 2 by FUNCT_2:7;
A4: (-v).0 = cr & (-v).1 = dr by BORSUK_2:def 4;
A5: for r being Point of I[01] holds a <= (f.r)`1 & (f.r)`1 <= b & a <= (g
.r)`1 & (g.r)`1 <= b & c <= (f.r)`2 & (f.r)`2 <= d & c <= (g.r)`2 & (g.r)`2 <=
d
proof
let r be Point of I[01];
A6: the carrier of TR = closed_inside_of_rectangle(a,b,c,d) by PRE_TOPC:8
.= {p where p is Point of TOP-REAL 2: a <= p`1 & p`1 <= b & c <= p`2
& p`2 <= d} by JGRAPH_6:def 2;
(-v).r in the carrier of TR;
then
A7: ex p being Point of TOP-REAL 2 st (-v).r = p & a <= p`1 & p`1 <= b
& c <= p`2 & p`2 <= d by A6;
h.r in the carrier of TR;
then
ex p being Point of TOP-REAL 2 st h.r = p & a <= p`1 & p`1 <= b & c
<= p`2 & p`2 <= d by A6;
hence thesis by A7;
end;
f is continuous & g is continuous by PRE_TOPC:26;
then rng f meets rng g by A1,A3,A4,A5,Th5,BORSUK_1:def 14,def 15;
then consider y being object such that
A8: y in rng f and
A9: y in rng g by XBOOLE_0:3;
consider t being object such that
A10: t in dom g and
A11: g.t = y by A9,FUNCT_1:def 3;
consider s being object such that
A12: s in dom f and
A13: f.s = y by A8,FUNCT_1:def 3;
reconsider s, t as Point of I[01] by A12,A10;
reconsider t1 = 1-t as Point of I[01] by JORDAN5B:4;
take s, t1;
dr,cr are_connected by BORSUK_2:def 3;
hence thesis by A13,A11,BORSUK_2:def 6;
end;
end;