Copyright (c) 1998 Association of Mizar Users
environ
vocabulary BOOLE, ARYTM_1, FINSEQ_1, MATRIX_1, MATRIX_2, PRE_TOPC, EUCLID,
ARYTM_3, TOPREAL1, METRIC_1, RELAT_2, JORDAN1, CONNSP_1, PCOMPS_1,
SPPOL_1, MCART_1, GOBOARD1, TREES_1, PSCOMP_1, SPRECT_1, COMPTS_1,
JORDAN3, RELAT_1, SPPOL_2, FUNCT_1, TARSKI, RFINSEQ, GROUP_2, SEQM_3,
GOBOARD5, GOBOARD9, SUBSET_1, TOPREAL4, JORDAN5D, GOBOARD2, SPRECT_2,
ABSVALUE, CARD_1, ORDINAL2, TOPS_1, JORDAN5C, FINSEQ_5, FINSEQ_4, ARYTM;
notation TARSKI, XBOOLE_0, ENUMSET1, ZFMISC_1, SUBSET_1, ORDINAL1, XREAL_0,
REAL_1, NAT_1, ABSVALUE, BINARITH, CARD_1, RFINSEQ, FUNCT_1, FINSEQ_1,
FINSEQ_4, FINSEQ_5, MATRIX_1, MATRIX_2, STRUCT_0, METRIC_1, PRE_TOPC,
TOPS_1, COMPTS_1, CONNSP_1, PCOMPS_1, EUCLID, TOPREAL1, TOPREAL4,
JORDAN1, PSCOMP_1, GOBOARD1, GOBOARD2, SPPOL_1, SPPOL_2, GOBOARD5,
GOBOARD9, JORDAN3, JORDAN5C, JORDAN5D, SPRECT_1, SPRECT_2;
constructors SPRECT_2, PSCOMP_1, REALSET1, SPRECT_1, SPPOL_1, COMPTS_1,
REAL_1, GOBOARD2, BINARITH, JORDAN3, TOPREAL2, TOPREAL4, GOBOARD9,
CONNSP_1, TOPS_1, JORDAN1, JORDAN5C, TOPS_2, MATRIX_2, ENUMSET1,
JORDAN5D, ABSVALUE, RFINSEQ, FINSEQ_4, TOPMETR, MEMBERED;
clusters STRUCT_0, RELSET_1, SPRECT_1, SPRECT_2, EUCLID, SPPOL_2, GOBOARD2,
XREAL_0, FINSEQ_5, ARYTM_3, MEMBERED, ZFMISC_1;
requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM;
definitions TARSKI, SPRECT_2, JORDAN1, TOPREAL4, GOBOARD1, XBOOLE_0;
theorems FINSEQ_4, TARSKI, FINSEQ_3, FINSEQ_1, SPRECT_2, GOBOARD7, PSCOMP_1,
SPRECT_1, TOPREAL3, AXIOMS, REAL_1, REAL_2, SPPOL_2, NAT_1, SPPOL_1,
EUCLID, ZFMISC_1, TOPREAL1, GOBOARD5, JORDAN5D, FINSEQ_5, AMI_5,
FINSEQ_6, JORDAN4, JORDAN3, TOPREAL5, TOPS_1, GOBRD11, GOBOARD9, TOPMETR,
GOBOARD6, JORDAN1, CONNSP_1, SUBSET_1, GOBRD12, JORDAN5C, JORDAN6,
CQC_THE1, MATRIX_2, SCMFSA_7, GOBOARD1, ENUMSET1, CARD_2, GOBOARD2,
SQUARE_1, BINARITH, NAT_2, ABSVALUE, GOBOARD8, RLVECT_1, PARTFUN2,
FUNCT_1, XBOOLE_0, XBOOLE_1, XREAL_0, XCMPLX_1, FINSEQ_2;
schemes DOMAIN_1;
begin :: Preliminaries
reserve i,j,k,n,m for Nat;
canceled;
theorem
for A,B,C,p being set st A c= B & B /\ C = {p} & p in A
holds A /\ C = {p}
proof
let A,B,C,p be set such that
A1: A c= B;
assume
A2: B /\ C = {p};
then p in B /\ C by TARSKI:def 1;
then A3: p in C by XBOOLE_0:def 3;
assume p in A;
then A4: p in A /\ C by A3,XBOOLE_0:def 3;
A /\ C c= { p } by A1,A2,XBOOLE_1:26;
hence A /\ C = {p} by A4,ZFMISC_1:39;
end;
theorem Th3:
for q,r,s,t being Real st t >= 0 & t <= 1 &
s = (1-t)*q + t*r & q <= s & r < s
holds t = 0
proof let q,r,s,t be Real such that
A1: t >= 0 and
A2: t <= 1 and
A3: s = (1-t)*q + t*r and
A4: q <= s and
A5: r < s;
A6: 1*s = ((1-t) + t)*s by XCMPLX_1:27
.= (1-t)*s + t*s by XCMPLX_1:8;
assume t <> 0;
then A7: t*r < t*s by A1,A5,REAL_1:70;
1-t >= 0 by A2,SQUARE_1:12;
then (1-t)*q <= (1-t)*s by A4,AXIOMS:25;
hence contradiction by A3,A6,A7,REAL_1:67;
end;
theorem Th4:
for q,r,s,t being Real st t >= 0 & t <= 1 &
s = (1-t)*q + t*r & q >= s & r > s
holds t = 0
proof let q,r,s,t be Real such that
A1: t >= 0 and
A2: t <= 1 and
A3: s = (1-t)*q + t*r and
A4: q >= s and
A5: r > s;
A6: 1*s = ((1-t) + t)*s by XCMPLX_1:27
.= (1-t)*s + t*s by XCMPLX_1:8;
assume t <> 0;
then A7: t*r > t*s by A1,A5,REAL_1:70;
1-t >= 0 by A2,SQUARE_1:12;
then (1-t)*q >= (1-t)*s by A4,AXIOMS:25;
hence contradiction by A3,A6,A7,REAL_1:67;
end;
theorem Th5:
i-'k <= j implies i <= j + k
proof assume
A1: i-'k <= j;
per cases;
suppose
A2: i >= k;
i-'k +k <= j + k by A1,AXIOMS:24;
hence i <= j + k by A2,AMI_5:4;
suppose
A3: i <= k;
k <= j + k by NAT_1:29;
hence i <= j + k by A3,AXIOMS:22;
end;
theorem Th6:
i <= j + k implies i-'k <= j
proof assume i <= j + k;
then i -' k <= j + k -' k by JORDAN3:5;
hence i-'k <= j by BINARITH:39;
end;
theorem Th7:
i <= j -' k & k <= j implies i + k <= j
proof assume that
A1: i <= j -' k and
A2: j >= k;
i + k <= j -' k + k by A1,AXIOMS:24;
hence i + k <= j by A2,AMI_5:4;
end;
theorem
j + k <= i implies k <= i -' j
proof assume
A1: j + k <= i;
per cases by A1,AXIOMS:21;
suppose j + k = i;
hence k <= i -' j by BINARITH:39;
suppose j + k < i;
hence k <= i -' j by Th5;
end;
theorem
k <= i & i < j implies i -' k < j -' k
proof assume that
A1: k <= i and
A2: i < j;
A3: k <= j by A1,A2,AXIOMS:22;
i -' k + k = i by A1,AMI_5:4;
then i -' k + k < j -' k + k by A2,A3,AMI_5:4;
hence i -' k < j -' k by AXIOMS:24;
end;
theorem
i < j & k < j implies i -' k < j -' k
proof assume that
A1: i < j and
A2: k < j;
per cases;
suppose k <= i;
then A3: i -' k = i - k by SCMFSA_7:3;
j -' k = j - k by A2,SCMFSA_7:3;
hence thesis by A1,A3,REAL_1:54;
suppose k > i;
then i - k < 0 by REAL_2:105;
then A4: i -' k = 0 by BINARITH:def 3;
j -' k <> 0 by A2,JORDAN4:1;
hence thesis by A4,NAT_1:19;
end;
theorem
for D being non empty set
for f being non empty FinSequence of D, g being FinSequence of D
holds (g^f)/.len(g^f) = f/.len f
proof
let D be non empty set,
f be non empty FinSequence of D, g be FinSequence of D;
A1: len(g^f) = len g + len f by FINSEQ_1:35;
len f <> 0 by FINSEQ_1:25;
then len f >= 1 by RLVECT_1:99;
hence thesis by A1,GOBOARD2:5;
end;
theorem Th12:
for a,b,c,d being set holds
Indices (a,b)][(c,d) = {[1,1],[1,2],[2,1],[2,2]}
proof let a,b,c,d be set;
thus Indices (a,b)][(c,d) = [:Seg 2,Seg 2:] by MATRIX_2:3
.= [:{1},Seg 2:] \/ [:{2},Seg 2:] by FINSEQ_1:4,ZFMISC_1:132
.= [:{1},Seg 2:] \/ {[2,1], [2,2]} by FINSEQ_1:4,ZFMISC_1:36
.= { [1,1], [1,2]} \/ {[2,1], [2,2]} by FINSEQ_1:4,ZFMISC_1:36
.= {[1,1],[1,2],[2,1],[2,2]} by ENUMSET1:45;
end;
begin :: Euclidean Space
theorem Th13:
for p,q being Point of TOP-REAL n, r being Real
st 0 < r & p = (1-r)*p+r*q
holds p = q
proof
let p,q be Point of TOP-REAL n, r be Real such that
A1: 0 < r and
A2: p = (1-r)*p+r*q;
A3: (1-r)*p+r*p = ((1-r)+r)*p by EUCLID:37
.= 1*p by XCMPLX_1:27
.= p by EUCLID:33;
r*p = r*p + 0.REAL n by EUCLID:31
.= r*p + ((1-r)*p + -(1-r)*p) by EUCLID:40
.= r*q + (1-r)*p + -(1-r)*p by A2,A3,EUCLID:30
.= r*q + ((1-r)*p + -(1-r)*p) by EUCLID:30
.= r*q + 0.REAL n by EUCLID:40
.= r*q by EUCLID:31;
hence p = q by A1,EUCLID:38;
end;
theorem Th14:
for p,q being Point of TOP-REAL n, r being Real
st r < 1 & p = (1-r)*q+r*p
holds p = q
proof let p,q be Point of TOP-REAL n, r be Real such that
A1: r < 1 and
A2: p = (1-r)*q+r*p;
set s = 1 -r;
r + 0 < 1 by A1;
then A3: 0 < 1 - r by REAL_1:86;
p = (1-s)*p+s*q by A2,XCMPLX_1:18;
hence p = q by A3,Th13;
end;
theorem
for p,q being Point of TOP-REAL n st p = 1/2*(p+q)
holds p = q
proof let p,q be Point of TOP-REAL n;
assume p = 1/2*(p+q);
then p = (1 - 1/2)*p + 1/2*q by EUCLID:36;
hence p = q by Th13;
end;
theorem Th16:
for p,q,r being Point of TOP-REAL n st
q in LSeg(p,r) & r in LSeg(p,q) holds q = r
proof let p,q,r be Point of TOP-REAL n;
assume q in LSeg(p,r);
then consider r1 being Real such that
A1: 0<=r1 and
A2: r1<=1 and
A3: q = (1-r1)*p+r1*r by SPPOL_1:21;
assume r in LSeg(p,q);
then consider r2 being Real such that
A4: 0<=r2 and
A5: r2<=1 and
A6: r = (1-r2)*p+r2*q by SPPOL_1:21;
A7: (1-r1)+r1*(1-r2) = (1-r1)+(r1*1-r1*r2) by XCMPLX_1:40
.= (1-r1)+r1-r1*r2 by XCMPLX_1:29
.= 1 - r1*r2 by XCMPLX_1:27;
A8: (1-r2)+r2*(1-r1) = (1-r2)+(r2*1-r2*r1) by XCMPLX_1:40
.= (1-r2)+r2-r2*r1 by XCMPLX_1:29
.= 1 - r2*r1 by XCMPLX_1:27;
A9: q = (1-r1)*p+(r1*((1-r2)*p)+r1*(r2*q)) by A3,A6,EUCLID:36
.= (1-r1)*p+r1*((1-r2)*p)+r1*(r2*q) by EUCLID:30
.= (1-r1)*p+r1*(1-r2)*p+r1*(r2*q) by EUCLID:34
.= (1 - r1*r2)*p+r1*(r2*q) by A7,EUCLID:37
.= (1 - r1*r2)*p+r1*r2*q by EUCLID:34;
A10: r = (1-r2)*p+(r2*((1-r1)*p)+r2*(r1*r)) by A3,A6,EUCLID:36
.= (1-r2)*p+r2*((1-r1)*p)+r2*(r1*r) by EUCLID:30
.= (1-r2)*p+r2*(1-r1)*p+r2*(r1*r) by EUCLID:34
.= (1 - r2*r1)*p+r2*(r1*r) by A8,EUCLID:37
.= (1 - r2*r1)*p+r2*r1*r by EUCLID:34;
A11: r1*r2 <= 1 by A1,A2,A4,A5,REAL_2:140;
per cases by A11,REAL_1:def 5;
suppose
A12: r1*r2 = 1;
then 1 <= r1 or 1 <= r2 by A1,A4,REAL_2:139;
then 1*r1 = 1 or 1*r2 = 1 by A2,A5,AXIOMS:21;
hence q = 0 * p+r by A3,A12,EUCLID:33
.= 0.REAL n+r by EUCLID:33
.= r by EUCLID:31;
suppose
A13: r1*r2 < 1;
hence q = p by A9,Th14
.= r by A10,A13,Th14;
end;
begin :: Euclidean Plane
theorem Th17:
for A being non empty Subset of TOP-REAL 2,
p being Element of Euclid 2, r being Real st A = Ball(p,r)
holds A is connected
proof
let A be non empty Subset of TOP-REAL 2,
p be Element of Euclid 2, r be Real such that
A1: A = Ball(p,r);
A is convex
proof let w1,w2 be Point of TOP-REAL 2;
assume w1 in A & w2 in A;
hence LSeg(w1,w2) c= A by A1,TOPREAL3:28;
end;
hence A is connected by JORDAN1:9;
end;
theorem Th18:
for A, B being Subset of TOP-REAL 2 st
A is open & B is_a_component_of A
holds B is open
proof let A, B be Subset of TOP-REAL 2 such that
A1: A is open and
A2: B is_a_component_of A;
A3: B c= A by A2,SPRECT_1:7;
A4: TOP-REAL 2 = TopSpaceMetr (Euclid 2) by EUCLID:def 8;
reconsider C = B, D = A
as Subset of TopSpaceMetr Euclid 2 by EUCLID:def 8;
for p being Point of Euclid 2 st p in C
ex r being real number st r>0 & Ball(p,r) c= C
proof let p be Point of Euclid 2; assume
A5: p in C;
then consider r being real number such that
A6: r > 0 and
A7: Ball(p,r) c= D by A1,A3,A4,TOPMETR:22;
reconsider r as Real by XREAL_0:def 1;
take r;
thus r>0 by A6;
the carrier of TopSpaceMetr Euclid 2 = the carrier of Euclid 2
by TOPMETR:16;
then reconsider E = Ball(p,r) as Subset of TOP-REAL 2 by A4;
A8: p in E by A6,GOBOARD6:4;
then A9: B meets E by A5,XBOOLE_0:3;
E is connected by A8,Th17;
hence Ball(p,r) c= C by A2,A7,A9,GOBOARD9:6;
end;
hence B is open by A4,TOPMETR:22;
end;
theorem Th19:
for p,q,r being Point of TOP-REAL 2
st LSeg(p,q) is horizontal & r in LSeg(p,q)
holds p`2 = r`2
proof let p,q,r be Point of TOP-REAL 2;
assume LSeg(p,q) is horizontal;
then A1: p`2 = q`2 by SPPOL_1:36;
assume r in LSeg(p,q);
then consider t being Real such that
0 <= t & t <= 1 and
A2: r = (1-t)*p+t*q by SPPOL_1:21;
thus p`2 = 1*p`2
.= (1-t+t)*p`2 by XCMPLX_1:27
.= (1-t)*p`2+t*p`2 by XCMPLX_1:8
.= ((1-t)*p)`2+t*q`2 by A1,TOPREAL3:9
.= ((1-t)*p)`2+(t*q)`2 by TOPREAL3:9
.= r`2 by A2,TOPREAL3:7;
end;
theorem Th20:
for p,q,r being Point of TOP-REAL 2
st LSeg(p,q) is vertical & r in LSeg(p,q)
holds p`1 = r`1
proof let p,q,r be Point of TOP-REAL 2;
assume LSeg(p,q) is vertical;
then A1: p`1 = q`1 by SPPOL_1:37;
assume r in LSeg(p,q);
then consider t being Real such that
0 <= t & t <= 1 and
A2: r = (1-t)*p+t*q by SPPOL_1:21;
thus p`1 = 1*p`1
.= (1-t+t)*p`1 by XCMPLX_1:27
.= (1-t)*p`1+t*p`1 by XCMPLX_1:8
.= ((1-t)*p)`1+t*q`1 by A1,TOPREAL3:9
.= ((1-t)*p)`1+(t*q)`1 by TOPREAL3:9
.= r`1 by A2,TOPREAL3:7;
end;
theorem
for p,q,r,s being Point of TOP-REAL 2
st LSeg(p,q) is horizontal & LSeg(r,s) is horizontal &
LSeg(p,q) meets LSeg(r,s)
holds p`2= r`2
proof
let p,q,r,s be Point of TOP-REAL 2 such that
A1: LSeg(p,q) is horizontal and
A2: LSeg(r,s) is horizontal;
assume LSeg(p,q) meets LSeg(r,s);
then LSeg(p,q) /\ LSeg(r,s) <> {} by XBOOLE_0:def 7;
then consider x being Point of TOP-REAL 2 such that
A3: x in LSeg(p,q) /\ LSeg(r,s) by SUBSET_1:10;
A4: x in LSeg(r,s) by A3,XBOOLE_0:def 3;
x in LSeg(p,q) by A3,XBOOLE_0:def 3;
hence p`2 = x`2 by A1,Th19
.= r`2 by A2,A4,Th19;
end;
theorem
for p,q,r being Point of TOP-REAL 2
st LSeg(p,q) is vertical & LSeg(q,r) is horizontal
holds LSeg(p,q) /\ LSeg(q,r) = {q}
proof let p,q,r be Point of TOP-REAL 2 such that
A1: LSeg(p,q) is vertical and
A2: LSeg(q,r) is horizontal;
for x being set holds x in LSeg(p,q) /\ LSeg(q,r) iff x = q
proof let x be set;
thus x in LSeg(p,q) /\ LSeg(q,r) implies x = q
proof assume
A3: x in LSeg(p,q) /\ LSeg(q,r);
then reconsider x as Point of TOP-REAL 2;
x in LSeg(p,q) & x in LSeg(q,r) by A3,XBOOLE_0:def 3;
then x`1 = q`1 & x`2 = q`2 by A1,A2,Th19,Th20;
hence thesis by TOPREAL3:11;
end;
assume x = q;
then x in LSeg(p,q) & x in LSeg(q,r) by TOPREAL1:6;
hence thesis by XBOOLE_0:def 3;
end;
hence LSeg(p,q) /\ LSeg(q,r) = {q} by TARSKI:def 1;
end;
theorem
for p,q,r,s being Point of TOP-REAL 2
st LSeg(p,q) is horizontal & LSeg(s,r) is vertical & r in LSeg(p,q)
holds LSeg(p,q) /\ LSeg(s,r) = {r}
proof let p,q,r,s be Point of TOP-REAL 2 such that
A1: LSeg(p,q) is horizontal and
A2: LSeg(s,r) is vertical and
A3: r in LSeg(p,q);
for x being set holds x in LSeg(p,q) /\ LSeg(s,r) iff x = r
proof let x be set;
thus x in LSeg(p,q) /\ LSeg(s,r) implies x = r
proof assume
A4: x in LSeg(p,q) /\ LSeg(s,r);
then reconsider x as Point of TOP-REAL 2;
A5: p`2 = r`2 by A1,A3,Th19;
x in LSeg(p,q) & x in LSeg(s,r) by A4,XBOOLE_0:def 3;
then x`2 = p`2 & x`1 = r`1 by A1,A2,Th19,Th20;
hence thesis by A5,TOPREAL3:11;
end;
assume x = r;
then x in LSeg(p,q) & x in LSeg(s,r) by A3,TOPREAL1:6;
hence thesis by XBOOLE_0:def 3;
end;
hence LSeg(p,q) /\ LSeg(s,r) = {r} by TARSKI:def 1;
end;
begin :: Main
reserve p,q for Point of TOP-REAL 2;
reserve G for Go-board;
theorem
1 <= j & j <= k & k <= width G & 1 <= i & i <= len G
implies G*(i,j)`2 <= G*(i,k)`2
proof
assume
A1: 1 <= j & j <= k & k <= width G & 1 <= i & i <= len G;
per cases by A1,REAL_1:def 5;
suppose j < k;
hence G*(i,j)`2 <= G*(i,k)`2 by A1,GOBOARD5:5;
suppose j = k;
hence thesis;
end;
theorem
1 <= j & j <= width G & 1 <= i & i <= k & k <= len G
implies G*(i,j)`1 <= G*(k,j)`1
proof assume
A1: 1 <= j & j <= width G & 1 <= i & i <= k & k <= len G;
per cases by A1,REAL_1:def 5;
suppose i < k;
hence G*(i,j)`1 <= G*(k,j)`1 by A1,GOBOARD5:4;
suppose i = k;
hence thesis;
end;
reserve C for Subset of TOP-REAL 2;
theorem Th26:
LSeg(NW-corner C,NE-corner C) c= L~SpStSeq C
proof
A1: LSeg(NW-corner C,NE-corner C) c=
LSeg(NW-corner C,NE-corner C) \/ LSeg(NE-corner C,SE-corner C) by XBOOLE_1:7;
LSeg(NW-corner C,NE-corner C) \/ LSeg(NE-corner C,SE-corner C) c=
(LSeg(NW-corner C,NE-corner C) \/ LSeg(NE-corner C,SE-corner C)) \/
(LSeg(SE-corner C,SW-corner C) \/ LSeg(SW-corner C,NW-corner C)) by XBOOLE_1:
7;
then LSeg(NW-corner C,NE-corner C) c=
(LSeg(NW-corner C,NE-corner C) \/ LSeg(NE-corner C,SE-corner C)) \/
(LSeg(SE-corner C,SW-corner C) \/ LSeg(SW-corner C,NW-corner C))
by A1,XBOOLE_1:1;
hence thesis by SPRECT_1:43;
end;
theorem Th27:
N-most C c= LSeg(NW-corner C,NE-corner C)
proof
N-most C = LSeg(NW-corner C, NE-corner C) /\ C by PSCOMP_1:def 39;
hence N-most C c= LSeg(NW-corner C,NE-corner C) by XBOOLE_1:17;
end;
theorem Th28:
for C being non empty compact Subset of TOP-REAL 2
holds N-min C in LSeg(NW-corner C,NE-corner C)
proof let C be non empty compact Subset of TOP-REAL 2;
A1: N-min C in N-most C by PSCOMP_1:101;
N-most C c= LSeg(NW-corner C,NE-corner C) by Th27;
hence N-min C in LSeg(NW-corner C,NE-corner C) by A1;
end;
theorem
LSeg(NW-corner C,NE-corner C) is horizontal
proof
(NW-corner C)`2 = N-bound C by PSCOMP_1:75
.= (NE-corner C)`2 by PSCOMP_1:77;
hence LSeg(NW-corner C,NE-corner C) is horizontal by SPPOL_1:36;
end;
canceled;
theorem :: JORDAN3:76
for g being FinSequence of TOP-REAL 2, p being Point of TOP-REAL 2 st
g/.1 <> p & ((g/.1)`1 = p`1 or (g/.1)`2 = p`2) &
g is_S-Seq & LSeg(p,g/.1) /\ L~g={ g/.1 }
holds <*p*>^g is_S-Seq
proof let g be FinSequence of TOP-REAL 2, p be Point of TOP-REAL 2 such that
A1: g/.1 <> p and
A2: (g/.1)`1 = p`1 or (g/.1)`2 = p`2 and
A3: g is_S-Seq and
A4: LSeg(p,g/.1) /\ L~g={ g/.1 };
set f = <*p,g/.1*>;
reconsider g' = g as S-Sequence_in_R2 by A3;
A5: 1 in dom g' by FINSEQ_5:6;
A6: len f = 1+1 by FINSEQ_1:61;
then A7: len f -' 1 = 1 by BINARITH:39;
A8: f.len f = g/.1 by A6,FINSEQ_1:61
.= g.1 by A5,FINSEQ_4:def 4;
A9: f is_S-Seq by A1,A2,SPPOL_2:46;
A10: L~f /\ L~g ={ g/.1 } by A4,SPPOL_2:21
.={g.1} by A5,FINSEQ_4:def 4;
mid(f,1,len f-'1) = <*f/.1*> by A6,A7,JORDAN4:27
.= <*p*> by FINSEQ_4:26;
hence <*p*>^g is_S-Seq by A3,A8,A9,A10,JORDAN3:80;
end;
canceled;
theorem
for f being S-Sequence_in_R2, p being Point of TOP-REAL 2 st
1 <j & j <= len f & p in L~mid(f,1,j)
holds LE p, f/.j, L~f, f/.1, f/.len f
proof
let f be S-Sequence_in_R2, p be Point of TOP-REAL 2 such that
A1: 1 <j & j <= len f and
A2: p in L~mid(f,1,j);
A3: L~f is_an_arc_of f/.1,f/.len f by TOPREAL1:31;
consider i such that
A4: 1 <= i & i+1 <= len mid(f,1,j) and
A5: p in LSeg(mid(f,1,j),i) by A2,SPPOL_2:13;
A6: j -' 1 + 1 = j by A1,AMI_5:4;
then A7: i+1 <= j by A1,A4,JORDAN4:20;
A8: i = i + 1 -' 1 by BINARITH:39;
i < j-'1+1 by A6,A7,NAT_1:38;
then A9: LSeg(mid(f,1,j),i) = LSeg(f,i+1-'1) by A1,A4,JORDAN4:31;
i+1 <= len f by A1,A7,AXIOMS:22;
then A10: LE p, f/.(i+1), L~f, f/.1, f/.len f by A4,A5,A8,A9,JORDAN5C:26;
1 <= i+1 by NAT_1:29;
then LE f/.(i+1), f/.j, L~f, f/.1, f/.len f by A1,A7,JORDAN5C:24;
hence LE p, f/.j, L~f, f/.1, f/.len f by A3,A10,JORDAN5C:13;
end;
theorem :: JORDAN4:47
for h being FinSequence of TOP-REAL 2 st
i in dom h & j in dom h holds L~mid(h,i,j) c= L~h
proof let h be FinSequence of TOP-REAL 2;
assume i in dom h & j in dom h;
then 1 <= i & i <= len h & 1 <= j & j <= len h by FINSEQ_3:27;
hence thesis by JORDAN4:47;
end;
theorem
1 <= i & i < j implies
for f being FinSequence of TOP-REAL 2 st j <= len f holds
L~mid(f,i,j) = LSeg(f,i) \/ L~mid(f,i+1,j)
proof assume that
A1: 1 <= i and
A2: i < j;
let f be FinSequence of TOP-REAL 2 such that
A3: j <= len f;
A4: 1 <= i+1 by NAT_1:29;
A5: i+1 <= j by A2,NAT_1:38;
set A = { LSeg(f,k): i <= k & k < j},
B = { LSeg(f,k): i+1 <= k & k < j};
A6: A = B \/ {LSeg(f,i)}
proof
thus A c= B \/ {LSeg(f,i)}
proof let e be set;
assume e in A;
then consider k such that
A7: e = LSeg(f,k) and
A8: i <= k and
A9: k < j;
i = k or i < k by A8,AXIOMS:21;
then i = k or i+1 <= k by NAT_1:38;
then e in B or e in {LSeg(f,i)} by A7,A9,TARSKI:def 1;
hence e in B \/ {LSeg(f,i)} by XBOOLE_0:def 2;
end;
let e be set;
assume
A10: e in B \/ {LSeg(f,i)};
per cases by A10,XBOOLE_0:def 2;
suppose e in B;
then consider k such that
A11: e = LSeg(f,k) and
A12: i+1 <= k and
A13: k < j;
i < k by A12,NAT_1:38;
hence e in A by A11,A13;
suppose e in {LSeg(f,i)};
then e = LSeg(f,i) by TARSKI:def 1;
hence e in A by A2;
end;
thus L~mid(f,i,j) = union A by A1,A2,A3,SPRECT_2:18
.= union B \/ union{LSeg(f,i)} by A6,ZFMISC_1:96
.= union B \/ LSeg(f,i) by ZFMISC_1:31
.= LSeg(f,i) \/ L~mid(f,i+1,j) by A3,A4,A5,SPRECT_2:18;
end;
theorem
for f being FinSequence of TOP-REAL 2 st 1 <= i holds
i < j & j <= len f implies
L~mid(f,i,j) = L~mid(f,i,j -' 1) \/ LSeg(f,j -' 1)
proof
let f be FinSequence of TOP-REAL 2 such that
A1: 1 <= i and
A2: i < j and
A3: j <= len f;
A4: i <= j -' 1 by A2,JORDAN3:12;
j -' 1 <= j by GOBOARD9:2;
then A5: j -' 1 <= len f by A3,AXIOMS:22;
set A = { LSeg(f,k): i <= k & k < j},
B = { LSeg(f,k): i <= k & k < j -' 1};
A6: A = B \/ {LSeg(f,j -' 1)}
proof
thus A c= B \/ {LSeg(f,j -' 1)}
proof let e be set;
assume e in A;
then consider k such that
A7: e = LSeg(f,k) and
A8: i <= k and
A9: k < j;
k <= j -' 1 by A9,JORDAN3:12;
then j -' 1 = k or k < j -' 1 by AXIOMS:21;
then e in B or e in {LSeg(f,j -' 1)} by A7,A8,TARSKI:def 1;
hence e in B \/ {LSeg(f,j -' 1)} by XBOOLE_0:def 2;
end;
let e be set;
assume
A10: e in B \/ {LSeg(f,j -' 1)};
A11: j -' 1 <= j by GOBOARD9:2;
per cases by A10,XBOOLE_0:def 2;
suppose e in B;
then consider k such that
A12: e = LSeg(f,k) and
A13: i <= k and
A14: k < j -' 1;
k < j by A11,A14,AXIOMS:22;
hence e in A by A12,A13;
suppose e in {LSeg(f,j -' 1)};
then A15: e = LSeg(f,j -' 1) by TARSKI:def 1;
1 <= j & 1 <= j -' 1 by A1,A2,A4,AXIOMS:22;
then j-' 1 < j by JORDAN3:14;
hence e in A by A4,A15;
end;
thus L~mid(f,i,j) = union A by A1,A2,A3,SPRECT_2:18
.= union B \/ union{LSeg(f,j -' 1)} by A6,ZFMISC_1:96
.= union B \/ LSeg(f,j -' 1) by ZFMISC_1:31
.= L~mid(f,i,j -' 1) \/ LSeg(f,j -' 1) by A1,A4,A5,SPRECT_2:18;
end;
canceled;
theorem
for f, g being FinSequence of TOP-REAL 2 st f is_S-Seq & g is_S-Seq &
((f/.len f)`1 = (g/.1)`1 or (f/.len f)`2 = (g/.1)`2) &
L~f misses L~g &
LSeg(f/.len f,g/.1) /\ L~f={ f/.len f } &
LSeg(f/.len f,g/.1) /\ L~g={ g/.1 }
holds f^g is_S-Seq
proof let f,g be FinSequence of TOP-REAL 2 such that
A1: f is_S-Seq and
A2: g is_S-Seq and
A3: (f/.len f)`1 = (g/.1)`1 or (f/.len f)`2 = (g/.1)`2 and
A4: L~f misses L~g and
A5: LSeg(f/.len f,g/.1) /\ L~f={ f/.len f } and
A6: LSeg(f/.len f,g/.1) /\ L~g={ g/.1 };
set h = <*f/.len f*>^g;
A7: len f >= 2 by A1,TOPREAL1:def 10;
A8: len g >= 2 by A2,TOPREAL1:def 10;
1 <= len f by A7,AXIOMS:22;
then A9: len f in dom f by FINSEQ_3:27;
A10: len g >= 1 by A8,AXIOMS:22;
then A11: 1 in dom g by FINSEQ_3:27;
A12: len h = len<*f/.len f*>+len g by FINSEQ_1:35
.= len g + 1 by FINSEQ_1:56;
then A13: len h >= 1+1 by A10,AXIOMS:24;
len g <> 0 by A2,TOPREAL1:def 10;
then A14: g is non empty by FINSEQ_1:25;
A15: f.len f = f/.len f by A9,FINSEQ_4:def 4
.=h.1 by FINSEQ_1:58;
f/.len f in L~f & g/.1 in L~g by A7,A8,A9,A11,GOBOARD1:16;
then f/.len f <> g/.1 by A4,XBOOLE_0:3;
then A16: h is_S-Seq by A2,A3,A6,SPRECT_2:64;
A17: L~f /\ L~h = L~f /\ (LSeg(f/.len f,g/.1) \/ L~g) by A14,SPPOL_2:20
.= L~f /\ LSeg(f/.len f,g/.1) \/ L~f /\ L~g by XBOOLE_1:23
.= L~f /\ LSeg(f/.len f,g/.1) \/ {} by A4,XBOOLE_0:def 7
.={h.1} by A5,A9,A15,FINSEQ_4:def 4;
mid(h,2,len h) = (h/^(1+1-'1))|(len h-'2+1) by A13,JORDAN3:def 1
.= (h/^1)|(len h-'2+1) by BINARITH:39
.= g|(len h-'2+1) by FINSEQ_6:49
.= g|(len h-'1-'1+1) by JORDAN3:8
.= g|(len g-'1+1) by A12,BINARITH:39
.= g|len g by A10,AMI_5:4
.= g by TOPREAL1:2;
hence f^g is_S-Seq by A1,A15,A16,A17,JORDAN3:73;
end;
theorem
for f being S-Sequence_in_R2, p being Point of TOP-REAL 2 st p in L~f
holds (R_Cut(f,p))/.1 = f/.1
proof let f be S-Sequence_in_R2, p be Point of TOP-REAL 2;
set i = Index(p,f);
assume
A1: p in L~f;
then A2: 1 <= i & i <= len f by JORDAN3:41;
A3: 1 in dom f by FINSEQ_5:6;
p = f.1 or p <> f.1;
then len R_Cut(f,p) = Index(p,f) or len R_Cut(f,p) = Index(p,f) + 1
by A1,JORDAN3:60;
then 1 <= len R_Cut(f,p) by A1,JORDAN3:41,NAT_1:29;
hence (R_Cut(f,p))/.1 = R_Cut(f,p).1 by FINSEQ_4:24
.= f.1 by A1,A2,JORDAN3:59
.= f/.1 by A3,FINSEQ_4:def 4;
end;
theorem
for f being S-Sequence_in_R2, p,q being Point of TOP-REAL 2 st
1 <=j & j < len f & p in LSeg(f,j) & q in LSeg(f/.j,p)
holds LE q, p, L~f, f/.1, f/.len f
proof let f be S-Sequence_in_R2, p,q be Point of TOP-REAL 2 such that
A1: 1 <=j & j < len f and
A2: p in LSeg(f,j) and
A3: q in LSeg(f/.j,p);
A4: L~f is_an_arc_of f/.1, f/.len f by TOPREAL1:31;
A5: j+1 <= len f by A1,NAT_1:38;
then A6: LSeg(f,j) = LSeg(f/.j,f/.(j+1)) by A1,TOPREAL1:def 5;
f/.j in LSeg(f,j) by A1,A5,TOPREAL1:27;
then A7: LSeg(f/.j,p) c= LSeg(f,j) by A2,A6,TOPREAL1:12;
then A8: q in LSeg(f,j) by A3;
A9: LSeg(f,j) c= L~f by TOPREAL3:26;
per cases;
suppose p = q;
hence thesis by A2,A4,A9,JORDAN5C:9;
suppose
A10: q <> p;
for i, j being Nat st q in LSeg(f,i) & p in LSeg(f,j)
& 1 <= i & i+1 <= len f
& 1 <= j & j+1 <= len f holds
i <= j & (i = j implies LE q,p,f/.i,f/.(i+1))
proof let i1, i2 be Nat such that
A11: q in LSeg(f,i1) and
A12: p in LSeg(f,i2) and
A13: 1 <= i1 & i1+1 <= len f and
A14: 1 <= i2 & i2+1 <= len f;
A15: now assume i2 + 1 > j & j+1 > i2;
then i2 <= j & j <= i2 by NAT_1:38;
hence i2 = j by AXIOMS:21;
end;
A16: p in LSeg(f,i2) /\ LSeg(f,j) by A2,A12,XBOOLE_0:def 3;
then LSeg(f,i2) meets LSeg(f,j) by XBOOLE_0:4;
then i2 + 1 >= j & j + 1 >= i2 by TOPREAL1:def 9;
then A17: i2 + 1 = j or i2 = j or j + 1 = i2 by A15,AXIOMS:21;
A18: now assume
A19: i2 + 1 = j;
i2+(1+1) = i2+1+1 by XCMPLX_1:1;
then i2+2 <= len f by A1,A19,NAT_1:38;
then p in {f/.j} by A14,A16,A19,TOPREAL1:def 8;
then p = f/.j by TARSKI:def 1;
then q in {p} by A3,TOPREAL1:7;
hence contradiction by A10,TARSKI:def 1;
end;
then A20: i2 >= j by A17,NAT_1:29;
A21: now assume i1 + 1 > j & j+1 > i1;
then i1 <= j & j <= i1 by NAT_1:38;
hence i1 = j by AXIOMS:21;
end;
A22: q in LSeg(f,i1) /\ LSeg(f,j) by A3,A7,A11,XBOOLE_0:def 3;
then LSeg(f,i1) meets LSeg(f,j) by XBOOLE_0:4;
then A23: i1 + 1 >= j & j + 1 >= i1 by TOPREAL1:def 9;
then A24: i1 + 1 = j or i1 = j or j + 1 = i1 by A21,AXIOMS:21;
1 <= j+1 by NAT_1:29;
then A25: j+1 in dom f by A5,FINSEQ_3:27;
A26: j in dom f by A1,FINSEQ_3:27;
A27:now assume f/.(j+1)=f/.j;
then j = j+1 by A25,A26,PARTFUN2:17;
hence contradiction by REAL_1:69;
end;
A28: now assume
A29: i1 = j + 1;
j+(1+1) = j+1+1 by XCMPLX_1:1;
then q in {f/.(j+1)} by A1,A13,A22,A29,TOPREAL1:def 8;
then q = f/.(j+1) by TARSKI:def 1;
hence contradiction by A3,A6,A7,A10,A27,SPPOL_1:24;
end;
then i1 <= j by A24,NAT_1:29;
hence i1 <= i2 by A20,AXIOMS:22;
assume
A30: i1 = i2;
not p in LSeg(f/.j,q) by A3,A10,Th16;
then not LE p,q,f/.j,f/.(j+1) by JORDAN3:65;
then LT q,p,f/.j,f/.(j+1)
by A2,A6,A11,A18,A21,A23,A27,A28,A30,AXIOMS:21,JORDAN3:63;
hence LE q,p,f/.i1,f/.(i1+1)
by A18,A21,A23,A28,A30,AXIOMS:21,JORDAN3:def 7;
end;
hence LE q, p, L~f, f/.1, f/.len f by A2,A8,A9,A10,JORDAN5C:30;
end;
begin :: Special circular
theorem Th41:
for f being non constant standard special_circular_sequence holds
LeftComp f is open & RightComp f is open
proof
let f be non constant standard special_circular_sequence;
L~f is closed by SPPOL_1:49;
then A1: (L~f)` is open by TOPS_1:29;
LeftComp f is_a_component_of (L~f)` by GOBOARD9:def 1;
then LeftComp f is_a_component_of (L~f)`;
hence LeftComp f is open by A1,Th18;
RightComp f is_a_component_of (L~f)` by GOBOARD9:def 2;
then RightComp f is_a_component_of (L~f)`;
hence RightComp f is open by A1,Th18;
end;
definition let f be non constant standard special_circular_sequence;
cluster L~f -> non vertical non horizontal;
coherence
proof
W-bound L~f <> E-bound L~f by TOPREAL5:23;
hence L~f is non vertical by SPRECT_1:17;
S-bound L~f <> N-bound L~f by TOPREAL5:22;
hence L~f is non horizontal by SPRECT_1:18;
end;
cluster LeftComp f -> being_Region;
coherence
proof
thus LeftComp f is open by Th41;
LeftComp f is_a_component_of (L~f)` by GOBOARD9:def 1;
then consider A being Subset of (TOP-REAL 2)|(L~f)` such that
A1: A = LeftComp f and
A2: A is_a_component_of (TOP-REAL 2)|(L~f)` by CONNSP_1:def 6;
A is connected by A2,CONNSP_1:def 5;
hence LeftComp f is connected by A1,CONNSP_1:24;
end;
cluster RightComp f -> being_Region;
coherence
proof
thus RightComp f is open by Th41;
RightComp f is_a_component_of (L~f)` by GOBOARD9:def 2;
then consider A being Subset of (TOP-REAL 2)|(L~f)` such that
A3: A = RightComp f and
A4: A is_a_component_of (TOP-REAL 2)|(L~f)` by CONNSP_1:def 6;
A is connected by A4,CONNSP_1:def 5;
hence RightComp f is connected by A3,CONNSP_1:24;
end;
end;
theorem Th42:
for f being non constant standard special_circular_sequence
holds RightComp f misses L~f
proof
let f be non constant standard special_circular_sequence;
(L~f)` =LeftComp f \/ RightComp f by GOBRD12:11;
then RightComp f c= (L~f)` by XBOOLE_1:7;
hence RightComp f misses L~f by SUBSET_1:43;
end;
theorem Th43:
for f being non constant standard special_circular_sequence
holds LeftComp f misses L~f
proof
let f be non constant standard special_circular_sequence;
(L~f)` =LeftComp f \/ RightComp f by GOBRD12:11;
then LeftComp f c= (L~f)` by XBOOLE_1:7;
hence LeftComp f misses L~f by SUBSET_1:43;
end;
theorem Th44:
for f being non constant standard special_circular_sequence
holds i_w_n f < i_e_n f
proof let f be non constant standard special_circular_sequence;
set G = GoB f;
A1: width G > 1 by GOBOARD7:35;
A2: i_w_n f <= len G by JORDAN5D:47;
A3: G*(i_w_n f,width G) = N-min L~f by JORDAN5D:def 7;
A4: 1 <= i_e_n f by JORDAN5D:47;
A5: G*(i_e_n f,width G) = N-max L~f by JORDAN5D:def 8;
A6: (N-min L~f)`1 < (N-max L~f)`1 by SPRECT_2:55;
then A7: i_w_n f <> i_e_n f by A5,JORDAN5D:def 7;
assume i_w_n f >= i_e_n f;
then i_w_n f > i_e_n f by A7,AXIOMS:21;
hence contradiction by A1,A2,A3,A4,A5,A6,GOBOARD5:4;
end;
theorem Th45:
for f being non constant standard special_circular_sequence
ex i st 1 <= i & i < len GoB f & N-min L~f = (GoB f)*(i,width GoB f)
proof let f be non constant standard special_circular_sequence;
take i = i_w_n f;
thus 1 <= i by JORDAN5D:47;
A1: i_e_n f <= len GoB f by JORDAN5D:47;
i < i_e_n f by Th44;
hence i < len GoB f by A1,AXIOMS:22;
thus N-min L~f = (GoB f)*(i,width GoB f) by JORDAN5D:def 7;
end;
theorem Th46:
for f being clockwise_oriented
(non constant standard special_circular_sequence)
st i in dom GoB f & f/.1 = (GoB f)*(i,width GoB f) &
f/.1 = N-min L~f
holds f/.2 = (GoB f)*(i+1,width GoB f)
& f/.(len f -' 1) = (GoB f)*(i,width GoB f -' 1)
proof
let f be clockwise_oriented (non constant standard special_circular_sequence)
such that
A1: i in dom GoB f and
A2: f/.1 = (GoB f)*(i,width GoB f) and
A3: f/.1 = N-min L~f;
A4: f/.2 in N-most L~f by A3,SPRECT_2:34;
A5: 1 <= width GoB f by GOBRD11:34;
A6: 4 < len f by GOBOARD7:36;
then A7: 1+1 <= len f by AXIOMS:22;
then A8: 1+1 in dom f by FINSEQ_3:27;
then consider i1,j1 being Nat such that
A9: [i1,j1] in Indices GoB f and
A10: f/.2 = (GoB f)*(i1,j1) by GOBOARD2:25;
A11: 1 <= len f by A6,AXIOMS:22;
then A12: 1 in dom f by FINSEQ_3:27;
A13: 1 <= i & i <= len GoB f by A1,FINSEQ_3:27;
then A14: [i,width GoB f] in Indices GoB f by A5,GOBOARD7:10;
A15: 1 <= j1 & j1 <= width GoB f by A9,GOBOARD5:1;
A16: 1 <= i1 & i1 <= len GoB f by A9,GOBOARD5:1;
now assume
A17: j1 < width GoB f;
A18: (GoB f)*(i1,width GoB f)`2 = (GoB f)*(1,width GoB f)`2
by A5,A16,GOBOARD5:2
.= N-bound L~f by JORDAN5D:42;
(f/.2)`2 = (N-min L~f)`2 by A4,PSCOMP_1:98
.= N-bound L~f by PSCOMP_1:94;
hence contradiction by A10,A15,A16,A17,A18,GOBOARD5:5;
end;
then A19: j1 = width GoB f by A15,AXIOMS:21;
A20: abs(i-i1)+0 = abs(i-i1)+abs(0) by ABSVALUE:7
.=abs(i-i1)+abs(width GoB f-width GoB f) by XCMPLX_1:14
.= 1 by A2,A8,A9,A10,A12,A14,A19,GOBOARD5:13;
now assume i > i1;
then (f/.2)`1 < (N-min L~f)`1 by A2,A3,A10,A13,A15,A16,A19,GOBOARD5:4;
hence contradiction by A4,PSCOMP_1:98;
end;
hence
A21: f/.2 = (GoB f)*(i+1,width GoB f) by A10,A19,A20,GOBOARD1:1;
A22: f/.len f = f/.1 by FINSEQ_6:def 1;
A23: len f -' 1 + 1 = len f by A11,AMI_5:4;
A24: 1 <= len f -' 1 & len f -' 1 <= len f by A7,JORDAN3:7,12;
then A25: len f -' 1 in dom f by FINSEQ_3:27;
then consider i2,j2 being Nat such that
A26: [i2,j2] in Indices GoB f and
A27: f/.(len f -' 1) = (GoB f)*(i2,j2) by GOBOARD2:25;
A28: 1 <= i2 & i2 <= len GoB f by A26,GOBOARD5:1;
A29: 1 <= j2 & j2 <= width GoB f by A26,GOBOARD5:1;
len f in dom f by A11,FINSEQ_3:27;
then A30: abs(i2-i)+abs(j2-width GoB f) = 1
by A2,A14,A22,A23,A25,A26,A27,GOBOARD5:13;
per cases by A30,GOBOARD1:2;
suppose that
A31: abs(i2-i)=1 and
A32: j2=width GoB f;
A33: (f/.(len f -' 1))`2 = ((GoB f)*(1,width GoB f))`2 by A5,A27,A28,A32,
GOBOARD5:2
.= (N-min L~f)`2 by A2,A3,A5,A13,GOBOARD5:2
.= N-bound L~f by PSCOMP_1:94;
f/.(len f -' 1) in L~f by A7,A25,GOBOARD1:16;
then A34: f/.(len f -' 1) in N-most L~f by A33,SPRECT_2:14;
now per cases by A31,GOBOARD1:1;
suppose i > i2;
then (f/.(len f -' 1))`1 < (N-min L~f)`1
by A2,A3,A5,A13,A27,A28,A32,GOBOARD5:4;
hence contradiction by A34,PSCOMP_1:98;
suppose i+1 = i2;
then 2 >= len f -' 1 by A21,A24,A27,A32,GOBOARD7:39;
then 2+1 >= len f by Th5;
hence contradiction by A6,AXIOMS:22;
end;
hence thesis;
suppose that
A35: abs(j2-width GoB f)=1 and
A36: i2=i;
j2 < width GoB f & width GoB f = j2+1 by A29,A35,GOBOARD1:1;
hence f/.(len f -' 1) = (GoB f)*(i,width GoB f -' 1) by A27,A36,BINARITH:39;
end;
theorem
for f being non constant standard special_circular_sequence
st 1 <= i & i < j & j <= len f & f/.1 in L~mid(f,i,j)
holds i = 1 or j = len f
proof
let f be non constant standard special_circular_sequence such that
A1: 1 <= i and
A2: i < j and
A3: j <= len f;
assume f/.1 in L~mid(f,i,j);
then consider n such that
A4: 1 <= n & n+1 <= len mid(f,i,j) and
A5: f/.1 in LSeg(mid(f,i,j),n) by SPPOL_2:13;
assume that
A6: i <> 1 and
A7: j <> len f;
n < len mid(f,i,j) by A4,NAT_1:38;
then A8: n<j-'i+1 by A1,A2,A3,JORDAN4:20;
then A9: LSeg(mid(f,i,j),n)=LSeg(f,n+i-'1) by A1,A2,A3,A4,JORDAN4:31;
A10: len f > 4 by GOBOARD7:36;
then 1+1 <= len f by AXIOMS:22;
then f/.1 in LSeg(f,1) by TOPREAL1:27;
then A11: f/.1 in LSeg(f,1) /\ LSeg(f,n+i-'1) by A5,A9,XBOOLE_0:def 3;
then A12: LSeg(f,1) meets LSeg(f,n+i-'1) by XBOOLE_0:4;
per cases by A12,GOBOARD5:def 4;
suppose 1+1 >= n+i-'1;
then A13: n+i <= 2+1 by Th5;
n+i >= i+1 by A4,AXIOMS:24;
then i+1 <= 2+1 by A13,AXIOMS:22;
then A14: i <= 2 by REAL_1:53;
i > 1 by A1,A6,AXIOMS:21;
then i >= 1+1 by NAT_1:38;
then A15: i = 2 by A14,AXIOMS:21;
then n <= 1 by A13,REAL_1:53;
then n = 1 by A4,AXIOMS:21;
then A16: n+i-'1 = 2 by A15,BINARITH:39;
1+2 <= len f by A10,AXIOMS:22;
then LSeg(f,1) /\ LSeg(f,1+1) = {f/.(1+1)} by TOPREAL1:def 8;
then A17: f/.1 = f/.2 by A11,A16,TARSKI:def 1;
2 < len f by A10,AXIOMS:22;
hence contradiction by A17,GOBOARD7:38;
suppose
A18: n+i-'1+1 >= len f;
n <= n+i by NAT_1:29;
then 1 <= n+i by A4,AXIOMS:22;
then A19: len f <= n+i by A18,AMI_5:4;
A20: j < len f by A3,A7,AXIOMS:21;
j-'i+1+i = j-'i+i+1 by XCMPLX_1:1
.= j+1 by A2,AMI_5:4;
then n+i < j+1 by A8,REAL_1:53;
then n+i <= j by NAT_1:38;
hence contradiction by A19,A20,AXIOMS:22;
end;
theorem
for f being
clockwise_oriented (non constant standard special_circular_sequence)
st f/.1 = N-min L~f
holds LSeg(f/.1,f/.2) c= L~SpStSeq L~f
proof
let f be clockwise_oriented (non constant standard special_circular_sequence);
assume
A1: f/.1 = N-min L~f;
then A2: f/.1 in LSeg(NW-corner L~f,NE-corner L~f) by Th28;
A3: f/.2 in N-most L~f by A1,SPRECT_2:34;
N-most L~f c= LSeg(NW-corner L~f,NE-corner L~f) by Th27;
then A4: LSeg(f/.1,f/.2) c= LSeg(NW-corner L~f,NE-corner L~f)
by A2,A3,TOPREAL1:12;
LSeg(NW-corner L~f,NE-corner L~f) c= L~SpStSeq L~f by Th26;
hence LSeg(f/.1,f/.2) c= L~SpStSeq L~f by A4,XBOOLE_1:1;
end;
begin :: Rectangular
theorem Th49:
for f being rectangular FinSequence of TOP-REAL 2,
p being Point of TOP-REAL 2 st p in L~f
holds p`1 = W-bound L~f or p`1 = E-bound L~f or
p`2 = S-bound L~f or p`2 = N-bound L~f
proof
let f be rectangular FinSequence of TOP-REAL 2,
p be Point of TOP-REAL 2 such that
A1: p in L~f;
consider D being non vertical non horizontal non empty compact
Subset of TOP-REAL 2
such that
A2: f = SpStSeq D by SPRECT_1:def 2;
L~f = (LSeg(NW-corner D,NE-corner D) \/ LSeg(NE-corner D,SE-corner D)) \/
(LSeg(SE-corner D,SW-corner D) \/ LSeg(SW-corner D,NW-corner D))
by A2,SPRECT_1:43;
then A3: p in LSeg(NW-corner D,NE-corner D) \/ LSeg(NE-corner D,SE-corner D
) or
p in LSeg(SE-corner D,SW-corner D) \/ LSeg(SW-corner D,NW-corner D)
by A1,XBOOLE_0:def 2;
per cases by A3,XBOOLE_0:def 2;
suppose
A4: p in LSeg(NW-corner D,NE-corner D);
N-bound L~SpStSeq D = N-bound D by SPRECT_1:68;
then (NW-corner D)`2 = N-bound L~f & (NE-corner D)`2 = N-bound L~f
by A2,PSCOMP_1:75,77;
hence thesis by A4,GOBOARD7:6;
suppose
A5: p in LSeg(NE-corner D,SE-corner D);
E-bound L~SpStSeq D = E-bound D by SPRECT_1:69;
then (NE-corner D)`1 = E-bound L~f & (SE-corner D)`1 = E-bound L~f
by A2,PSCOMP_1:76,78;
hence thesis by A5,GOBOARD7:5;
suppose
A6: p in LSeg(SE-corner D,SW-corner D);
S-bound L~SpStSeq D = S-bound D by SPRECT_1:67;
then (SE-corner D)`2 = S-bound L~f & (SW-corner D)`2 = S-bound L~f
by A2,PSCOMP_1:73,79;
hence thesis by A6,GOBOARD7:6;
suppose
A7: p in LSeg(SW-corner D,NW-corner D);
W-bound L~SpStSeq D = W-bound D by SPRECT_1:66;
then (SW-corner D)`1 = W-bound L~f & (NW-corner D)`1 = W-bound L~f
by A2,PSCOMP_1:72,74;
hence thesis by A7,GOBOARD7:5;
end;
definition
cluster rectangular special_circular_sequence;
existence
proof
consider C being non empty compact non vertical non horizontal
Subset of TOP-REAL2;
SpStSeq C is special_circular_sequence;
hence thesis;
end;
end;
theorem Th50:
for f being rectangular special_circular_sequence,
g being S-Sequence_in_R2
st g/.1 in LeftComp f & g/.len g in RightComp f
holds L~f meets L~g
proof
let f be rectangular special_circular_sequence,
g be S-Sequence_in_R2 such that
A1: g/.1 in LeftComp f and
A2: g/.len g in RightComp f;
assume L~f misses L~g;
then L~g c= (L~f)` by SUBSET_1:43;
then A3: L~g c= LeftComp f \/ RightComp f by GOBRD12:11;
A4: LeftComp f is open & RightComp f is open by Th41;
A5: len g >= 2 by TOPREAL1:def 10;
then g/.1 in L~g by JORDAN3:34;
then g/.1 in LeftComp f /\ L~g by A1,XBOOLE_0:def 3;
then A6:LeftComp f meets L~g by XBOOLE_0:4;
g/.len g in L~g by A5,JORDAN3:34;
then g/.len g in RightComp f /\ L~g by A2,XBOOLE_0:def 3;
then A7:RightComp f meets L~g by XBOOLE_0:4;
LeftComp f misses RightComp f by SPRECT_1:96;
then A8: L~g is not connected by A3,A4,A6,A7,TOPREAL5:4;
L~g is_an_arc_of g/.1,g/.len g by TOPREAL1:31;
hence contradiction by A8,JORDAN6:11;
end;
theorem Th51:
for f being rectangular special_circular_sequence
holds SpStSeq L~f = f
proof let f be rectangular special_circular_sequence;
A1: SpStSeq L~f = <*NW-corner L~f,NE-corner L~f,SE-corner L~f*>^
<*SW-corner L~f,NW-corner L~f*> by SPRECT_1:def 1;
set C = L~f, g = SpStSeq C;
consider D being non vertical non horizontal non empty compact
Subset of TOP-REAL 2 such that
A2: f = SpStSeq D by SPRECT_1:def 2;
A3: 5 = len f by SPRECT_1:90;
A4: len g = len<*NW-corner L~f,NE-corner L~f,SE-corner L~f*>
+len<*SW-corner L~f,NW-corner L~f*> by A1,FINSEQ_1:35
.= 3+len<*SW-corner L~f,NW-corner L~f*> by FINSEQ_1:62
.= 3+2 by FINSEQ_1:61;
then A5: dom f = dom g by A3,FINSEQ_3:31;
for i st i in dom f holds f/.i = g/.i
proof let i;
assume i in dom f;
then A6: 0 <> i & i <= len f by FINSEQ_3:27;
A7: f/.1 = W-max C by SPRECT_1:91
.= NW-corner D by A2,SPRECT_1:83
.= NW-corner C by A2,SPRECT_1:70
.= g/.1 by SPRECT_1:37;
per cases by A3,A6,CQC_THE1:6;
suppose i = 1;
hence thesis by A7;
suppose
A8: i = 2;
hence f/.i = E-max C by SPRECT_1:92
.= NE-corner D by A2,SPRECT_1:87
.= NE-corner C by A2,SPRECT_1:71
.= g/.i by A8,SPRECT_1:38;
suppose
A9: i = 3;
hence f/.i = E-min C by SPRECT_1:93
.= SE-corner D by A2,SPRECT_1:86
.= SE-corner C by A2,SPRECT_1:73
.= g/.i by A9,SPRECT_1:39;
suppose
A10: i = 4;
hence f/.i = W-min C by SPRECT_1:94
.= SW-corner D by A2,SPRECT_1:82
.= SW-corner C by A2,SPRECT_1:72
.= g/.i by A10,SPRECT_1:40;
suppose
A11: i = 5;
hence f/.i = f/.1 by A3,FINSEQ_6:def 1
.= g/.i by A4,A7,A11,FINSEQ_6:def 1;
end;
hence f = g by A5,FINSEQ_5:13;
end;
theorem Th52:
for f being rectangular special_circular_sequence holds
L~f = { p where p is Point of TOP-REAL 2:
p`1 = W-bound L~f & p`2 <= N-bound L~f & p`2 >= S-bound L~f or
p`1 <= E-bound L~f & p`1 >= W-bound L~f & p`2 = N-bound L~f or
p`1 <= E-bound L~f & p`1 >= W-bound L~f & p`2 = S-bound L~f or
p`1 = E-bound L~f & p`2 <= N-bound L~f & p`2 >= S-bound L~f}
proof let f be rectangular special_circular_sequence;
set C = L~f,
E = { p : p`1 = E-bound C & p`2 <= N-bound C & p`2 >= S-bound C},
S = { p : p`1 <= E-bound C & p`1 >= W-bound C & p`2 = S-bound C},
N = { p : p`1 <= E-bound C & p`1 >= W-bound C & p`2 = N-bound C},
W = { p : p`1 = W-bound C & p`2 <= N-bound C & p`2 >= S-bound C};
A1: C = L~SpStSeq C by Th51;
A2: LSeg(SE-corner C, NE-corner C) = E by SPRECT_1:25;
A3: LSeg(SW-corner C, SE-corner C) = S by SPRECT_1:26;
A4: LSeg(NW-corner C, NE-corner C) = N by SPRECT_1:27;
A5: LSeg(SW-corner C, NW-corner C) = W by SPRECT_1:28;
thus
C c= { p where p is Point of TOP-REAL 2:
p`1 = W-bound C & p`2 <= N-bound C & p`2 >= S-bound C or
p`1 <= E-bound C & p`1 >= W-bound C & p`2 = N-bound C or
p`1 <= E-bound C & p`1 >= W-bound C & p`2 = S-bound C or
p`1 = E-bound C & p`2 <= N-bound C & p`2 >= S-bound C}
proof let x be set;
assume
A6: x in C;
then reconsider q=x as Point of TOP-REAL 2;
q in (LSeg(NW-corner C,NE-corner C) \/ LSeg(NE-corner C,SE-corner C)) \/
(LSeg(SE-corner C,SW-corner C) \/ LSeg(SW-corner C,NW-corner C))
by A1,A6,SPRECT_1:43;
then q in (LSeg(NW-corner C,NE-corner C) \/ LSeg(NE-corner C,SE-corner C))
or
q in (LSeg(SE-corner C,SW-corner C) \/ LSeg(SW-corner C,NW-corner C))
by XBOOLE_0:def 2;
then q in LSeg(NW-corner C,NE-corner C) or q in LSeg(NE-corner C,SE-corner
C) or
q in LSeg(SE-corner C,SW-corner C) or q in LSeg(SW-corner C,NW-corner C)
by XBOOLE_0:def 2;
then (ex p st x = p & p`1 = E-bound C & p`2 <= N-bound C & p`2 >=
S-bound C)
or (ex p st x = p & p`1 <= E-bound C & p`1 >=
W-bound C & p`2 = S-bound C)
or (ex p st x = p & p`1 <= E-bound C & p`1 >=
W-bound C & p`2 = N-bound C)
or (ex p st x = p & p`1 = W-bound C & p`2 <= N-bound C & p`2 >=
S-bound C)
by A2,A3,A4,A5;
hence x in { p where p is Point of TOP-REAL 2:
p`1 = W-bound C & p`2 <= N-bound C & p`2 >= S-bound C or
p`1 <= E-bound C & p`1 >= W-bound C & p`2 = N-bound C or
p`1 <= E-bound C & p`1 >= W-bound C & p`2 = S-bound C or
p`1 = E-bound C & p`2 <= N-bound C & p`2 >= S-bound C};
end;
let x be set;
assume x in { p where p is Point of TOP-REAL 2:
p`1 = W-bound C & p`2 <= N-bound C & p`2 >= S-bound C or
p`1 <= E-bound C & p`1 >= W-bound C & p`2 = N-bound C or
p`1 <= E-bound C & p`1 >= W-bound C & p`2 = S-bound C or
p`1 = E-bound C & p`2 <= N-bound C & p`2 >= S-bound C};
then ex p st x = p &
(p`1 = W-bound C & p`2 <= N-bound C & p`2 >= S-bound C or
p`1 <= E-bound C & p`1 >= W-bound C & p`2 = N-bound C or
p`1 <= E-bound C & p`1 >= W-bound C & p`2 = S-bound C or
p`1 = E-bound C & p`2 <= N-bound C & p`2 >= S-bound C);
then x in LSeg(NW-corner C,NE-corner C) or x in LSeg(NE-corner C,SE-corner
C) or
x in LSeg(SE-corner C,SW-corner C) or x in LSeg(SW-corner C,NW-corner C)
by A2,A3,A4,A5;
then x in (LSeg(NW-corner C,NE-corner C) \/ LSeg(NE-corner C,SE-corner C))
or
x in (LSeg(SE-corner C,SW-corner C) \/ LSeg(SW-corner C,NW-corner C))
by XBOOLE_0:def 2;
then x in (LSeg(NW-corner C,NE-corner C) \/ LSeg(NE-corner C,SE-corner C))
\/
(LSeg(SE-corner C,SW-corner C) \/ LSeg(SW-corner C,NW-corner C))
by XBOOLE_0:def 2;
hence x in C by A1,SPRECT_1:43;
end;
theorem Th53:
for f being rectangular special_circular_sequence holds
GoB f = (f/.4,f/.1)][(f/.3,f/.2)
proof let f be rectangular special_circular_sequence;
set G = (f/.4,f/.1)][(f/.3,f/.2),
v1 = Incr X_axis f, v2 = Incr Y_axis f;
A1: f/.1 = N-min L~f & f/.1 = W-max L~f by SPRECT_1:91;
A2: f/.2 = N-max L~f & f/.2 = E-max L~f by SPRECT_1:92;
A3: f/.3 = S-max L~f & f/.3 = E-min L~f by SPRECT_1:93;
A4: f/.4 = S-min L~f & f/.4 = W-min L~f by SPRECT_1:94;
A5: len f = 5 by SPRECT_1:90;
set g = <*(f/.1)`1,(f/.2)`1*>,
h = <*(f/.1)`1,(f/.2)`1*>^<*(f/.3)`1,(f/.4)`1,(f/.5)`1*>;
A6: len g = 2 by FINSEQ_1:61;
A7: len<*(f/.3)`1,(f/.4)`1,(f/.5)`1*> = 3 by FINSEQ_1:62;
A8: len h = len <*(f/.1)`1,(f/.2)`1*> + len<*(f/.3)`1,(f/.4)`1,(f/.5)`1*>
by FINSEQ_1:35
.= len <*(f/.1)`1,(f/.2)`1*> + 3 by FINSEQ_1:62
.= 2 + 3 by FINSEQ_1:61
.= len f by SPRECT_1:90;
for n st n in dom h holds h.n = (f/.n)`1
proof let n;
assume n in dom h;
then 1 <= n & n <= 5 by A5,A8,FINSEQ_3:27;
then A9: 1 <= n & (n=0 or n=1 or n=2 or n=3 or n=4 or n=5) by
CQC_THE1:6;
per cases by A9;
suppose
A10: n=1;
then n in dom g by A6,FINSEQ_3:27;
hence h.n = <*(f/.1)`1,(f/.2)`1*>.1 by A10,FINSEQ_1:def 7
.= (f/.n)`1 by A10,FINSEQ_1:61;
suppose
A11: n=2;
then n in dom g by A6,FINSEQ_3:27;
hence h.n = <*(f/.1)`1,(f/.2)`1*>.2 by A11,FINSEQ_1:def 7
.= (f/.n)`1 by A11,FINSEQ_1:61;
suppose
A12: n=3;
hence h.n = h.(2+1)
.= <*(f/.3)`1,(f/.4)`1,(f/.5)`1*>.1 by A6,A7,SCMFSA_7:10
.= (f/.n)`1 by A12,FINSEQ_1:62;
suppose
A13: n=4;
hence h.n = h.(2+2)
.= <*(f/.3)`1,(f/.4)`1,(f/.5)`1*>.2 by A6,A7,SCMFSA_7:10
.= (f/.n)`1 by A13,FINSEQ_1:62;
suppose
A14: n=5;
hence h.n = h.(2+3)
.= <*(f/.3)`1,(f/.4)`1,(f/.5)`1*>.3 by A6,A7,SCMFSA_7:10
.= (f/.n)`1 by A14,FINSEQ_1:62;
end;
then A15: X_axis f = h by A8,GOBOARD1:def 3;
A16: dom g = {1,2} by FINSEQ_1:4,FINSEQ_3:29;
A17: {(f/.3)`1,(f/.4)`1,(f/.5)`1} c= { (f/.1)`1,(f/.2)`1 }
proof let x be set;
assume
A18: x in {(f/.3)`1,(f/.4)`1,(f/.5)`1};
per cases by A18,ENUMSET1:13;
suppose x = (f/.3)`1;
then x = (f/.2)`1 by A2,A3,PSCOMP_1:105;
hence thesis by TARSKI:def 2;
suppose x = (f/.4)`1;
then x = (f/.1)`1 by A1,A4,PSCOMP_1:85;
hence thesis by TARSKI:def 2;
suppose x = (f/.5)`1;
then x = (f/.1)`1 by A5,FINSEQ_6:def 1;
hence thesis by TARSKI:def 2;
end;
A19: rng g = { (f/.1)`1,(f/.2)`1 } by FINSEQ_2:147;
then A20: rng g = rng<*(f/.1)`1,(f/.2)`1*> \/ {(f/.3)`1,(f/.4)`1,(f/.5)`1}
by A17,XBOOLE_1:12
.= rng<*(f/.1)`1,(f/.2)`1*> \/ rng<*(f/.3)`1,(f/.4)`1,(f/.5)`1*>
by FINSEQ_2:148
.= rng X_axis f by A15,FINSEQ_1:44;
A21: (f/.1)`1 < (f/.2)`1 by A1,A2,SPRECT_2:55;
A22: len g = 2 by FINSEQ_1:61
.= Card rng X_axis f by A19,A20,A21,CARD_2:76;
g is increasing
proof let n,m such that
A23: n in dom g and
A24: m in dom g and
A25: n<m;
A26: g.1 = (f/.1)`1 & g.2 = (f/.2)`1 by FINSEQ_1:61;
(n = 1 or n = 2) & (m = 1 or m = 2) by A16,A23,A24,TARSKI:def 2;
hence g.n < g.m by A1,A2,A25,A26,SPRECT_2:55;
end;
then A27: v1 = <*(f/.1)`1,(f/.2)`1*> by A20,A22,GOBOARD2:def 2;
set g = <*(f/.4)`2,(f/.5)`2*>,
h = <*(f/.1)`2,(f/.2)`2,(f/.3)`2*>^<*(f/.4)`2,(f/.5)`2*>;
A28: len g = 2 by FINSEQ_1:61;
A29: len<*(f/.1)`2,(f/.2)`2,(f/.3)`2*> = 3 by FINSEQ_1:62;
A30: len h = len <*(f/.1)`2,(f/.2)`2,(f/.3)`2*> + len<*(f/.4)`2,(f/.5)`2*>
by FINSEQ_1:35
.= len <*(f/.4)`2,(f/.5)`2*> + 3 by FINSEQ_1:62
.= 2 + 3 by FINSEQ_1:61
.= len f by SPRECT_1:90;
for n st n in dom h holds h.n = (f/.n)`2
proof let n;
assume n in dom h;
then 1 <= n & n <= 5 by A5,A30,FINSEQ_3:27;
then A31: 1 <= n & (n=0 or n=1 or n=2 or n=3 or n=4 or n=5) by
CQC_THE1:6;
per cases by A31;
suppose
A32: n=1;
then n in dom<*(f/.1)`2,(f/.2)`2,(f/.3)`2*> by A29,FINSEQ_3:27;
hence h.n = <*(f/.1)`2,(f/.2)`2,(f/.3)`2*>.1 by A32,FINSEQ_1:def 7
.= (f/.n)`2 by A32,FINSEQ_1:62;
suppose
A33: n=2;
then n in dom<*(f/.1)`2,(f/.2)`2,(f/.3)`2*> by A29,FINSEQ_3:27;
hence h.n = <*(f/.1)`2,(f/.2)`2,(f/.3)`2*>.2 by A33,FINSEQ_1:def 7
.= (f/.n)`2 by A33,FINSEQ_1:62;
suppose
A34: n=3;
then n in dom<*(f/.1)`2,(f/.2)`2,(f/.3)`2*> by A29,FINSEQ_3:27;
hence h.n = <*(f/.1)`2,(f/.2)`2,(f/.3)`2*>.3 by A34,FINSEQ_1:def 7
.= (f/.n)`2 by A34,FINSEQ_1:62;
suppose
A35: n=4;
hence h.n = h.(3+1)
.= <*(f/.4)`2,(f/.5)`2*>.1 by A28,A29,SCMFSA_7:10
.= (f/.n)`2 by A35,FINSEQ_1:61;
suppose
A36: n=5;
hence h.n = h.(2+3)
.= <*(f/.4)`2,(f/.5)`2*>.2 by A28,A29,SCMFSA_7:10
.= (f/.n)`2 by A36,FINSEQ_1:61;
end;
then A37: Y_axis f = h by A30,GOBOARD1:def 4;
A38: dom g = {1,2} by FINSEQ_1:4,FINSEQ_3:29;
A39: f/.1 = f/.5 by A5,FINSEQ_6:def 1;
A40: {(f/.1)`2,(f/.2)`2,(f/.3)`2} c= { (f/.4)`2,(f/.5)`2 }
proof let x be set;
assume
A41: x in {(f/.1)`2,(f/.2)`2,(f/.3)`2};
per cases by A41,ENUMSET1:13;
suppose x = (f/.1)`2;
hence thesis by A39,TARSKI:def 2;
suppose x = (f/.2)`2;
then x = (f/.1)`2 by A1,A2,PSCOMP_1:95;
hence thesis by A39,TARSKI:def 2;
suppose x = (f/.3)`2;
then x = (f/.4)`2 by A3,A4,PSCOMP_1:115;
hence thesis by TARSKI:def 2;
end;
A42: rng g = { (f/.4)`2,(f/.5)`2 } by FINSEQ_2:147;
then A43: rng g = {(f/.1)`2,(f/.2)`2,(f/.3)`2} \/ {(f/.4)`2,(f/.5)`2}
by A40,XBOOLE_1:12
.= rng<*(f/.1)`2,(f/.2)`2,(f/.3)`2*> \/ {(f/.4)`2,(f/.5)`2}
by FINSEQ_2:148
.= rng<*(f/.1)`2,(f/.2)`2,(f/.3)`2*> \/ rng<*(f/.4)`2,(f/.5)`2*>
by FINSEQ_2:147
.= rng Y_axis f by A37,FINSEQ_1:44;
A44: (f/.4)`2 < (f/.5)`2 by A1,A4,A39,SPRECT_2:61;
A45: len g = 2 by FINSEQ_1:61
.= Card rng Y_axis f by A42,A43,A44,CARD_2:76;
g is increasing
proof let n,m such that
A46: n in dom g and
A47: m in dom g and
A48: n<m;
A49: g.1 = (f/.4)`2 & g.2 = (f/.5)`2 by FINSEQ_1:61;
(n = 1 or n = 2) & (m = 1 or m = 2) by A38,A46,A47,TARSKI:def 2;
hence g.n < g.m by A1,A4,A39,A48,A49,SPRECT_2:61;
end;
then A50: v2 = <*(f/.4)`2,(f/.1)`2*> by A39,A43,A45,GOBOARD2:def 2;
A51: len G = 2 by MATRIX_2:3 .= len v1 by A27,FINSEQ_1:61;
A52: width G = 2 by MATRIX_2:3 .= len v2 by A50,FINSEQ_1:61;
A53: v1.1 = (f/.1)`1 by A27,FINSEQ_1:61;
A54: v1.2 = (f/.2)`1 by A27,FINSEQ_1:61;
A55: v2.1 = (f/.4)`2 by A50,FINSEQ_1:61;
A56: v2.2 = (f/.1)`2 by A50,FINSEQ_1:61;
A57: (f/.1)`1 = (f/.4)`1 by A1,A4,PSCOMP_1:85;
A58: (f/.3)`1 = (f/.2)`1 by A2,A3,PSCOMP_1:105;
A59: (f/.3)`2 = (f/.4)`2 by A3,A4,PSCOMP_1:115;
A60: (f/.2)`2 = (f/.1)`2 by A1,A2,PSCOMP_1:95;
for n,m st [n,m] in Indices G holds G*(n,m) = |[v1.n,v2.m]|
proof let n,m;
assume [n,m] in Indices G;
then A61: [n,m]in { [1,1], [1,2],[2,1], [2,2]} by Th12;
per cases by A61,ENUMSET1:18;
suppose [n,m] = [1,1];
then A62: n = 1 & m = 1 by ZFMISC_1:33;
hence G*(n,m) = f/.4 by MATRIX_2:6
.= |[v1.n,v2.m]| by A53,A55,A57,A62,EUCLID:57;
suppose [n,m] = [1,2];
then A63: n = 1 & m = 2 by ZFMISC_1:33;
hence G*(n,m) = f/.1 by MATRIX_2:6
.= |[v1.n,v2.m]| by A53,A56,A63,EUCLID:57;
suppose [n,m] = [2,1];
then A64: n = 2 & m = 1 by ZFMISC_1:33;
hence G*(n,m) = f/.3 by MATRIX_2:6
.= |[v1.n,v2.m]| by A54,A55,A58,A59,A64,EUCLID:57;
suppose [n,m] = [2,2];
then A65: n = 2 & m = 2 by ZFMISC_1:33;
hence G*(n,m) = f/.2 by MATRIX_2:6
.= |[v1.n,v2.m]| by A54,A56,A60,A65,EUCLID:57;
end;
then GoB(v1,v2) = G by A51,A52,GOBOARD2:def 1;
hence thesis by GOBOARD2:def 3;
end;
theorem Th54:
for f being rectangular special_circular_sequence holds
LeftComp f = {p : not(W-bound L~f <= p`1 & p`1 <= E-bound L~f
& S-bound L~f <= p`2 & p`2 <= N-bound L~f)} &
RightComp f = {q : W-bound L~f < q`1 & q`1 < E-bound L~f
& S-bound L~f < q`2 & q`2 < N-bound L~f}
proof let f be rectangular special_circular_sequence;
defpred U[Element of TOP-REAL 2] means
not(W-bound L~f <= $1`1 & $1`1 <= E-bound L~f
& S-bound L~f <= $1`2 & $1`2 <= N-bound L~f);
defpred V[Element of TOP-REAL 2] means
W-bound L~f < $1`1 & $1`1 < E-bound L~f
& S-bound L~f < $1`2 & $1`2 < N-bound L~f;
defpred W[Element of TOP-REAL 2] means
$1`1 = W-bound L~f & $1`2 <= N-bound L~f & $1`2 >= S-bound L~f or
$1`1 <= E-bound L~f & $1`1 >= W-bound L~f & $1`2 = N-bound L~f or
$1`1 <= E-bound L~f & $1`1 >= W-bound L~f & $1`2 = S-bound L~f or
$1`1 = E-bound L~f & $1`2 <= N-bound L~f & $1`2 >= S-bound L~f;
set LC = {p : U[p] }, RC = {q : V[q] }, Lf = {p : W[p] };
A1: L~f = Lf by Th52;
A2: W-bound L~f < E-bound L~f by SPRECT_1:33;
A3: S-bound L~f < N-bound L~f by SPRECT_1:34;
A4: LC is Subset of TOP-REAL 2 from SubsetD;
A5: RC is Subset of TOP-REAL 2 from SubsetD;
Lf is Subset of TOP-REAL 2 from SubsetD;
then reconsider Lc'=LC,Rc'=RC,Lf as Subset of TOP-REAL 2
by A4,A5;
reconsider Lc', Rc' as Subset of TOP-REAL 2;
reconsider Lf as Subset of TOP-REAL 2;
reconsider Lc=Lc', Rc=Rc' as Subset of (TOP-REAL 2)|Lf`
by A2,A3,JORDAN1:44,46;
reconsider Lc, Rc as Subset of (TOP-REAL 2)|Lf`;
A6: LeftComp f is_a_component_of (L~f)` & RightComp f is_a_component_of (L~f)`
by GOBOARD9:def 1,def 2;
Rc = Rc';
then Lc is_a_component_of (TOP-REAL 2)|Lf` by A2,A3,JORDAN1:41;
then A7: Lc' is_a_component_of Lf` by CONNSP_1:def 6;
len f > 4 by GOBOARD7:36;
then A8: 1+1 <= len f by AXIOMS:22;
1 < width GoB f by GOBOARD7:35;
then A9: 1+1 <= width GoB f by NAT_1:38;
1 <= len GoB f by GOBOARD7:34;
then A10: [1,1+1] in Indices GoB f by A9,GOBOARD7:10;
A11: GoB f = (f/.4,f/.1)][(f/.3,f/.2) by Th53;
then A12: f/.1 = (GoB f)*(1,1+1) by MATRIX_2:6;
A13: 1+1 = len GoB f by A11,MATRIX_2:3;
then A14: [1+1,1+1] in Indices GoB f by A9,GOBOARD7:10;
A15: 1+1 = width GoB f by A11,MATRIX_2:3;
A16: f/.(1+1) = (GoB f)*(1+1,1+1) by A11,MATRIX_2:6;
then A17: left_cell(f,1) = cell(GoB f,1,1+1)by A8,A10,A12,A14,GOBOARD5:29;
set p = 1/2*((GoB f)*(1,width GoB f)+(GoB f)*(1+1,width GoB f))+|[0,1]|,
q = 1/2*((GoB f)*(1,width GoB f)+(GoB f)*(1+1,width GoB f));
A18: p in Int cell(GoB f,1,1+1) by A13,A15,GOBOARD6:35;
A19: Int cell(GoB f,1,1+1) c= LeftComp f by A17,GOBOARD9:def 1;
A20: p`2 = q`2+|[0,1]|`2 by TOPREAL3:7
.= q`2+1 by EUCLID:56;
q`2 = (1/2*((GoB f)*(1,width GoB f)+f/.2))`2 by A11,A15,MATRIX_2:6
.= (1/2*(f/.1+f/.2))`2 by A11,A15,MATRIX_2:6
.= 1/2*(f/.1+f/.2)`2 by TOPREAL3:9
.= 1/2*((f/.1)`2+(f/.2)`2) by TOPREAL3:7
.= 1/2*((N-min L~f)`2+(f/.2)`2) by SPRECT_1:91
.= 1/2*((N-min L~f)`2+(N-max L~f)`2) by SPRECT_1:92
.= 1/2*(N-bound L~f+(N-max L~f)`2) by PSCOMP_1:94
.= 1/2*(N-bound L~f+N-bound L~f) by PSCOMP_1:94
.= 1/2*(2*N-bound L~f) by XCMPLX_1:11
.= N-bound L~f by XCMPLX_1:108;
then p`2 > 0 + N-bound L~f by A20,REAL_1:67;
then p in LC;
then LC meets LeftComp f by A18,A19,XBOOLE_0:3;
hence LeftComp f = LC by A1,A6,A7,GOBOARD9:3;
Lc = Lc';
then Rc is_a_component_of (TOP-REAL 2)|Lf` by A2,A3,JORDAN1:41;
then A21: Rc' is_a_component_of Lf` by CONNSP_1:def 6;
A22: right_cell(f,1) = cell(GoB f,1,1) by A8,A10,A12,A14,A16,GOBOARD5:29;
set p = 1/2*((GoB f)*(1,1)+(GoB f)*(2,2));
A23: p in Int cell(GoB f,1,1) by A13,A15,GOBOARD6:34;
A24: Int cell(GoB f,1,1) c= RightComp f by A22,GOBOARD9:def 2;
A25: p = 1/2*((GoB f)*(1,1)+f/.2) by A11,MATRIX_2:6
.= 1/2*(f/.4+f/.2) by A11,MATRIX_2:6;
A26: 1/2*(W-bound L~f) + 1/2*(W-bound L~f)
= 1/2*((W-bound L~f)+(W-bound L~f)) by XCMPLX_1:8
.= 1/2*(2*(W-bound L~f)) by XCMPLX_1:11
.= (W-bound L~f) by XCMPLX_1:108;
A27: 1/2*(S-bound L~f) + 1/2*(S-bound L~f)
= 1/2*((S-bound L~f)+(S-bound L~f)) by XCMPLX_1:8
.= 1/2*(2*(S-bound L~f)) by XCMPLX_1:11
.= (S-bound L~f) by XCMPLX_1:108;
A28: 1/2*(N-bound L~f) + 1/2*(N-bound L~f)
= 1/2*((N-bound L~f)+(N-bound L~f)) by XCMPLX_1:8
.= 1/2*(2*(N-bound L~f)) by XCMPLX_1:11
.= (N-bound L~f) by XCMPLX_1:108;
A29: 1/2*(E-bound L~f) + 1/2*(E-bound L~f)
= 1/2*((E-bound L~f)+(E-bound L~f)) by XCMPLX_1:8
.= 1/2*(2*(E-bound L~f)) by XCMPLX_1:11
.= (E-bound L~f) by XCMPLX_1:108;
A30: p`1 = 1/2*(f/.4+f/.2)`1 by A25,TOPREAL3:9
.= 1/2*((f/.4)`1+(f/.2)`1) by TOPREAL3:7
.= 1/2*(f/.4)`1+ 1/2*(f/.2)`1 by XCMPLX_1:8;
A31: p`2 = 1/2*(f/.4+f/.2)`2 by A25,TOPREAL3:9
.= 1/2*((f/.4)`2+(f/.2)`2) by TOPREAL3:7
.= 1/2*(f/.4)`2+ 1/2*(f/.2)`2 by XCMPLX_1:8;
A32: (f/.4)`1 = (W-min L~f)`1 by SPRECT_1:94
.= W-bound L~f by PSCOMP_1:84;
A33: (f/.2)`1 = (E-max L~f)`1 by SPRECT_1:92
.= E-bound L~f by PSCOMP_1:104;
A34: (f/.4)`2 = (S-min L~f)`2 by SPRECT_1:94
.= S-bound L~f by PSCOMP_1:114;
A35: (f/.2)`2 = (N-max L~f)`2 by SPRECT_1:92
.= N-bound L~f by PSCOMP_1:94;
(f/.2)`1 > W-bound L~f by A33,SPRECT_1:33;
then 1/2*(f/.2)`1 > 1/2*W-bound L~f by REAL_1:70;
then A36: W-bound L~f < p`1 by A26,A30,A32,REAL_1:53;
(f/.4)`1 < E-bound L~f by A32,SPRECT_1:33;
then 1/2*(f/.4)`1 < 1/2*E-bound L~f by REAL_1:70;
then A37: p`1 < E-bound L~f by A29,A30,A33,REAL_1:53;
(f/.2)`2 > S-bound L~f by A35,SPRECT_1:34;
then 1/2*(f/.2)`2 > 1/2*S-bound L~f by REAL_1:70;
then A38: S-bound L~f < p`2 by A27,A31,A34,REAL_1:53;
(f/.4)`2 < N-bound L~f by A34,SPRECT_1:34;
then 1/2*(f/.4)`2 < 1/2*N-bound L~f by REAL_1:70;
then p`2 < N-bound L~f by A28,A31,A35,REAL_1:53;
then p in RC by A36,A37,A38;
then RC meets RightComp f by A23,A24,XBOOLE_0:3;
hence RightComp f = RC by A1,A6,A21,GOBOARD9:3;
end;
definition
cluster clockwise_oriented (rectangular special_circular_sequence);
existence
proof
consider C being non empty compact non vertical non horizontal
Subset of TOP-REAL2;
SpStSeq C is clockwise_oriented;
hence thesis;
end;
end;
definition
cluster -> clockwise_oriented (rectangular special_circular_sequence);
coherence
proof let f be rectangular special_circular_sequence;
consider D being non vertical non horizontal non empty compact
Subset of TOP-REAL 2 such that
A1: f = SpStSeq D by SPRECT_1:def 2;
thus thesis by A1;
end;
end;
theorem
for f being rectangular special_circular_sequence,
g being S-Sequence_in_R2
st g/.1 in LeftComp f & g/.len g in RightComp f
holds Last_Point(L~g,g/.1,g/.len g,L~f) <> NW-corner L~f
proof
let f be rectangular special_circular_sequence,
g be S-Sequence_in_R2 such that
A1: g/.1 in LeftComp f and
A2: g/.len g in RightComp f;
A3: L~f meets L~g by A1,A2,Th50;
A4: L~f is closed by SPPOL_1:49;
L~f is closed & L~g is closed by SPPOL_1:49;
then A5: L~f /\ L~g is closed by TOPS_1:35;
A6: L~g is_an_arc_of g/.1, g/.len g by TOPREAL1:31;
set nw = NW-corner L~f, inw = Index(nw,g);
assume
A7: Last_Point(L~g,g/.1,g/.len g,L~f) = NW-corner L~f;
then A8: nw in L~g /\ L~f by A3,A5,A6,JORDAN5C:def 2;
then A9: nw in L~g by XBOOLE_0:def 3;
A10: L~f misses RightComp f by Th42;
A11: nw in L~f by A8,XBOOLE_0:def 3;
A12: len g in dom g by FINSEQ_5:6;
then g.len g = g/.len g by FINSEQ_4:def 4;
then A13: nw <> g.len g by A2,A10,A11,XBOOLE_0:3;
A14: inw < len g by A9,JORDAN3:41;
then A15: 1 <= inw & inw+1 <= len g by A9,JORDAN3:41,NAT_1:38;
A16: nw in LSeg(g,inw) by A9,JORDAN3:42;
A17: 1 <= inw+1 by NAT_1:29;
then A18: inw+1 in dom g by A15,FINSEQ_3:27;
A19: now
assume nw <> g.(inw+1);
then A20: nw <> g/.(inw+1) by A18,FINSEQ_4:def 4;
A21: len g >= 1 by A15,A17,AXIOMS:22;
per cases;
suppose
A22: g/.(inw+1) in L~f;
then inw+1 <> len g by A2,A10,XBOOLE_0:3;
then inw+1 < len g by A15,AXIOMS:21;
then A23: inw+1+1 <= len g by NAT_1:38;
then g/.(inw+1) in LSeg(g,inw+1) by A17,TOPREAL1:27;
then inw >= inw+1 by A3,A4,A7,A15,A16,A17,A20,A22,A23,JORDAN5C:28;
hence contradiction by REAL_1:69;
suppose not g/.(inw+1) in L~f;
then g/.(inw+1) in (L~f)` by SUBSET_1:50;
then A24: g/.(inw+1) in LeftComp f \/ RightComp f by GOBRD12:11;
A25: now
A26: RightComp f = {q : W-bound L~f < q`1 & q`1 < E-bound L~f
& S-bound L~f < q`2 & q`2 < N-bound L~f} by Th54;
assume g/.(inw+1) in RightComp f;
then A27: ex q st g/.(inw+1) = q &
W-bound L~f < q`1 & q`1 < E-bound L~f &
S-bound L~f < q`2 & q`2 < N-bound L~f by A26;
A28: LSeg(g,inw) = LSeg(g/.inw,g/.(inw+1)) by A15,TOPREAL1:def 5;
LSeg(g,inw) is vertical or LSeg(g,inw) is horizontal by SPPOL_1:41;
then (g/.(inw+1))`1 = nw`1 or (g/.(inw+1))`2 = nw`2 by A16,A28,Th19,Th20;
hence contradiction by A27,PSCOMP_1:74,75;
end;
then A29: g/.(inw+1) in LeftComp f by A24,XBOOLE_0:def 2;
A30: inw+1<len g by A2,A15,A25,AXIOMS:21;
reconsider m = mid(g,inw+1,len g) as S-Sequence_in_R2
by A2,A15,A17,A21,A25,JORDAN3:39;
A31: m/.1 in LeftComp f by A12,A18,A29,SPRECT_2:12;
m/.len m in RightComp f by A2,A12,A18,SPRECT_2:13;
then L~f meets L~m by A31,Th50;
then consider q being set such that
A32: q in L~f and
A33: q in L~m by XBOOLE_0:3;
reconsider q as Point of TOP-REAL 2 by A33;
consider i such that
A34: 1 <= i & i+1 <= len m and
A35: q in LSeg(m,i) by A33,SPPOL_2:13;
A36: len m = len g-'(inw+1)+1 by A15,A17,JORDAN4:20;
i < len m by A34,NAT_1:38;
then A37: LSeg(m,i)=LSeg(g,i+(inw+1)-'1) by A17,A30,A34,A36,JORDAN4:31;
set j = i+(inw+1)-'1;
A38: j = i+inw+1-'1 by XCMPLX_1:1
.= i+inw by BINARITH:39;
inw >= 0 by NAT_1:18;
then A39: 0+1 <= j by A34,A38,REAL_1:55;
len m = len g -' inw by A14,A36,NAT_2:9;
then len m + inw = len g by A14,AMI_5:4;
then i+1 + inw <= len g by A34,AXIOMS:24;
then A40: j + 1 <= len g by A38,XCMPLX_1:1;
A41: j >= inw+1 by A34,A38,AXIOMS:24;
now assume nw = q;
then A42: nw in LSeg(g,inw) /\ LSeg(g,j) by A16,A35,A37,XBOOLE_0:def 3;
then A43: LSeg(g,inw) meets LSeg(g,j) by XBOOLE_0:4;
per cases by A41,AXIOMS:21;
suppose
A44: inw+1 = j;
inw+1+1 <= len g by A30,NAT_1:38;
then inw + (1+1) <= len g by XCMPLX_1:1;
then LSeg(g,inw) /\ LSeg(g,inw+1) = {g/.(inw+1)} by A15,TOPREAL1:def 8;
hence contradiction by A20,A42,A44,TARSKI:def 1;
suppose inw+1 < j;
hence contradiction by A43,TOPREAL1:def 9;
end;
then inw >= j by A3,A4,A7,A15,A16,A32,A35,A37,A39,A40,JORDAN5C:28;
then inw >= inw+1 by A41,AXIOMS:22;
hence contradiction by REAL_1:69;
end;
then A45: inw+1 < len g by A13,A15,AXIOMS:21;
then A46: inw+1+1 <= len g by NAT_1:38;
A47: 1 <= inw+1+1 by NAT_1:29;
then A48: inw+1+1 in dom g by A46,FINSEQ_3:27;
g/.(inw+1) in LSeg(g,inw+1) by A17,A46,TOPREAL1:27;
then A49: nw in LSeg(g,inw+1) by A18,A19,FINSEQ_4:def 4;
inw+1 < inw+1+1 by NAT_1:38;
then A50: nw <> g.(inw+1+1) by A18,A19,A48,FUNCT_1:def 8;
then A51: nw <> g/.(inw+1+1) by A48,FINSEQ_4:def 4;
A52: len g >= 1 by A46,A47,AXIOMS:22;
per cases;
suppose
A53: g/.(inw+1+1) in L~f;
then inw+1+1 <> len g by A2,A10,XBOOLE_0:3;
then inw+1+1 < len g by A46,AXIOMS:21;
then A54: inw+1+1+1 <= len g by NAT_1:38;
then A55: g/.(inw+1+1) in LSeg(g,inw+1+1) by A47,TOPREAL1:27;
nw <> g/.(inw+1+1) by A48,A50,FINSEQ_4:def 4;
then inw+1 >= inw+1+1 by A3,A4,A7,A17,A46,A47,A49,A53,A54,A55,JORDAN5C:28;
hence contradiction by REAL_1:69;
suppose not g/.(inw+1+1) in L~f;
then g/.(inw+1+1) in (L~f)` by SUBSET_1:50;
then A56: g/.(inw+1+1) in LeftComp f \/ RightComp f by GOBRD12:11;
A57: now
A58: RightComp f = {q : W-bound L~f < q`1 & q`1 < E-bound L~f
& S-bound L~f < q`2 & q`2 < N-bound L~f} by Th54;
assume g/.(inw+1+1) in RightComp f;
then A59: ex q st g/.(inw+1+1) = q &
W-bound L~f < q`1 & q`1 < E-bound L~f &
S-bound L~f < q`2 & q`2 < N-bound L~f by A58;
A60: LSeg(g,inw+1) = LSeg(g/.(inw+1),g/.(inw+1+1))
by A17,A46,TOPREAL1:def 5;
LSeg(g,inw+1) is vertical or LSeg(g,inw+1) is horizontal by SPPOL_1:41;
then (g/.(inw+1+1))`1 = nw`1 or (g/.(inw+1+1))`2 = nw`2
by A49,A60,Th19,Th20;
hence contradiction by A59,PSCOMP_1:74,75;
end;
then A61: g/.(inw+1+1) in LeftComp f by A56,XBOOLE_0:def 2;
A62: inw+1+1<len g by A2,A46,A57,AXIOMS:21;
reconsider m = mid(g,inw+1+1,len g) as S-Sequence_in_R2
by A2,A46,A47,A52,A57,JORDAN3:39;
A63: m/.1 in LeftComp f by A12,A48,A61,SPRECT_2:12;
m/.len m in RightComp f by A2,A12,A48,SPRECT_2:13;
then L~f meets L~m by A63,Th50;
then consider q being set such that
A64: q in L~f and
A65: q in L~m by XBOOLE_0:3;
reconsider q as Point of TOP-REAL 2 by A65;
consider i such that
A66: 1 <= i & i+1 <= len m and
A67: q in LSeg(m,i) by A65,SPPOL_2:13;
A68: len m = len g-'(inw+1+1)+1 by A46,A47,JORDAN4:20;
i < len m by A66,NAT_1:38;
then A69: LSeg(m,i)=LSeg(g,i+(inw+1+1)-'1) by A47,A62,A66,A68,JORDAN4:31;
set j = i+(inw+1+1)-'1;
A70: j = i+(inw+1)+1-'1 by XCMPLX_1:1
.= i+inw+1+1-'1 by XCMPLX_1:1
.= i+inw+1 by BINARITH:39;
then A71: 0+1 <= j by NAT_1:29;
len m = len g -' (inw+1) by A45,A68,NAT_2:9;
then len m + (inw+1) = len g by A15,AMI_5:4;
then i+ 1 + (inw +1) <= len g by A66,AXIOMS:24;
then i+ 1 + inw +1 <= len g by XCMPLX_1:1;
then A72: j + 1 <= len g by A70,XCMPLX_1:1;
j = i+(inw+1) by A70,XCMPLX_1:1;
then A73: j >= inw+1+1 by A66,AXIOMS:24;
now assume nw = q;
then A74: nw in LSeg(g,inw+1) /\ LSeg(g,j) by A49,A67,A69,XBOOLE_0:def 3;
then A75: LSeg(g,inw+1) meets LSeg(g,j) by XBOOLE_0:4;
per cases by A73,AXIOMS:21;
suppose
A76: inw+1+1 = j;
inw+1+1+1 <= len g by A62,NAT_1:38;
then inw+1 + (1+1) <= len g by XCMPLX_1:1;
then LSeg(g,inw+1) /\ LSeg(g,inw+1+1) = {g/.(inw+1+1)}
by A17,TOPREAL1:def 8;
hence contradiction by A51,A74,A76,TARSKI:def 1;
suppose inw+1+1 < j;
hence contradiction by A75,TOPREAL1:def 9;
end;
then inw+1 >= j by A3,A4,A7,A17,A46,A49,A64,A67,A69,A71,A72,JORDAN5C:28;
then inw+1 >= inw+1+1 by A73,AXIOMS:22;
hence contradiction by REAL_1:69;
end;
theorem
for f being rectangular special_circular_sequence,
g being S-Sequence_in_R2
st g/.1 in LeftComp f & g/.len g in RightComp f
holds Last_Point(L~g,g/.1,g/.len g,L~f) <> SE-corner L~f
proof
let f be rectangular special_circular_sequence,
g be S-Sequence_in_R2 such that
A1: g/.1 in LeftComp f and
A2: g/.len g in RightComp f;
A3: L~f meets L~g by A1,A2,Th50;
A4: L~f is closed by SPPOL_1:49;
L~f is closed & L~g is closed by SPPOL_1:49;
then A5: L~f /\ L~g is closed by TOPS_1:35;
A6: L~g is_an_arc_of g/.1, g/.len g by TOPREAL1:31;
set se = SE-corner L~f, ise = Index(se,g);
assume
A7: Last_Point(L~g,g/.1,g/.len g,L~f) = SE-corner L~f;
then A8: se in L~g /\ L~f by A3,A5,A6,JORDAN5C:def 2;
then A9: se in L~g by XBOOLE_0:def 3;
A10: L~f misses RightComp f by Th42;
A11: se in L~f by A8,XBOOLE_0:def 3;
A12: len g in dom g by FINSEQ_5:6;
then g.len g = g/.len g by FINSEQ_4:def 4;
then A13: se <> g.len g by A2,A10,A11,XBOOLE_0:3;
A14: ise < len g by A9,JORDAN3:41;
then A15: 1 <= ise & ise+1 <= len g by A9,JORDAN3:41,NAT_1:38;
A16: se in LSeg(g,ise) by A9,JORDAN3:42;
A17: 1 <= ise+1 by NAT_1:29;
then A18: ise+1 in dom g by A15,FINSEQ_3:27;
A19: now
assume se <> g.(ise+1);
then A20: se <> g/.(ise+1) by A18,FINSEQ_4:def 4;
A21: len g >= 1 by A15,A17,AXIOMS:22;
per cases;
suppose
A22: g/.(ise+1) in L~f;
then ise+1 <> len g by A2,A10,XBOOLE_0:3;
then ise+1 < len g by A15,AXIOMS:21;
then A23: ise+1+1 <= len g by NAT_1:38;
then g/.(ise+1) in LSeg(g,ise+1) by A17,TOPREAL1:27;
then ise >= ise+1 by A3,A4,A7,A15,A16,A17,A20,A22,A23,JORDAN5C:28;
hence contradiction by REAL_1:69;
suppose not g/.(ise+1) in L~f;
then g/.(ise+1) in (L~f)` by SUBSET_1:50;
then A24: g/.(ise+1) in LeftComp f \/ RightComp f by GOBRD12:11;
A25: now
A26: RightComp f = {q : W-bound L~f < q`1 & q`1 < E-bound L~f
& S-bound L~f < q`2 & q`2 < N-bound L~f} by Th54;
assume g/.(ise+1) in RightComp f;
then A27: ex q st g/.(ise+1) = q &
W-bound L~f < q`1 & q`1 < E-bound L~f &
S-bound L~f < q`2 & q`2 < N-bound L~f by A26;
A28: LSeg(g,ise) = LSeg(g/.ise,g/.(ise+1)) by A15,TOPREAL1:def 5;
LSeg(g,ise) is vertical or LSeg(g,ise) is horizontal by SPPOL_1:41;
then (g/.(ise+1))`1 = se`1 or (g/.(ise+1))`2 = se`2 by A16,A28,Th19,Th20;
hence contradiction by A27,PSCOMP_1:78,79;
end;
then A29: g/.(ise+1) in LeftComp f by A24,XBOOLE_0:def 2;
A30: ise+1<len g by A2,A15,A25,AXIOMS:21;
reconsider m = mid(g,ise+1,len g) as S-Sequence_in_R2
by A2,A15,A17,A21,A25,JORDAN3:39;
A31: m/.1 in LeftComp f by A12,A18,A29,SPRECT_2:12;
m/.len m in RightComp f by A2,A12,A18,SPRECT_2:13;
then L~f meets L~m by A31,Th50;
then consider q being set such that
A32: q in L~f and
A33: q in L~m by XBOOLE_0:3;
reconsider q as Point of TOP-REAL 2 by A33;
consider i such that
A34: 1 <= i & i+1 <= len m and
A35: q in LSeg(m,i) by A33,SPPOL_2:13;
A36: len m = len g-'(ise+1)+1 by A15,A17,JORDAN4:20;
i < len m by A34,NAT_1:38;
then A37: LSeg(m,i)=LSeg(g,i+(ise+1)-'1) by A17,A30,A34,A36,JORDAN4:31;
set j = i+(ise+1)-'1;
A38: j = i+ise+1-'1 by XCMPLX_1:1
.= i+ise by BINARITH:39;
ise >= 0 by NAT_1:18;
then A39: 0+1 <= j by A34,A38,REAL_1:55;
len m = len g -' ise by A14,A36,NAT_2:9;
then len m + ise = len g by A14,AMI_5:4;
then i+1 + ise <= len g by A34,AXIOMS:24;
then A40: j + 1 <= len g by A38,XCMPLX_1:1;
A41: j >= ise+1 by A34,A38,AXIOMS:24;
now assume se = q;
then A42: se in LSeg(g,ise) /\ LSeg(g,j) by A16,A35,A37,XBOOLE_0:def 3;
then A43: LSeg(g,ise) meets LSeg(g,j) by XBOOLE_0:4;
per cases by A41,AXIOMS:21;
suppose
A44: ise+1 = j;
ise+1+1 <= len g by A30,NAT_1:38;
then ise + (1+1) <= len g by XCMPLX_1:1;
then LSeg(g,ise) /\ LSeg(g,ise+1) = {g/.(ise+1)} by A15,TOPREAL1:def 8;
hence contradiction by A20,A42,A44,TARSKI:def 1;
suppose ise+1 < j;
hence contradiction by A43,TOPREAL1:def 9;
end;
then ise >= j by A3,A4,A7,A15,A16,A32,A35,A37,A39,A40,JORDAN5C:28;
then ise >= ise+1 by A41,AXIOMS:22;
hence contradiction by REAL_1:69;
end;
then A45: ise+1 < len g by A13,A15,AXIOMS:21;
then A46: ise+1+1 <= len g by NAT_1:38;
A47: 1 <= ise+1+1 by NAT_1:29;
then A48: ise+1+1 in dom g by A46,FINSEQ_3:27;
g/.(ise+1) in LSeg(g,ise+1) by A17,A46,TOPREAL1:27;
then A49: se in LSeg(g,ise+1) by A18,A19,FINSEQ_4:def 4;
ise+1 < ise+1+1 by NAT_1:38;
then A50: se <> g.(ise+1+1) by A18,A19,A48,FUNCT_1:def 8;
then A51: se <> g/.(ise+1+1) by A48,FINSEQ_4:def 4;
A52: len g >= 1 by A46,A47,AXIOMS:22;
per cases;
suppose
A53: g/.(ise+1+1) in L~f;
then ise+1+1 <> len g by A2,A10,XBOOLE_0:3;
then ise+1+1 < len g by A46,AXIOMS:21;
then A54: ise+1+1+1 <= len g by NAT_1:38;
then A55: g/.(ise+1+1) in LSeg(g,ise+1+1) by A47,TOPREAL1:27;
se <> g/.(ise+1+1) by A48,A50,FINSEQ_4:def 4;
then ise+1 >= ise+1+1 by A3,A4,A7,A17,A46,A47,A49,A53,A54,A55,JORDAN5C:28;
hence contradiction by REAL_1:69;
suppose not g/.(ise+1+1) in L~f;
then g/.(ise+1+1) in (L~f)` by SUBSET_1:50;
then A56: g/.(ise+1+1) in LeftComp f \/ RightComp f by GOBRD12:11;
A57: now
A58: RightComp f = {q : W-bound L~f < q`1 & q`1 < E-bound L~f
& S-bound L~f < q`2 & q`2 < N-bound L~f} by Th54;
assume g/.(ise+1+1) in RightComp f;
then A59: ex q st g/.(ise+1+1) = q &
W-bound L~f < q`1 & q`1 < E-bound L~f &
S-bound L~f < q`2 & q`2 < N-bound L~f by A58;
A60: LSeg(g,ise+1) = LSeg(g/.(ise+1),g/.(ise+1+1))
by A17,A46,TOPREAL1:def 5;
LSeg(g,ise+1) is vertical or LSeg(g,ise+1) is horizontal by SPPOL_1:41;
then (g/.(ise+1+1))`1 = se`1 or (g/.(ise+1+1))`2 = se`2
by A49,A60,Th19,Th20;
hence contradiction by A59,PSCOMP_1:78,79;
end;
then A61: g/.(ise+1+1) in LeftComp f by A56,XBOOLE_0:def 2;
A62: ise+1+1<len g by A2,A46,A57,AXIOMS:21;
reconsider m = mid(g,ise+1+1,len g) as S-Sequence_in_R2
by A2,A46,A47,A52,A57,JORDAN3:39;
A63: m/.1 in LeftComp f by A12,A48,A61,SPRECT_2:12;
m/.len m in RightComp f by A2,A12,A48,SPRECT_2:13;
then L~f meets L~m by A63,Th50;
then consider q being set such that
A64: q in L~f and
A65: q in L~m by XBOOLE_0:3;
reconsider q as Point of TOP-REAL 2 by A65;
consider i such that
A66: 1 <= i & i+1 <= len m and
A67: q in LSeg(m,i) by A65,SPPOL_2:13;
A68: len m = len g-'(ise+1+1)+1 by A46,A47,JORDAN4:20;
i < len m by A66,NAT_1:38;
then A69: LSeg(m,i)=LSeg(g,i+(ise+1+1)-'1) by A47,A62,A66,A68,JORDAN4:31;
set j = i+(ise+1+1)-'1;
A70: j = i+(ise+1)+1-'1 by XCMPLX_1:1
.= i+ise+1+1-'1 by XCMPLX_1:1
.= i+ise+1 by BINARITH:39;
then A71: 0+1 <= j by NAT_1:29;
len m = len g -' (ise+1) by A45,A68,NAT_2:9;
then len m + (ise+1) = len g by A15,AMI_5:4;
then i+ 1 + (ise +1) <= len g by A66,AXIOMS:24;
then i+ 1 + ise +1 <= len g by XCMPLX_1:1;
then A72: j + 1 <= len g by A70,XCMPLX_1:1;
j = i+(ise+1) by A70,XCMPLX_1:1;
then A73: j >= ise+1+1 by A66,AXIOMS:24;
now assume se = q;
then A74: se in LSeg(g,ise+1) /\ LSeg(g,j) by A49,A67,A69,XBOOLE_0:def 3;
then A75: LSeg(g,ise+1) meets LSeg(g,j) by XBOOLE_0:4;
per cases by A73,AXIOMS:21;
suppose
A76: ise+1+1 = j;
ise+1+1+1 <= len g by A62,NAT_1:38;
then ise+1 + (1+1) <= len g by XCMPLX_1:1;
then LSeg(g,ise+1) /\ LSeg(g,ise+1+1) = {g/.(ise+1+1)}
by A17,TOPREAL1:def 8;
hence contradiction by A51,A74,A76,TARSKI:def 1;
suppose ise+1+1 < j;
hence contradiction by A75,TOPREAL1:def 9;
end;
then ise+1 >= j by A3,A4,A7,A17,A46,A49,A64,A67,A69,A71,A72,JORDAN5C:28;
then ise+1 >= ise+1+1 by A73,AXIOMS:22;
hence contradiction by REAL_1:69;
end;
theorem Th57:
for f being rectangular special_circular_sequence,
p being Point of TOP-REAL 2 st
W-bound L~f > p`1 or p`1 > E-bound L~f or
S-bound L~f > p`2 or p`2 > N-bound L~f
holds p in LeftComp f
proof
let f be rectangular special_circular_sequence,
p be Point of TOP-REAL 2;
LeftComp f = {q : not(W-bound L~f <= q`1 & q`1 <= E-bound L~f
& S-bound L~f <= q`2 & q`2 <= N-bound L~f)} by Th54;
hence thesis;
end;
theorem
for f being
clockwise_oriented (non constant standard special_circular_sequence)
st f/.1 = N-min L~f
holds LeftComp SpStSeq L~f c= LeftComp f
proof
let f be clockwise_oriented (non constant standard special_circular_sequence)
such that
A1: f/.1 = N-min L~f;
A2: LeftComp f is_a_component_of (L~f)` by GOBOARD9:def 1;
LeftComp SpStSeq L~f is_a_component_of (L~SpStSeq L~f)` by GOBOARD9:def 1;
then consider B1 being Subset of (TOP-REAL 2)|(L~SpStSeq L~f)`
such that
A3: B1 = LeftComp SpStSeq L~f and
A4: B1 is_a_component_of (TOP-REAL 2)|(L~SpStSeq L~f)` by CONNSP_1:def 6;
B1 is connected by A4,CONNSP_1:def 5;
then A5: LeftComp SpStSeq L~f is connected by A3,CONNSP_1:24;
consider i such that
A6: 1 <= i & i < len GoB f and
A7: N-min L~f = (GoB f)*(i,width GoB f) by Th45;
A8: i in dom GoB f by A6,FINSEQ_3:27;
then A9: f/.2 = (GoB f)*(i+1,width GoB f) by A1,A7,Th46;
A10: width GoB f >= 1 by GOBRD11:34;
then A11: width GoB f -' 1 + 1 = width GoB f by AMI_5:4;
len f > 4 by GOBOARD7:36;
then A12: 1+1 <= len f by AXIOMS:22;
A13: [i,width GoB f] in Indices GoB f by A6,A10,GOBOARD7:10;
A14: 1 <= i+1 & i+1 <= len GoB f by A6,NAT_1:38;
then [i+1,width GoB f] in Indices GoB f by A10,GOBOARD7:10;
then A15: left_cell(f,1) = cell(GoB f,i,width GoB f) by A1,A7,A9,A11,A12,A13,
GOBOARD5:29;
set a = 1/2*((GoB f)*(i,width GoB f)+(GoB f)*(i+1,width GoB f))+|[0,1]|,
q = 1/2*((GoB f)*(i,width GoB f)+(GoB f)*(i+1,width GoB f));
A16: a in Int cell(GoB f,i,width GoB f) by A6,A14,GOBOARD6:35;
A17: Int cell(GoB f,i,width GoB f) c= LeftComp f by A15,GOBOARD9:def 1;
A18: a`2 = q`2+|[0,1]|`2 by TOPREAL3:7
.= q`2+1 by EUCLID:56;
A19: N-bound L~SpStSeq L~f = N-bound L~f by SPRECT_1:68;
A20: (f/.2)`2 = ((GoB f)*(1,width GoB f))`2 by A9,A10,A14,GOBOARD5:2
.= (N-min L~f)`2 by A6,A7,A10,GOBOARD5:2
.= N-bound L~f by PSCOMP_1:94;
A21: LeftComp SpStSeq L~f =
{p : not(W-bound L~SpStSeq L~f <= p`1 & p`1 <= E-bound L~SpStSeq L~f
& S-bound L~SpStSeq L~f <= p`2 & p`2 <= N-bound L~SpStSeq L~f)}
by Th54;
q`2 = (1/2*((GoB f)*(i,width GoB f)+f/.2))`2 by A1,A7,A8,Th46
.= 1/2*(f/.1+f/.2)`2 by A1,A7,TOPREAL3:9
.= 1/2*((f/.1)`2+(f/.2)`2) by TOPREAL3:7
.= 1/2*(N-bound L~f+N-bound L~f) by A1,A20,PSCOMP_1:94
.= 1/2*(2*N-bound L~f) by XCMPLX_1:11
.= N-bound L~f by XCMPLX_1:108;
then a`2 > 0 + N-bound L~f by A18,REAL_1:67;
then a`2 > N-bound L~SpStSeq L~f by SPRECT_1:68;
then a in LeftComp SpStSeq L~f by A21;
then A22: LeftComp f meets LeftComp SpStSeq L~f by A16,A17,XBOOLE_0:3;
defpred X[Element of TOP-REAL 2] means $1`2 < S-bound L~f;
reconsider P1 = { p: X[p] }
as Subset of TOP-REAL 2 from SubsetD;
defpred X[Element of TOP-REAL 2] means $1`2 > N-bound L~f;
reconsider P2 = { p: X[p] }
as Subset of TOP-REAL 2 from SubsetD;
defpred X[Element of TOP-REAL 2] means $1`1 > E-bound L~f;
reconsider P3 = { p: X[p] }
as Subset of TOP-REAL 2 from SubsetD;
defpred X[Element of TOP-REAL 2] means $1`1 < W-bound L~f;
reconsider P4 = { p: X[p] }
as Subset of TOP-REAL 2 from SubsetD;
A23: W-bound L~SpStSeq L~f = W-bound L~f by SPRECT_1:66;
A24: S-bound L~SpStSeq L~f = S-bound L~f by SPRECT_1:67;
A25: E-bound L~SpStSeq L~f = E-bound L~f by SPRECT_1:69;
A26: LeftComp SpStSeq L~f = P1 \/ P2 \/ (P3 \/ P4)
proof
thus LeftComp SpStSeq L~f c= P1 \/ P2 \/ (P3 \/ P4)
proof let x be set;
assume x in LeftComp SpStSeq L~f;
then x in { p : not(W-bound L~f <= p`1 & p`1 <= E-bound L~f
& S-bound L~f <= p`2 & p`2 <= N-bound L~f)}
by A19,A23,A24,A25,Th54;
then ex p st p = x & not(W-bound L~f <= p`1 & p`1 <= E-bound L~f
& S-bound L~f <= p`2 & p`2 <= N-bound L~f);
then x in P1 or x in P2 or x in P3 or x in P4;
then x in P1 \/ P2 or x in P3 \/ P4 by XBOOLE_0:def 2;
hence thesis by XBOOLE_0:def 2;
end;
let x be set;
assume x in P1 \/ P2 \/ (P3 \/ P4);
then A27: x in P1 \/ P2 or x in P3 \/ P4 by XBOOLE_0:def 2;
per cases by A27,XBOOLE_0:def 2;
suppose x in P1;
then ex p st x = p & p`2 < S-bound L~f;
hence x in LeftComp SpStSeq L~f by A24,Th57;
suppose x in P2;
then ex p st x = p & p`2 > N-bound L~f;
hence x in LeftComp SpStSeq L~f by A19,Th57;
suppose x in P3;
then ex p st x = p & p`1 > E-bound L~f;
hence x in LeftComp SpStSeq L~f by A25,Th57;
suppose x in P4;
then ex p st x = p & p`1 < W-bound L~f;
hence x in LeftComp SpStSeq L~f by A23,Th57;
end;
for p st p in P1 holds p`2 < (GoB f)*(1,1)`2
proof let p;
assume p in P1;
then ex q st p = q & q`2 < S-bound L~f;
hence p`2 < (GoB f)*(1,1)`2 by JORDAN5D:40;
end;
then A28: P1 misses L~f by GOBOARD8:23;
for p st p in P2 holds p`2 > (GoB f)*(1, width GoB f)`2
proof let p;
assume p in P2;
then ex q st p = q & q`2 > N-bound L~f;
hence p`2 > (GoB f)*(1,width GoB f)`2 by JORDAN5D:42;
end;
then P2 misses L~f by GOBOARD8:24;
then A29: P1 \/ P2 misses L~f by A28,XBOOLE_1:70;
for p st p in P3 holds p`1 > (GoB f)*(len GoB f,1)`1
proof let p;
assume p in P3;
then ex q st p = q & q`1 > E-bound L~f;
hence p`1 > (GoB f)*(len GoB f,1)`1 by JORDAN5D:41;
end;
then A30: P3 misses L~f by GOBOARD8:22;
for p st p in P4 holds p`1 < (GoB f)*(1,1)`1
proof let p;
assume p in P4;
then ex q st p = q & q`1 < W-bound L~f;
hence p`1 < (GoB f)*(1,1)`1 by JORDAN5D:39;
end;
then P4 misses L~f by GOBOARD8:21;
then P3 \/ P4 misses L~f by A30,XBOOLE_1:70;
then LeftComp SpStSeq L~f misses L~f by A26,A29,XBOOLE_1:70;
then LeftComp SpStSeq L~f c= (L~f)` by SUBSET_1:43;
hence LeftComp SpStSeq L~f c= LeftComp f by A2,A5,A22,GOBOARD9:6;
end;
begin :: In the area
theorem Th59:
for f being FinSequence of TOP-REAL 2,
p,q being Point of TOP-REAL 2 holds <*p,q*> is_in_the_area_of f
iff <*p*> is_in_the_area_of f &
<*q*> is_in_the_area_of f
proof let f be FinSequence of TOP-REAL 2,
p,q be Point of TOP-REAL 2;
thus <*p,q*> is_in_the_area_of f
implies <*p*> is_in_the_area_of f & <*q*> is_in_the_area_of f
proof assume
A1: <*p,q*> is_in_the_area_of f;
dom<*p,q*> = {1,2} by FINSEQ_1:4,FINSEQ_3:29;
then 1 in dom<*p,q*> & <*p,q*>/.1 = p & 2 in
dom<*p,q*> & <*p,q*>/.2 = q by FINSEQ_4:26,TARSKI:def 2;
then A2: W-bound L~f <= p`1 & p`1 <= E-bound L~f &
S-bound L~f <= p`2 & p`2 <= N-bound L~f &
W-bound L~f <= q`1 & q`1 <= E-bound L~f &
S-bound L~f <= q`2 & q`2 <= N-bound L~f by A1,SPRECT_2:def 1;
thus <*p*> is_in_the_area_of f
proof let i;
assume i in dom<*p*>;
then i in {1} by FINSEQ_1:4,55;
then i = 1 by TARSKI:def 1;
hence thesis by A2,FINSEQ_4:25;
end;
let i;
assume i in dom<*q*>;
then i in {1} by FINSEQ_1:4,55;
then i = 1 by TARSKI:def 1;
hence thesis by A2,FINSEQ_4:25;
end;
assume
A3: <*p*> is_in_the_area_of f;
dom<*p*> = {1} by FINSEQ_1:4,55;
then 1 in dom<*p*> & <*p*>/.1 = p by FINSEQ_4:25,TARSKI:def 1;
then A4: W-bound L~f <= p`1 & p`1 <= E-bound L~f &
S-bound L~f <= p`2 & p`2 <= N-bound L~f by A3,SPRECT_2:def 1;
assume
A5: <*q*> is_in_the_area_of f;
dom<*q*> = {1} by FINSEQ_1:4,55;
then 1 in dom<*q*> & <*q*>/.1 = q by FINSEQ_4:25,TARSKI:def 1;
then A6: W-bound L~f <= q`1 & q`1 <= E-bound L~f &
S-bound L~f <= q`2 & q`2 <= N-bound L~f by A5,SPRECT_2:def 1;
let i;
assume i in dom<*p,q*>;
then i in {1,2} by FINSEQ_1:4,FINSEQ_3:29;
then i =1 or i =2 by TARSKI:def 2;
hence thesis by A4,A6,FINSEQ_4:26;
end;
theorem Th60:
for f being rectangular FinSequence of TOP-REAL 2,
p being Point of TOP-REAL 2
st <*p*> is_in_the_area_of f &
(p`1 = W-bound L~f or p`1 = E-bound L~f or
p`2 = S-bound L~f or p`2 = N-bound L~f)
holds p in L~f
proof let f be rectangular FinSequence of TOP-REAL 2,
p be Point of TOP-REAL 2;
assume
A1: <*p*> is_in_the_area_of f;
dom<*p*> = {1} by FINSEQ_1:4,55;
then 1 in dom<*p*> & <*p*>/.1 = p by FINSEQ_4:25,TARSKI:def 1;
then A2: W-bound L~f <= p`1 & p`1 <= E-bound L~f &
S-bound L~f <= p`2 & p`2 <= N-bound L~f by A1,SPRECT_2:def 1;
consider D being non vertical non horizontal non empty compact
Subset of TOP-REAL 2
such that
A3: f = SpStSeq D by SPRECT_1:def 2;
A4: L~f = (LSeg(NW-corner D,NE-corner D) \/ LSeg(NE-corner D,SE-corner D)) \/
(LSeg(SE-corner D,SW-corner D) \/ LSeg(SW-corner D,NW-corner D))
by A3,SPRECT_1:43;
A5: W-bound L~SpStSeq D = W-bound D by SPRECT_1:66;
A6: S-bound L~SpStSeq D = S-bound D by SPRECT_1:67;
A7: N-bound L~SpStSeq D = N-bound D by SPRECT_1:68;
A8: E-bound L~SpStSeq D = E-bound D by SPRECT_1:69;
assume
A9: p`1 = W-bound L~f or p`1 = E-bound L~f or
p`2 = S-bound L~f or p`2 = N-bound L~f;
per cases by A9;
suppose
A10: p`1 = W-bound L~f;
A11: (SW-corner D)`1 = W-bound D & (NW-corner D)`1 = W-bound D
by PSCOMP_1:72,74;
(SW-corner D)`2 = S-bound D & (NW-corner D)`2 = N-bound D
by PSCOMP_1:73,75;
then p in
LSeg(SW-corner D,NW-corner D) by A2,A3,A5,A6,A7,A10,A11,GOBOARD7:8;
then p in LSeg(SE-corner D,SW-corner D) \/ LSeg(SW-corner D,NW-corner D)
by XBOOLE_0:def 2;
hence p in L~f by A4,XBOOLE_0:def 2;
suppose
A12: p`1 = E-bound L~f;
A13: (NE-corner D)`1 = E-bound D & (SE-corner D)`1 = E-bound D
by PSCOMP_1:76,78;
(NE-corner D)`2 = N-bound D & (SE-corner D)`2 = S-bound D
by PSCOMP_1:77,79;
then p in
LSeg(NE-corner D,SE-corner D) by A2,A3,A6,A7,A8,A12,A13,GOBOARD7:8;
then p in LSeg(NW-corner D,NE-corner D) \/ LSeg(NE-corner D,SE-corner D)
by XBOOLE_0:def 2;
hence p in L~f by A4,XBOOLE_0:def 2;
suppose
A14: p`2 = S-bound L~f;
A15: (SE-corner D)`1 = E-bound D & (SW-corner D)`1 = W-bound D
by PSCOMP_1:72,78;
(SE-corner D)`2 = S-bound D & (SW-corner D)`2 = S-bound D
by PSCOMP_1:73,79;
then p in
LSeg(SE-corner D,SW-corner D) by A2,A3,A5,A6,A8,A14,A15,GOBOARD7:9;
then p in LSeg(SE-corner D,SW-corner D) \/ LSeg(SW-corner D,NW-corner D)
by XBOOLE_0:def 2;
hence p in L~f by A4,XBOOLE_0:def 2;
suppose
A16: p`2 = N-bound L~f;
A17: (NW-corner D)`1 = W-bound D & (NE-corner D)`1 = E-bound D
by PSCOMP_1:74,76;
(NW-corner D)`2 = N-bound D & (NE-corner D)`2 = N-bound D
by PSCOMP_1:75,77;
then p in
LSeg(NW-corner D,NE-corner D) by A2,A3,A5,A7,A8,A16,A17,GOBOARD7:9;
then p in LSeg(NW-corner D,NE-corner D) \/ LSeg(NE-corner D,SE-corner D)
by XBOOLE_0:def 2;
hence p in L~f by A4,XBOOLE_0:def 2;
end;
theorem Th61:
for f being FinSequence of TOP-REAL 2,
p,q being Point of TOP-REAL 2, r being Real
st 0<=r & r <= 1 & <*p,q*> is_in_the_area_of f
holds <*(1-r)*p+r*q*> is_in_the_area_of f
proof
let f be FinSequence of TOP-REAL 2,
p,q be Point of TOP-REAL 2, r be Real such that
A1: 0 <= r and
A2: r <= 1 and
A3: <*p,q*> is_in_the_area_of f;
dom<*p,q*> = {1,2} by FINSEQ_1:4,FINSEQ_3:29;
then 1 in dom<*p,q*> & <*p,q*>/.1 = p & 2 in
dom<*p,q*> & <*p,q*>/.2 = q by FINSEQ_4:26,TARSKI:def 2;
then A4: W-bound L~f <= p`1 & p`1 <= E-bound L~f &
S-bound L~f <= p`2 & p`2 <= N-bound L~f &
W-bound L~f <= q`1 & q`1 <= E-bound L~f &
S-bound L~f <= q`2 & q`2 <= N-bound L~f by A3,SPRECT_2:def 1;
let n;
assume
A5: n in dom <*(1-r)*p+r*q*>;
dom <*(1-r)*p+r*q*> = {1} by FINSEQ_1:4,55;
then A6: n = 1 by A5,TARSKI:def 1;
A7: ((1-r)*p+r*q)`1 = ((1-r)*p)`1+(r*q)`1 by TOPREAL3:7
.= (1-r)*p`1+(r*q)`1 by TOPREAL3:9
.= (1-r)*p`1+r*q`1 by TOPREAL3:9;
A8: (1-r)*W-bound L~f+r*W-bound L~f = ((1-r)+r)*W-bound L~f by XCMPLX_1:8
.= 1*W-bound L~f by XCMPLX_1:27;
A9: r*W-bound L~f <= r*q`1 by A1,A4,AXIOMS:25;
A10: 1-r >= 0 by A2,SQUARE_1:12;
then (1-r)*W-bound L~f <= (1-r)*p`1 by A4,AXIOMS:25;
then W-bound L~f <= (1-r)*p`1+r*q`1 by A8,A9,REAL_1:55;
hence W-bound L~f <= (<*(1-r)*p+r*q*>/.n)`1 by A6,A7,FINSEQ_4:25;
A11: (1-r)*E-bound L~f+r*E-bound L~f = ((1-r)+r)*E-bound L~f by XCMPLX_1:8
.= 1*E-bound L~f by XCMPLX_1:27;
A12: r*q`1<= r*E-bound L~f by A1,A4,AXIOMS:25;
(1-r)*p`1 <= (1-r)*E-bound L~f by A4,A10,AXIOMS:25;
then (1-r)*p`1+r*q`1 <= E-bound L~f by A11,A12,REAL_1:55;
hence (<*(1-r)*p+r*q*>/.n)`1 <= E-bound L~f by A6,A7,FINSEQ_4:25;
A13: ((1-r)*p+r*q)`2 = ((1-r)*p)`2+(r*q)`2 by TOPREAL3:7
.= (1-r)*p`2+(r*q)`2 by TOPREAL3:9
.= (1-r)*p`2+r*q`2 by TOPREAL3:9;
A14: (1-r)*S-bound L~f+r*S-bound L~f = ((1-r)+r)*S-bound L~f by XCMPLX_1:8
.= 1*S-bound L~f by XCMPLX_1:27;
A15: r*S-bound L~f <= r*q`2 by A1,A4,AXIOMS:25;
(1-r)*S-bound L~f <= (1-r)*p`2 by A4,A10,AXIOMS:25;
then S-bound L~f <= (1-r)*p`2+r*q`2 by A14,A15,REAL_1:55;
hence S-bound L~f <= (<*(1-r)*p+r*q*>/.n)`2 by A6,A13,FINSEQ_4:25;
A16: (1-r)*N-bound L~f+r*N-bound L~f = ((1-r)+r)*N-bound L~f by XCMPLX_1:8
.= 1*N-bound L~f by XCMPLX_1:27;
A17: r*q`2<= r*N-bound L~f by A1,A4,AXIOMS:25;
(1-r)*p`2 <= (1-r)*N-bound L~f by A4,A10,AXIOMS:25;
then (1-r)*p`2+r*q`2 <= N-bound L~f by A16,A17,REAL_1:55;
hence (<*(1-r)*p+r*q*>/.n)`2 <= N-bound L~f by A6,A13,FINSEQ_4:25;
end;
theorem Th62:
for f, g being FinSequence of TOP-REAL 2
st g is_in_the_area_of f & i in dom g
holds <*g/.i*> is_in_the_area_of f
proof
let f, g be FinSequence of TOP-REAL 2 such that
A1: g is_in_the_area_of f and
A2: i in dom g;
let n;
assume
A3: n in dom <*g/.i*>;
dom <*g/.i*> = {1} by FINSEQ_1:4,55;
then n = 1 by A3,TARSKI:def 1;
then <*g/.i*>/.n = g/.i by FINSEQ_4:25;
hence thesis by A1,A2,SPRECT_2:def 1;
end;
theorem Th63:
for f, g being FinSequence of TOP-REAL 2,
p being Point of TOP-REAL 2
st g is_in_the_area_of f & p in L~g
holds <*p*> is_in_the_area_of f
proof
let f, g be FinSequence of TOP-REAL 2,
p be Point of TOP-REAL 2 such that
A1: g is_in_the_area_of f;
assume p in L~g;
then consider i such that
A2: 1 <= i and
A3: i+1 <= len g and
A4: p in LSeg(g/.i,g/.(i+1)) by SPPOL_2:14;
i <= i+1 by NAT_1:29;
then i <= len g by A3,AXIOMS:22;
then i in dom g by A2,FINSEQ_3:27;
then A5: <*g/.i*> is_in_the_area_of f by A1,Th62;
1 <= i+1 by NAT_1:29;
then i+1 in dom g by A3,FINSEQ_3:27;
then <*g/.(i+1)*> is_in_the_area_of f by A1,Th62;
then A6: <*g/.i,g/.(i+1)*> is_in_the_area_of f by A5,Th59;
ex r being Real st
0<=r & r<=1 & p = (1-r)*g/.i+r*g/.(i+1) by A4,SPPOL_1:21;
hence thesis by A6,Th61;
end;
theorem Th64:
for f being rectangular FinSequence of TOP-REAL 2,
p,q being Point of TOP-REAL 2
st not q in L~f & <*p,q*> is_in_the_area_of f
holds LSeg(p,q) /\ L~f c= {p}
proof
let f be rectangular FinSequence of TOP-REAL 2,
p,q be Point of TOP-REAL 2 such that
A1: not q in L~f;
assume
A2: <*p,q*> is_in_the_area_of f;
then <*q*> is_in_the_area_of f by Th59;
then A3: q`1 <> W-bound L~f & q`1 <> E-bound L~f &
q`2 <> S-bound L~f & q`2 <> N-bound L~f by A1,Th60;
A4: dom <*p,q*> = {1,2} by FINSEQ_1:4,FINSEQ_3:29;
then A5: 1 in dom <*p,q*> by TARSKI:def 2;
A6: <*p,q*>/.1 = p by FINSEQ_4:26;
then A7: W-bound L~f <= p`1 & p`1 <= E-bound L~f by A2,A5,SPRECT_2:def 1;
A8: S-bound L~f <= p`2 & p`2 <= N-bound L~f by A2,A5,A6,SPRECT_2:def 1;
A9: 2 in dom <*p,q*> by A4,TARSKI:def 2;
A10: <*p,q*>/.2 = q by FINSEQ_4:26;
then W-bound L~f <= q`1 & q`1 <= E-bound L~f by A2,A9,SPRECT_2:def 1;
then A11: W-bound L~f < q`1 & q`1 < E-bound L~f by A3,REAL_1:def 5;
S-bound L~f <= q`2 & q`2 <= N-bound L~f by A2,A9,A10,SPRECT_2:def 1;
then A12: S-bound L~f < q`2 & q`2 < N-bound L~f by A3,REAL_1:def 5;
let x be set;
assume
A13: x in LSeg(p,q) /\ L~f;
then A14: x in LSeg(p,q) by XBOOLE_0:def 3;
reconsider p' = x as Point of TOP-REAL 2 by A13;
consider r being Real such that
A15: 0<=r and
A16: r<=1 and
A17: p' = (1-r)*p+r*q by A14,SPPOL_1:21;
A18: p'`1 = ((1-r)*p)`1+(r*q)`1 by A17,TOPREAL3:7
.= (1-r)*p`1+(r*q)`1 by TOPREAL3:9
.= (1-r)*p`1+r*q`1 by TOPREAL3:9;
A19: p'`2 = ((1-r)*p)`2+(r*q)`2 by A17,TOPREAL3:7
.= (1-r)*p`2+(r*q)`2 by TOPREAL3:9
.= (1-r)*p`2+r*q`2 by TOPREAL3:9;
A20: p' in L~f by A13,XBOOLE_0:def 3;
per cases by A20,Th49;
suppose p'`1 = W-bound L~f;
then r = 0 by A7,A11,A15,A16,A18,Th4;
then p' = 1*p+0.REAL 2 by A17,EUCLID:33
.= 1*p by EUCLID:31
.= p by EUCLID:33;
hence x in {p} by ZFMISC_1:37;
suppose p'`1 = E-bound L~f;
then r = 0 by A7,A11,A15,A16,A18,Th3;
then p' = 1*p+0.REAL 2 by A17,EUCLID:33
.= 1*p by EUCLID:31
.= p by EUCLID:33;
hence x in {p} by ZFMISC_1:37;
suppose p'`2 = S-bound L~f;
then r = 0 by A8,A12,A15,A16,A19,Th4;
then p' = 1*p+0.REAL 2 by A17,EUCLID:33
.= 1*p by EUCLID:31
.= p by EUCLID:33;
hence x in {p} by ZFMISC_1:37;
suppose p'`2 = N-bound L~f;
then r = 0 by A8,A12,A15,A16,A19,Th3;
then p' = 1*p+0.REAL 2 by A17,EUCLID:33
.= 1*p by EUCLID:31
.= p by EUCLID:33;
hence x in {p} by ZFMISC_1:37;
end;
theorem
for f being rectangular FinSequence of TOP-REAL 2,
p,q being Point of TOP-REAL 2
st p in L~f & not q in L~f & <*q*> is_in_the_area_of f
holds LSeg(p,q) /\ L~f = {p}
proof
let f be rectangular FinSequence of TOP-REAL 2,
p,q be Point of TOP-REAL 2 such that
A1: p in L~f and
A2: not q in L~f and
A3: <*q*> is_in_the_area_of f;
f is_in_the_area_of f by SPRECT_2:25;
then A4: <*p*> is_in_the_area_of f by A1,Th63;
<*p,q*> = <*p*>^<*q*> by FINSEQ_1:def 9;
then <*p,q*> is_in_the_area_of f by A3,A4,SPRECT_2:28;
hence LSeg(p,q) /\ L~f c= {p} by A2,Th64;
p in LSeg(p,q) by TOPREAL1:6;
then p in LSeg(p,q) /\ L~f by A1,XBOOLE_0:def 3;
hence {p} c= LSeg(p,q) /\ L~f by ZFMISC_1:37;
end;
theorem Th66:
for f being non constant standard special_circular_sequence
st 1 <= i & i <= len GoB f & 1 <= j & j <= width GoB f
holds <*(GoB f)*(i,j)*> is_in_the_area_of f
proof
let f be non constant standard special_circular_sequence such that
A1: 1 <= i & i <= len GoB f & 1 <= j & j <= width GoB f;
set p = (GoB f)*(i,j);
let n;
assume n in dom<*(GoB f)*(i,j)*>;
then n in {1} by FINSEQ_1:4,55;
then n = 1 by TARSKI:def 1;
then A2: <*p*>/.n = p by FINSEQ_4:25;
set G = GoB f;
A3: 1 <= len G by A1,AXIOMS:22;
A4: 1 <= width G by A1,AXIOMS:22;
A5: W-bound L~f = G*(1,1)`1 by JORDAN5D:39
.= G*(1,j)`1 by A1,A3,GOBOARD5:3;
A6: i = 1 or i > 1 by A1,REAL_1:def 5;
A7: S-bound L~f = (G)*(1,1)`2 by JORDAN5D:40
.= (G)*(i,1)`2 by A1,A4,GOBOARD5:2;
A8: j = 1 or j > 1 by A1,REAL_1:def 5;
A9: E-bound L~f = (G)*(len G,1)`1 by JORDAN5D:41
.= (G)*(len G,j)`1 by A1,A3,GOBOARD5:3;
A10: i = len G or i < len G by A1,REAL_1:def 5;
A11: N-bound L~f = (G)*(1,width G)`2 by JORDAN5D:42
.= (G)*(i,width G)`2 by A1,A4,GOBOARD5:2;
j = width G or j < width G by A1,REAL_1:def 5;
hence thesis by A2,A5,A6,A7,A8,A9,A10,A11,GOBOARD5:4,5;
end;
theorem
for g being FinSequence of TOP-REAL 2,
p,q being Point of TOP-REAL 2
st <*p,q*> is_in_the_area_of g
holds <*1/2*(p+q)*> is_in_the_area_of g
proof
let g be FinSequence of TOP-REAL 2,
p,q be Point of TOP-REAL 2;
1/2*(p+q) = (1 - 1/2)*p + 1/2*q by EUCLID:36;
hence thesis by Th61;
end;
theorem
for f, g being FinSequence of TOP-REAL 2 st g is_in_the_area_of f
holds Rev g is_in_the_area_of f
proof
let f, g be FinSequence of TOP-REAL 2 such that
A1: g is_in_the_area_of f;
A2: Rev Rev g = g by FINSEQ_6:29;
A3: len Rev g = len g by FINSEQ_5:def 3;
let n such that
A4: n in dom Rev g;
set i = len g + 1 -' n;
A5: n <= len g by A3,A4,FINSEQ_3:27;
len g <= len g + 1 by NAT_1:29;
then n <= len g + 1 by A5,AXIOMS:22;
then n + i = len g + 1 by AMI_5:4;
then A6: (Rev g)/.n = g/.i by A2,A3,A4,FINSEQ_5:69;
A7: i = len g -' n + 1 by A5,JORDAN4:3;
then A8: 1 <= i by NAT_1:29;
A9: i = len g - n + 1 by A5,A7,SCMFSA_7:3
.= len g - (n-1) by XCMPLX_1:37;
n >= 1 by A4,FINSEQ_3:27;
then n-1 >= 0 by SQUARE_1:12;
then i <= len g - 0 by A9,REAL_1:92;
then i in dom g by A8,FINSEQ_3:27;
hence W-bound L~f <= ((Rev g)/.n)`1 & ((Rev g)/.n)`1 <= E-bound L~f &
S-bound L~f <= ((Rev g)/.n)`2 & ((Rev g)/.n)`2 <= N-bound L~f
by A1,A6,SPRECT_2:def 1;
end;
theorem
for f, g being FinSequence of TOP-REAL 2,
p being Point of TOP-REAL 2
st g is_in_the_area_of f & <*p*> is_in_the_area_of f &
g is_S-Seq & p in L~g
holds R_Cut(g,p) is_in_the_area_of f
proof
let f, g be FinSequence of TOP-REAL 2,
p be Point of TOP-REAL 2 such that
A1: g is_in_the_area_of f and
A2: <*p*> is_in_the_area_of f and
A3: g is_S-Seq;
2 <= len g by A3,TOPREAL1:def 10;
then A4: 1 <= len g by AXIOMS:22;
then A5: 1 in dom g by FINSEQ_3:27;
assume p in L~g;
then 1<=Index(p,g) & Index(p,g) < len g by JORDAN3:41;
then A6: Index(p,g) in dom g by FINSEQ_3:27;
per cases;
suppose p<>g.1;
then A7: R_Cut(g,p) = mid(g,1,Index(p,g))^<*p*> by JORDAN3:def 5;
mid(g,1,Index(p,g)) is_in_the_area_of f by A1,A5,A6,SPRECT_2:26;
hence R_Cut(g,p) is_in_the_area_of f by A2,A7,SPRECT_2:28;
suppose p=g.1;
then R_Cut(g,p) = <*g.1*> by JORDAN3:def 5
.= <*g/.1*> by A5,FINSEQ_4:def 4
.= mid(g,1,1) by A4,JORDAN4:27;
hence R_Cut(g,p) is_in_the_area_of f by A1,A5,SPRECT_2:26;
end;
theorem
for f being non constant standard special_circular_sequence,
g being FinSequence of TOP-REAL2
holds g is_in_the_area_of f iff g is_in_the_area_of SpStSeq L~f
proof
let f be non constant standard special_circular_sequence,
g be FinSequence of TOP-REAL2;
A1: W-bound L~SpStSeq L~f = W-bound L~f &
S-bound L~SpStSeq L~f = S-bound L~f &
N-bound L~SpStSeq L~f = N-bound L~f &
E-bound L~SpStSeq L~f = E-bound L~f by SPRECT_1:66,67,68,69;
thus g is_in_the_area_of f implies g is_in_the_area_of SpStSeq L~f
proof assume
A2: g is_in_the_area_of f;
let n; thus thesis by A1,A2,SPRECT_2:def 1;
end;
assume
A3: g is_in_the_area_of SpStSeq L~f;
let n; thus thesis by A1,A3,SPRECT_2:def 1;
end;
theorem
for f being rectangular special_circular_sequence,
g being S-Sequence_in_R2
st g/.1 in LeftComp f & g/.len g in RightComp f
holds L_Cut(g,Last_Point(L~g,g/.1,g/.len g,L~f)) is_in_the_area_of f
proof
let f be rectangular special_circular_sequence,
g be S-Sequence_in_R2 such that
A1: g/.1 in LeftComp f and
A2: g/.len g in RightComp f;
set lp = Last_Point(L~g,g/.1,g/.len g,L~f),
ilp = Index(lp,g),
h = L_Cut(g,lp);
A3: L~f misses LeftComp f by Th43;
A4: L~g meets L~f by A1,A2,Th50;
A5: L~g is closed & L~f is closed by SPPOL_1:49;
then A6: L~g /\ L~f is closed by TOPS_1:35;
L~g is_an_arc_of g/.1,g/.len g by TOPREAL1:31;
then A7: lp in L~g /\ L~f by A4,A6,JORDAN5C:def 2;
then A8: lp in L~f by XBOOLE_0:def 3;
A9: lp in L~g by A7,XBOOLE_0:def 3;
A10: len g in dom g by FINSEQ_5:6;
1 in dom g by FINSEQ_5:6;
then A11: len g >= 1 by FINSEQ_3:27;
A12: lp in LSeg(g,ilp) by A9,JORDAN3:42;
given n such that
A13: n in dom h and
A14: W-bound L~f > (h/.n)`1 or (h/.n)`1 > E-bound L~f or
S-bound L~f > (h/.n)`2 or (h/.n)`2 > N-bound L~f;
LeftComp f = {p : not(W-bound L~f <= p`1 & p`1 <= E-bound L~f
& S-bound L~f <= p`2 & p`2 <= N-bound L~f)} by Th54;
then A15: h/.n in LeftComp f by A14;
A16: 1 <= n & n <= len h by A13,FINSEQ_3:27;
then A17: n = n -'1 +1 by AMI_5:4;
A18: len<*lp*> = 1 by FINSEQ_1:56;
A19: ilp < len g by A9,JORDAN3:41;
then A20: ilp+1<=len g by NAT_1:38;
A21: 1<=ilp+1 by NAT_1:29;
then A22: len mid(g,ilp+1,len g)=len g-'(ilp+1)+1 by A20,JORDAN4:20
.= len g -' ilp by A19,NAT_2:9;
then A23: ilp + len mid(g,ilp+1,len g) + 1 = len g + 1 by A19,AMI_5:4;
A24: ilp+1 in dom g by A20,A21,FINSEQ_3:27;
A25: n+ilp <= len h + ilp by A16,AXIOMS:24;
A26: LeftComp f misses RightComp f by SPRECT_1:96;
A27: 1 <= ilp by A9,JORDAN3:41;
now
assume
A28: n = 1;
per cases;
suppose lp <> g.(ilp+1);
then h = <*lp*>^mid(g,ilp+1,len g) by JORDAN3:def 4;
then h/.n = lp by A28,FINSEQ_5:16;
hence contradiction by A3,A8,A15,XBOOLE_0:3;
suppose
A29: lp = g.(ilp+1);
then h = mid(g,ilp+1,len g) by JORDAN3:def 4;
then h/.n = g/.(1+(ilp+1)-'1) by A10,A13,A20,A24,A28,SPRECT_2:7
.= g/.(ilp+1) by BINARITH:39
.= lp by A24,A29,FINSEQ_4:def 4;
hence contradiction by A3,A8,A15,XBOOLE_0:3;
end;
then A30: n > 1 by A16,AXIOMS:21;
then A31: 1+1 < ilp+n by A27,REAL_1:67;
then A32: 1 <= ilp+n-'1 by JORDAN3:12;
A33: ilp+n-'1 = ilp+(n-'1) by A16,JORDAN4:3;
A34: 1 <= n-'1 by A17,A30,NAT_1:38;
now assume
A35: lp <> g.(ilp+1);
then A36: h = <*lp*>^mid(g,ilp+1,len g) by JORDAN3:def 4;
then A37: len h = 1 + len mid(g,ilp+1,len g) by A18,FINSEQ_1:35;
then len h -' 1 = len mid(g,ilp+1,len g) by BINARITH:39;
then A38: n-'1 <= len mid(g,ilp+1,len g) by A16,JORDAN3:5;
then A39: h/.n = (mid(g,ilp+1,len g))/.(n-'1) by A17,A18,A34,A36,GOBOARD2:5;
A40: ilp + len h = len g + 1 by A23,A37,XCMPLX_1:1;
n-'1 in dom mid(g,ilp+1,len g) by A34,A38,FINSEQ_3:27;
then A41: h/.n = g/.(n-'1+(ilp+1)-'1) by A10,A20,A24,A39,SPRECT_2:7
.= g/.(n+ilp-'1) by A17,XCMPLX_1:1;
A42: ilp+n-'1 <= len g by A25,A40,Th6;
A43: ilp+n-'1<>len g by A2,A15,A26,A41,XBOOLE_0:3;
then reconsider m = mid(g,ilp+n-'1,len g) as S-Sequence_in_R2
by A11,A32,A42,JORDAN3:39;
A44: ilp+n-'1 in dom g by A32,A42,FINSEQ_3:27;
then A45: m/.1 in LeftComp f by A10,A15,A41,SPRECT_2:12;
m/.len m in RightComp f by A2,A10,A44,SPRECT_2:13;
then L~f meets L~m by A45,Th50;
then consider q being set such that
A46: q in L~f and
A47: q in L~m by XBOOLE_0:3;
reconsider q as Point of TOP-REAL 2 by A47;
consider i such that
A48: 1 <= i & i+1 <= len m and
A49: q in LSeg(m,i) by A47,SPPOL_2:13;
A50: len m = len g-'(ilp+n-'1)+1 by A32,A42,JORDAN4:20;
A51: i < len m by A48,NAT_1:38;
ilp+n-'1<len g by A42,A43,AXIOMS:21;
then A52: LSeg(m,i)=LSeg(g,i+(ilp+n-'1)-'1) by A32,A48,A50,A51,JORDAN4:31;
set j = i+(ilp+n-'1)-'1;
j = i-'1+(ilp+n-'1) by A48,JORDAN4:3;
then A53: j >= ilp+n-'1 by NAT_1:29;
ilp+1 <= ilp+n-'1 by A33,A34,AXIOMS:24;
then A54: ilp +1 <= j by A53,AXIOMS:22;
A55: lp <> g/.(ilp+1) by A24,A35,FINSEQ_4:def 4;
A56: 1 <= j by A21,A54,AXIOMS:22;
i <= len g-'(ilp+n-'1) by A48,A50,REAL_1:53;
then A57: i+(ilp+n-'1) <= len g by A42,Th7;
i <= i+(ilp+n-'1) by NAT_1:29;
then 1 <= i+(ilp+n-'1) by A48,AXIOMS:22;
then A58: j + 1 <= len g by A57,AMI_5:4;
now assume lp = q;
then A59: lp in LSeg(g,ilp) /\ LSeg(g,j) by A12,A49,A52,XBOOLE_0:def 3;
then A60: LSeg(g,ilp) meets LSeg(g,j) by XBOOLE_0:4;
per cases by A54,AXIOMS:21;
suppose
A61: ilp+1 = j;
then ilp + (1+1) <= len g by A58,XCMPLX_1:1;
then LSeg(g,ilp) /\ LSeg(g,ilp+1) = {g/.(ilp+1)} by A27,TOPREAL1:def 8;
hence contradiction by A55,A59,A61,TARSKI:def 1;
suppose ilp+1 < j;
hence contradiction by A60,TOPREAL1:def 9;
end;
then ilp >= j by A4,A5,A12,A20,A27,A46,A49,A52,A56,A58,JORDAN5C:28;
then ilp >= ilp+1 by A54,AXIOMS:22;
hence contradiction by REAL_1:69;
end;
then A62: h = mid(g,ilp+1,len g) by JORDAN3:def 4;
then A63: ilp + len h = len g by A19,A22,AMI_5:4;
A64: 1 <= ilp+n by A31,AXIOMS:22;
then ilp+n -' 1 + 1 = ilp+n by AMI_5:4;
then A65: ilp+n-'1 < len g by A25,A63,NAT_1:38;
set m = mid(g,ilp+n,len g);
m = g/^(ilp+n-'1) by A25,A63,JORDAN3:26;
then A66: m/.len m in RightComp f by A2,A65,JORDAN4:18;
A67: h/.n = g/.(n+(ilp+1)-'1) by A10,A13,A20,A24,A62,SPRECT_2:7
.= g/.(n+ilp+1-'1) by XCMPLX_1:1
.= g/.(ilp+n) by BINARITH:39;
then A68: ilp+n <> len g by A2,A15,A26,XBOOLE_0:3;
then reconsider m as S-Sequence_in_R2 by A11,A25,A63,A64,JORDAN3:39;
ilp+n in dom g by A25,A63,A64,FINSEQ_3:27;
then m/.1 in LeftComp f by A10,A15,A67,SPRECT_2:12;
then L~f meets L~m by A66,Th50;
then consider q being set such that
A69: q in L~f and
A70: q in L~m by XBOOLE_0:3;
reconsider q as Point of TOP-REAL 2 by A70;
consider i such that
A71: 1 <= i & i+1 <= len m and
A72: q in LSeg(m,i) by A70,SPPOL_2:13;
A73: ilp+n < len g by A25,A63,A68,AXIOMS:21;
len m = len g -' (ilp+n) + 1 by A11,A25,A63,A64,JORDAN3:27;
then A74: i < len g -'(ilp+n) +1 by A71,NAT_1:38;
then A75: LSeg(m,i) = LSeg(g,i+(ilp+n)-'1) by A64,A71,A73,JORDAN4:31;
set j = i+(ilp+n)-'1;
A76: j = i-'1+(ilp+n) by A71,JORDAN4:3;
then A77: j >= ilp+n by NAT_1:29;
ilp+1 < ilp+n by A30,REAL_1:53;
then A78: j > ilp+1 by A77,AXIOMS:22;
A79: now assume lp = q;
then lp in LSeg(g,ilp) /\ LSeg(g,j) by A12,A72,A75,XBOOLE_0:def 3;
then LSeg(g,ilp) meets LSeg(g,j) by XBOOLE_0:4;
hence contradiction by A78,TOPREAL1:def 9;
end;
i-'1 < len g-'(ilp+n) by A71,A74,Th7;
then i-'1+(ilp+n) < len g by Th6;
then A80: j + 1 <= len g by A76,NAT_1:38;
1 <= j by A64,A77,AXIOMS:22;
then ilp >= j by A4,A5,A12,A20,A27,A69,A72,A75,A79,A80,JORDAN5C:28;
then ilp >= ilp+1 by A78,AXIOMS:22;
hence contradiction by REAL_1:69;
end;
theorem
for f being non constant standard special_circular_sequence
st 1 <= i & i < len GoB f & 1 <= j & j < width GoB f
holds Int cell(GoB f,i,j) misses L~SpStSeq L~f
proof
let f be non constant standard special_circular_sequence
such that
A1: 1 <= i & i < len GoB f and
A2: 1 <= j & j < width GoB f;
set G = GoB f;
A3: Int cell(G,i,j) = { |[r,s]| where r,s is Real:
G*(i,1)`1 < r & r < G*(i+1,1)`1 &
G*(1,j)`2 < s & s < G*(1,j+1)`2 } by A1,A2,GOBOARD6:29;
assume Int cell(GoB f,i,j) meets L~SpStSeq L~f;
then consider x being set such that
A4: x in Int cell(GoB f,i,j) and
A5: x in L~SpStSeq L~f by XBOOLE_0:3;
consider r,s being Real such that
A6: x = |[r,s]| and
A7: G*(i,1)`1 < r & r < G*(i+1,1)`1 and
A8: G*(1,j)`2 < s & s < G*(1,j+1)`2 by A3,A4;
A9: 1 <= width GoB f by GOBRD11:34;
then A10: <*(GoB f)*(i,1)*> is_in_the_area_of f by A1,Th66;
A11: 1 <= len GoB f by GOBRD11:34;
then A12: <*(GoB f)*(1,j)*> is_in_the_area_of f by A2,Th66;
1 <= i+1 & i+1 <= len GoB f by A1,NAT_1:38;
then A13: <*(GoB f)*(i+1,1)*> is_in_the_area_of f by A9,Th66;
1 <= j+1 & j+1 <= width GoB f by A2,NAT_1:38;
then A14: <*(GoB f)*(1,j+1)*> is_in_the_area_of f by A11,Th66;
L~SpStSeq L~f = { p:
p`1 = W-bound L~SpStSeq L~f &
p`2 <= N-bound L~SpStSeq L~f & p`2 >= S-bound L~SpStSeq L~f or
p`1 <= E-bound L~SpStSeq L~f & p`1 >= W-bound L~SpStSeq L~f &
p`2 = N-bound L~SpStSeq L~f or
p`1 <= E-bound L~SpStSeq L~f & p`1 >= W-bound L~SpStSeq L~f &
p`2 = S-bound L~SpStSeq L~f or
p`1 = E-bound L~SpStSeq L~f &
p`2 <= N-bound L~SpStSeq L~f & p`2 >= S-bound L~SpStSeq L~f}
by Th52;
then consider p such that
A15: p = x and
A16: p`1 = W-bound L~SpStSeq L~f &
p`2 <= N-bound L~SpStSeq L~f & p`2 >= S-bound L~SpStSeq L~f or
p`1 <= E-bound L~SpStSeq L~f & p`1 >= W-bound L~SpStSeq L~f &
p`2 = N-bound L~SpStSeq L~f or
p`1 <= E-bound L~SpStSeq L~f & p`1 >= W-bound L~SpStSeq L~f &
p`2 = S-bound L~SpStSeq L~f or
p`1 = E-bound L~SpStSeq L~f &
p`2 <= N-bound L~SpStSeq L~f & p`2 >= S-bound L~SpStSeq L~f by A5;
A17: p`1 = r by A6,A15,EUCLID:56;
A18: p`2 = s by A6,A15,EUCLID:56;
A19: W-bound L~SpStSeq L~f = W-bound L~f &
S-bound L~SpStSeq L~f = S-bound L~f &
N-bound L~SpStSeq L~f = N-bound L~f &
E-bound L~SpStSeq L~f = E-bound L~f by SPRECT_1:66,67,68,69;
per cases by A16;
suppose
A20: p`1 = W-bound L~SpStSeq L~f;
A21: <*G*(i,1)*>/.1 = G*(i,1) by FINSEQ_4:25;
1 in dom<*G*(i,1)*> by FINSEQ_5:6;
hence contradiction by A7,A10,A17,A19,A20,A21,SPRECT_2:def 1;
suppose
A22: p`2 = N-bound L~SpStSeq L~f;
A23: <*G*(1,j+1)*>/.1 = G*(1,j+1) by FINSEQ_4:25;
1 in dom<*G*(1,j+1)*> by FINSEQ_5:6;
hence contradiction by A8,A14,A18,A19,A22,A23,SPRECT_2:def 1;
suppose that
A24: p`2 = S-bound L~SpStSeq L~f;
A25: <*G*(1,j)*>/.1 = G*(1,j) by FINSEQ_4:25;
1 in dom<*G*(1,j)*> by FINSEQ_5:6;
hence contradiction by A8,A12,A18,A19,A24,A25,SPRECT_2:def 1;
suppose that
A26: p`1 = E-bound L~SpStSeq L~f;
A27: <*G*(i+1,1)*>/.1 = G*(i+1,1) by FINSEQ_4:25;
1 in dom<*G*(i+1,1)*> by FINSEQ_5:6;
hence contradiction by A7,A13,A17,A19,A26,A27,SPRECT_2:def 1;
end;
theorem
for f, g being FinSequence of TOP-REAL 2,
p being Point of TOP-REAL 2
st g is_in_the_area_of f & <*p*> is_in_the_area_of f &
g is_S-Seq & p in L~g
holds L_Cut(g,p) is_in_the_area_of f
proof
let f, g be FinSequence of TOP-REAL 2,
p be Point of TOP-REAL 2 such that
A1: g is_in_the_area_of f and
A2: <*p*> is_in_the_area_of f and
A3: g is_S-Seq;
2 <= len g by A3,TOPREAL1:def 10;
then 1 <= len g by AXIOMS:22;
then A4: len g in dom g by FINSEQ_3:27;
assume p in L~g;
then Index(p,g) < len g by JORDAN3:41;
then A5: Index(p,g)+1 <= len g by NAT_1:38;
1<=Index(p,g)+1 by NAT_1:29;
then A6: Index(p,g)+1 in dom g by A5,FINSEQ_3:27;
per cases;
suppose p<>g.(Index(p,g)+1);
then A7: L_Cut(g,p) = <*p*>^mid(g,Index(p,g)+1,len g) by JORDAN3:def 4;
mid(g,Index(p,g)+1,len g) is_in_the_area_of f by A1,A4,A6,SPRECT_2:26;
hence L_Cut(g,p) is_in_the_area_of f by A2,A7,SPRECT_2:28;
suppose p=g.(Index(p,g)+1);
then L_Cut(g,p) = mid(g,Index(p,g)+1,len g) by JORDAN3:def 4;
hence L_Cut(g,p) is_in_the_area_of f by A1,A4,A6,SPRECT_2:26;
end;