:: 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-2016 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, TOPALG_2;
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 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 by EUCLID:52;
A8: (1-l)*w1=|[ (1-l)*w1`1 ,(1-l)*w1`2 ]| by EUCLID:57;
then ((1-l)*w1)`2= (1-l)*w1`2 by EUCLID:52;
then w`2=(1-l)* w1`2+ l* w2`2 by A5,A7,EUCLID:52;
then
A9: c <= w`2 & w`2 <= d by A2,A4,XREAL_1:173,174;
A10: (l*w2)`1=l*w2`1 by A6,EUCLID:52;
((1-l)*w1)`1= (1-l)*w1`1 by A8,EUCLID:52;
then w`1=(1-l)* w1`1+ l* w2`1 by A5,A10,EUCLID:52;
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 & i0 by XREAL_1:215;
f is uniformly_continuous by UNIFORM1:8,A4;
then consider s1 being Real such that
A7: 0) 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 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 & i0 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 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)~~=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{} 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~~~~=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=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).|=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).|=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=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)) .|=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).|=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;
i0 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;
~~