:: Some properties of special polygonal curves
:: by Andrzej Trybulec and Yatsuka Nakamura
::
:: Received October 22, 1998
:: Copyright (c) 1998-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies NUMBERS, NAT_1, XBOOLE_0, FINSEQ_1, ORDINAL4, PARTFUN1, XXREAL_0,
ARYTM_3, MATRIX_1, ZFMISC_1, SUBSET_1, PRE_TOPC, EUCLID, REAL_1, CARD_1,
ARYTM_1, RELAT_1, SUPINF_2, RLTOPSP1, METRIC_1, RELAT_2, CONVEX1,
RCOMP_1, CONNSP_1, TARSKI, PCOMPS_1, SPPOL_1, MCART_1, GOBOARD1, TREES_1,
PSCOMP_1, TOPREAL1, SPRECT_1, SPPOL_2, JORDAN3, FUNCT_1, RFINSEQ,
GROUP_2, GOBOARD5, GOBOARD9, TOPREAL4, JORDAN5D, GOBOARD2, SPRECT_2,
COMPLEX1, ORDINAL2, TOPS_1, JORDAN5C, FINSEQ_5;
notations TARSKI, XBOOLE_0, ENUMSET1, ZFMISC_1, SUBSET_1, ORDINAL1, NUMBERS,
XCMPLX_0, XREAL_0, COMPLEX1, REAL_1, NAT_1, NAT_D, CARD_1, RFINSEQ,
FUNCT_1, PARTFUN1, FINSEQ_1, FINSEQ_4, FINSEQ_5, MATRIX_0, MATRIX_1,
SEQM_3, SEQ_4, FINSEQ_6, STRUCT_0, METRIC_1, PRE_TOPC, TOPS_1, COMPTS_1,
CONNSP_1, PCOMPS_1, RLVECT_1, RLTOPSP1, EUCLID, TOPREAL1, TOPREAL4,
PSCOMP_1, GOBOARD1, GOBOARD2, SPPOL_1, SPPOL_2, GOBOARD5, GOBOARD9,
JORDAN3, JORDAN5C, JORDAN5D, SPRECT_1, SPRECT_2, XXREAL_0;
constructors REAL_1, FINSEQ_4, RFINSEQ, NAT_D, TOPS_1, CONNSP_1, TOPS_2,
COMPTS_1, MATRIX_1, TOPMETR, TOPREAL2, TOPREAL4, GOBOARD2, SPPOL_1,
PSCOMP_1, GOBOARD9, JORDAN3, JORDAN5C, SPRECT_1, SPRECT_2, JORDAN5D,
GOBOARD1, PCOMPS_1, BINARITH, FUNCSDOM, CONVEX1, SEQ_4, RVSUM_1,
VALUED_0;
registrations RELSET_1, XREAL_0, FINSEQ_1, STRUCT_0, EUCLID, GOBOARD2,
SPPOL_2, SPRECT_1, SPRECT_2, VALUED_0, CARD_1, FUNCT_1, SEQ_4, SPPOL_1,
TOPS_1, JORDAN1, RVSUM_1, NAT_1, ORDINAL1;
requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM;
definitions TARSKI, SPRECT_2, TOPREAL4, XBOOLE_0, SEQM_3;
equalities RLTOPSP1, XBOOLE_0, PSCOMP_1;
expansions TARSKI, SPRECT_2, JORDAN1, XBOOLE_0;
theorems FINSEQ_4, TARSKI, FINSEQ_3, FINSEQ_1, SPRECT_2, GOBOARD7, PSCOMP_1,
SPRECT_1, TOPREAL3, SPPOL_2, NAT_1, SPPOL_1, EUCLID, ZFMISC_1, TOPREAL1,
GOBOARD5, JORDAN5D, FINSEQ_5, FINSEQ_6, JORDAN4, JORDAN3, TOPREAL5,
GOBRD11, GOBOARD9, TOPMETR, GOBOARD6, JORDAN1, CONNSP_1, SUBSET_1,
GOBRD12, JORDAN5C, JORDAN6, GOBOARD1, ENUMSET1, CARD_2, GOBOARD2, NAT_2,
ABSVALUE, GOBOARD8, PARTFUN2, FUNCT_1, XBOOLE_0, XBOOLE_1, FINSEQ_2,
XREAL_1, XXREAL_0, PARTFUN1, MATRIX_0, NAT_D, PRE_TOPC, RLTOPSP1, SEQM_3,
SEQ_4, XTUPLE_0, RVSUM_1, RLVECT_1;
schemes DOMAIN_1;
begin :: Preliminaries
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 f >= 1 by NAT_1:14;
len(g^f) = len g + len f by FINSEQ_1:22;
hence thesis by A1,SEQ_4:136;
end;
theorem Th2:
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_0:47
.= [:{1},Seg 2:] \/ [:{2},Seg 2:] by FINSEQ_1:2,ZFMISC_1:109
.= [:{1},Seg 2:] \/ {[2,1], [2,2]} by FINSEQ_1:2,ZFMISC_1:30
.= { [1,1], [1,2]} \/ {[2,1], [2,2]} by FINSEQ_1:2,ZFMISC_1:30
.= {[1,1],[1,2],[2,1],[2,2]} by ENUMSET1:5;
end;
begin :: Euclidean Space
reserve i,j,k,n,m for Nat;
theorem Th3:
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 RLVECT_1:def 6
.= p by RLVECT_1:def 8;
r*p = r*p + 0.TOP-REAL n by RLVECT_1:4
.= r*p + ((1-r)*p + -(1-r)*p) by RLVECT_1:5
.= r*q + (1-r)*p + -(1-r)*p by A2,A3,RLVECT_1:def 3
.= r*q + ((1-r)*p + -(1-r)*p) by RLVECT_1:def 3
.= r*q + 0.TOP-REAL n by RLVECT_1:5
.= r*q by RLVECT_1:4;
hence thesis by A1,RLVECT_1:36;
end;
theorem Th4:
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 XREAL_1:20;
p = (1-s)*p+s*q by A2;
hence thesis by A3,Th3;
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 RLVECT_1:def 5;
hence thesis by Th3;
end;
theorem Th6:
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: q = (1-r1)*p+r1*r and
A2: 0<=r1 and
A3: r1<=1;
assume r in LSeg(p,q);
then consider r2 being Real such that
A4: r = (1-r2)*p+r2*q and
0<=r2 and
A5: r2<=1;
A6: r1*r2 <= 1 by A2,A3,A5,XREAL_1:160;
A7: (1-r2)+r2*(1-r1) = 1 - r2*r1;
A8: r = (1-r2)*p+(r2*((1-r1)*p)+r2*(r1*r)) by A1,A4,RLVECT_1:def 5
.= (1-r2)*p+r2*((1-r1)*p)+r2*(r1*r) by RLVECT_1:def 3
.= (1-r2)*p+r2*(1-r1)*p+r2*(r1*r) by RLVECT_1:def 7
.= (1 - r2*r1)*p+r2*(r1*r) by A7,RLVECT_1:def 6
.= (1 - r2*r1)*p+r2*r1*r by RLVECT_1:def 7;
A9: (1-r1)+r1*(1-r2) = 1 - r1*r2;
A10: q = (1-r1)*p+(r1*((1-r2)*p)+r1*(r2*q)) by A1,A4,RLVECT_1:def 5
.= (1-r1)*p+r1*((1-r2)*p)+r1*(r2*q) by RLVECT_1:def 3
.= (1-r1)*p+r1*(1-r2)*p+r1*(r2*q) by RLVECT_1:def 7
.= (1 - r1*r2)*p+r1*(r2*q) by A9,RLVECT_1:def 6
.= (1 - r1*r2)*p+r1*r2*q by RLVECT_1:def 7;
per cases by A6,XXREAL_0:1;
suppose
A11: r1*r2 = 1;
then 1 <= r1 or 1 <= r2 by A2,XREAL_1:162;
then 1*r1 = 1 or 1*r2 = 1 by A3,A5,XXREAL_0:1;
hence q = 0 * p+r by A1,A11,RLVECT_1:def 8
.= 0.TOP-REAL n+r by RLVECT_1:10
.= r by RLVECT_1:4;
end;
suppose
A12: r1*r2 < 1;
hence q = p by A10,Th4
.= r by A8,A12,Th4;
end;
end;
begin :: Euclidean Plane
theorem Th7:
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
by A1,TOPREAL3:21;
hence thesis;
end;
theorem Th8:
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:5;
A4: the TopStruct of TOP-REAL 2 = TopSpaceMetr Euclid 2 by EUCLID:def 8;
then reconsider C = B, D = A as Subset of TopSpaceMetr Euclid 2;
A5: D is open by A1,A4,PRE_TOPC:30;
for p being Point of Euclid 2 st p in C ex r being Real st r>0 &
Ball(p,r) c= C
proof
let p be Point of Euclid 2;
assume
A6: p in C;
then consider r being Real such that
A7: r > 0 and
A8: Ball(p,r) c= D by A3,A5,TOPMETR:15;
reconsider r as Real;
take r;
thus r>0 by A7;
reconsider E = Ball(p,r) as Subset of TOP-REAL 2 by A4,TOPMETR:12;
A9: p in E by A7,GOBOARD6:1;
then
A10: E is connected by Th7;
B meets E by A6,A9,XBOOLE_0:3;
hence thesis by A2,A8,A10,GOBOARD9:4;
end;
then C is open by TOPMETR:15;
hence B is open by A4,PRE_TOPC:30;
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) <> {};
then consider x being Point of TOP-REAL 2 such that
A3: x in LSeg(p,q) /\ LSeg(r,s) by SUBSET_1:4;
A4: x in LSeg(r,s) by A3,XBOOLE_0:def 4;
x in LSeg(p,q) by A3,XBOOLE_0:def 4;
hence p`2 = x`2 by A1,SPPOL_1:40
.= r`2 by A2,A4,SPPOL_1:40;
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 object holds x in LSeg(p,q) /\ LSeg(q,r) iff x = q
proof
let x be object;
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(q,r) by A3,XBOOLE_0:def 4;
then
A4: x`2 = q`2 by A2,SPPOL_1:40;
x in LSeg(p,q) by A3,XBOOLE_0:def 4;
then x`1 = q`1 by A1,SPPOL_1:41;
hence thesis by A4,TOPREAL3:6;
end;
assume
A5: x = q;
then
A6: x in LSeg(q,r) by RLTOPSP1:68;
x in LSeg(p,q) by A5,RLTOPSP1:68;
hence thesis by A6,XBOOLE_0:def 4;
end;
hence thesis 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 object holds x in LSeg(p,q) /\ LSeg(s,r) iff x = r
proof
let x be object;
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;
x in LSeg(p,q) by A4,XBOOLE_0:def 4;
then
A5: x`2 = p`2 by A1,SPPOL_1:40;
x in LSeg(s,r) by A4,XBOOLE_0:def 4;
then
A6: x`1 = r`1 by A2,SPPOL_1:41;
p`2 = r`2 by A1,A3,SPPOL_1:40;
hence thesis by A5,A6,TOPREAL3:6;
end;
assume
A7: x = r;
then x in LSeg(s,r) by RLTOPSP1:68;
hence thesis by A3,A7,XBOOLE_0:def 4;
end;
hence thesis 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 that
A1: 1 <= j and
A2: j <= k and
A3: k <= width G and
A4: 1 <= i and
A5: i <= len G;
per cases by A2,XXREAL_0:1;
suppose
j < k;
hence thesis by A1,A3,A4,A5,GOBOARD5:4;
end;
suppose
j = k;
hence thesis;
end;
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 that
A1: 1 <= j and
A2: j <= width G and
A3: 1 <= i and
A4: i <= k and
A5: k <= len G;
per cases by A4,XXREAL_0:1;
suppose
i < k;
hence thesis by A1,A2,A3,A5,GOBOARD5:3;
end;
suppose
i = k;
hence thesis;
end;
end;
reserve C for Subset of TOP-REAL 2;
theorem Th14:
LSeg(NW-corner C,NE-corner C) c= L~SpStSeq C
proof
A1: 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;
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;
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;
hence thesis by SPRECT_1:41;
end;
theorem Th15:
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-most C c= LSeg(NW-corner C,NE-corner C) by XBOOLE_1:17;
N-min C in N-most C by PSCOMP_1:42;
hence thesis by A1;
end;
registration
let C;
cluster LSeg(NW-corner C,NE-corner C) -> horizontal;
coherence
proof
(NW-corner C)`2 = N-bound C by EUCLID:52
.= (NE-corner C)`2 by EUCLID:52;
hence thesis by SPPOL_1:15;
end;
end;
theorem
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 being_S-Seq & LSeg(p,g/.1
) /\ L~g={ g/.1 } holds <*p*>^g is being_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 being_S-Seq and
A4: LSeg(p,g/.1) /\ L~g={ g/.1 };
set f = <*p,g/.1*>;
A5: f is being_S-Seq by A1,A2,SPPOL_2:43;
reconsider g9 = g as S-Sequence_in_R2 by A3;
A6: 1 in dom g9 by FINSEQ_5:6;
A7: len f = 1+1 by FINSEQ_1:44;
then AB: len f -' 1 = 1 by NAT_D:34;
AA: 1 in dom f by FINSEQ_3:25,A7;
then
A8: mid(f,1,len f-'1) = <*f.1*> by AB,FINSEQ_6:193
.= <*f/.1*> by AA,PARTFUN1:def 6
.= <*p*> by FINSEQ_4:17;
A9: L~f /\ L~g ={ g/.1 } by A4,SPPOL_2:21
.={g.1} by A6,PARTFUN1:def 6;
f.len f = g/.1 by A7
.= g.1 by A6,PARTFUN1:def 6;
hence thesis by A3,A5,A9,A8,JORDAN3:45;
end;
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 and
A2: j <= len f and
A3: p in L~mid(f,1,j);
consider i such that
A4: 1 <= i and
A5: i+1 <= len mid(f,1,j) and
A6: p in LSeg(mid(f,1,j),i) by A3,SPPOL_2:13;
A7: j -' 1 + 1 = j by A1,XREAL_1:235;
then
A8: i+1 <= j by A1,A2,A5,FINSEQ_6:186;
then i < j-'1+1 by A7,NAT_1:13;
then
A9: LSeg(mid(f,1,j),i) = LSeg(f,i+1-'1) by A1,A2,A4,JORDAN4:19;
1 <= i+1 by NAT_1:11;
then
A10: LE f/.(i+1), f/.j, L~f, f/.1, f/.len f by A2,A8,JORDAN5C:24;
A11: i = i + 1 -' 1 by NAT_D:34;
i+1 <= len f by A2,A8,XXREAL_0:2;
then LE p, f/.(i+1), L~f, f/.1, f/.len f by A4,A6,A11,A9,JORDAN5C:26;
hence thesis by 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 that
A1: i in dom h and
A2: j in dom h;
A3: i <= len h by A1,FINSEQ_3:25;
A4: j <= len h by A2,FINSEQ_3:25;
A5: 1 <= j by A2,FINSEQ_3:25;
1 <= i by A1,FINSEQ_3:25;
hence thesis by A3,A5,A4,JORDAN4:35;
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;
set A = { LSeg(f,k): i <= k & k < j}, B = { LSeg(f,k): i+1 <= k & k < j};
A4: A = B \/ {LSeg(f,i)}
proof
thus A c= B \/ {LSeg(f,i)}
proof
let e be object;
assume e in A;
then consider k such that
A5: e = LSeg(f,k) and
A6: i <= k and
A7: k < j;
i = k or i < k by A6,XXREAL_0:1;
then i = k or i+1 <= k by NAT_1:13;
then e in B or e in {LSeg(f,i)} by A5,A7,TARSKI:def 1;
hence thesis by XBOOLE_0:def 3;
end;
let e be object;
assume
A8: e in B \/ {LSeg(f,i)};
per cases by A8,XBOOLE_0:def 3;
suppose
e in B;
then consider k such that
A9: e = LSeg(f,k) and
A10: i+1 <= k and
A11: k < j;
i < k by A10,NAT_1:13;
hence thesis by A9,A11;
end;
suppose
e in {LSeg(f,i)};
then e = LSeg(f,i) by TARSKI:def 1;
hence thesis by A2;
end;
end;
A12: 1 <= i+1 by NAT_1:11;
A13: i+1 <= j by A2,NAT_1:13;
thus L~mid(f,i,j) = union A by A1,A2,A3,SPRECT_2:14
.= union B \/ union{LSeg(f,i)} by A4,ZFMISC_1:78
.= union B \/ LSeg(f,i) by ZFMISC_1:25
.= LSeg(f,i) \/ L~mid(f,i+1,j) by A3,A12,A13,SPRECT_2:14;
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;
j -' 1 <= j by NAT_D:35;
then
A4: j -' 1 <= len f by A3,XXREAL_0:2;
set A = { LSeg(f,k): i <= k & k < j}, B = { LSeg(f,k): i <= k & k < j -' 1};
A5: i <= j -' 1 by A2,NAT_D:49;
A6: A = B \/ {LSeg(f,j -' 1)}
proof
thus A c= B \/ {LSeg(f,j -' 1)}
proof
let e be object;
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,NAT_D:49;
then j -' 1 = k or k < j -' 1 by XXREAL_0:1;
then e in B or e in {LSeg(f,j -' 1)} by A7,A8,TARSKI:def 1;
hence thesis by XBOOLE_0:def 3;
end;
let e be object;
A10: j -' 1 <= j by NAT_D:35;
assume
A11: e in B \/ {LSeg(f,j -' 1)};
per cases by A11,XBOOLE_0:def 3;
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 A10,A14,XXREAL_0:2;
hence thesis by A12,A13;
end;
suppose
A15: e in {LSeg(f,j -' 1)};
1 <= j -' 1 by A1,A5,XXREAL_0:2;
then
A16: j-' 1 < j by NAT_D:51;
e = LSeg(f,j -' 1) by A15,TARSKI:def 1;
hence thesis by A5,A16;
end;
end;
thus L~mid(f,i,j) = union A by A1,A2,A3,SPRECT_2:14
.= union B \/ union{LSeg(f,j -' 1)} by A6,ZFMISC_1:78
.= union B \/ LSeg(f,j -' 1) by ZFMISC_1:25
.= L~mid(f,i,j -' 1) \/ LSeg(f,j -' 1) by A1,A5,A4,SPRECT_2:14;
end;
theorem
for f, g being FinSequence of TOP-REAL 2 st f is being_S-Seq & g is
being_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 being_S-Seq
proof
let f,g be FinSequence of TOP-REAL 2 such that
A1: f is being_S-Seq and
A2: g is being_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 };
A7: len g >= 2 by A2,TOPREAL1:def 8;
then
A8: len g >= 1 by XXREAL_0:2;
then 1 in dom g by FINSEQ_3:25;
then
A9: g/.1 in L~g by A7,GOBOARD1:1;
set h = <*f/.len f*>^g;
A10: len f >= 2 by A1,TOPREAL1:def 8;
then 1 <= len f by XXREAL_0:2;
then
A11: len f in dom f by FINSEQ_3:25;
then
A12: f.len f = f/.len f by PARTFUN1:def 6
.=h.1 by FINSEQ_1:41;
A13: len h = len<*f/.len f*>+len g by FINSEQ_1:22
.= len g + 1 by FINSEQ_1:39;
then len h >= 1+1 by A8,XREAL_1:6;
then
A14: mid(h,2,len h) = (h/^(1+1-'1))|(len h-'2+1) by FINSEQ_6:def 3
.= (h/^1)|(len h-'2+1) by NAT_D:34
.= g|(len h-'2+1) by FINSEQ_6:45
.= g|(len h-'1-'1+1) by NAT_D:45
.= g|(len g-'1+1) by A13,NAT_D:34
.= g|len g by A7,XREAL_1:235,XXREAL_0:2
.= g by FINSEQ_1:58;
f/.len f in L~f by A10,A11,GOBOARD1:1;
then f/.len f <> g/.1 by A4,A9,XBOOLE_0:3;
then
A15: h is being_S-Seq by A2,A3,A6,SPRECT_2:60;
L~f /\ L~h = L~f /\ (LSeg(f/.len f,g/.1) \/ L~g) by A2,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
.={h.1} by A5,A11,A12,PARTFUN1:def 6;
hence thesis by A1,A12,A15,A14,JORDAN3:38;
end;
theorem
for f be FinSequence of TOP-REAL 2 for p be Point of TOP-REAL 2 st p
in L~f holds R_Cut(f,p)/.1 = f/.1
proof
let f be FinSequence of TOP-REAL 2;
let p be Point of TOP-REAL 2;
set i = Index(p,f);
assume
A1: p in L~f;
then
A2: 1 <= i by JORDAN3:8;
i <= len f by A1,JORDAN3:8;
then f <> {} by A2;
then
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:25;
then 1 <= len R_Cut(f,p) by A1,JORDAN3:8,NAT_1:11;
hence (R_Cut(f,p))/.1 = R_Cut(f,p).1 by FINSEQ_4:15
.= f.1 by A1,A2,JORDAN3:24
.= f/.1 by A3,PARTFUN1:def 6;
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 and
A2: j < len f and
A3: p in LSeg(f,j) and
A4: q in LSeg(f/.j,p);
A5: j+1 <= len f by A2,NAT_1:13;
then
A6: LSeg(f,j) = LSeg(f/.j,f/.(j+1)) by A1,TOPREAL1:def 3;
A7: f/.j in LSeg(f,j) by A1,A5,TOPREAL1:21;
then
A8: LSeg(f/.j,p) c= LSeg(f,j) by A3,A6,TOPREAL1:6;
then
A9: q in LSeg(f,j) by A4;
A10: LSeg(f,j) c= L~f by TOPREAL3:19;
per cases;
suppose
p = q;
hence thesis by A3,A10,JORDAN5C:9;
end;
suppose
A11: 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
1 <= j+1 by NAT_1:11;
then
A12: j+1 in dom f by A5,FINSEQ_3:25;
let i1, i2 be Nat such that
A13: q in LSeg(f,i1) and
A14: p in LSeg(f,i2) and
1 <= i1 and
A15: i1+1 <= len f and
A16: 1 <= i2 and
i2+1 <= len f;
A17: p in LSeg(f,i2) /\ LSeg(f,j) by A3,A14,XBOOLE_0:def 4;
then
A18: LSeg(f,i2) meets LSeg(f,j);
then
A19: j + 1 >= i2 by TOPREAL1:def 7;
A20: q in LSeg(f,i1) /\ LSeg(f,j) by A4,A8,A13,XBOOLE_0:def 4;
then
A21: LSeg(f,i1) meets LSeg(f,j);
then
A22: i1 + 1 >= j by TOPREAL1:def 7;
A23: now
assume
A24: i2 + 1 = j;
i2+(1+1) = i2+1+1;
then i2+2 <= len f by A2,A24,NAT_1:13;
then p in {f/.j} by A16,A17,A24,TOPREAL1:def 6;
then p = f/.j by TARSKI:def 1;
then q in {p} by A4,RLTOPSP1:70;
hence contradiction by A11,TARSKI:def 1;
end;
A25: now
assume that
A26: i2 + 1 > j and
A27: j+1 > i2;
A28: j <= i2 by A26,NAT_1:13;
i2 <= j by A27,NAT_1:13;
hence i2 = j by A28,XXREAL_0:1;
end;
i2 + 1 >= j by A18,TOPREAL1:def 7;
then i2 + 1 = j or i2 = j or j + 1 = i2 by A25,A19,XXREAL_0:1;
then
A29: i2 >= j by A23,NAT_1:11;
A30: now
assume that
A31: i1 + 1 > j and
A32: j+1 > i1;
A33: j <= i1 by A31,NAT_1:13;
i1 <= j by A32,NAT_1:13;
hence i1 = j by A33,XXREAL_0:1;
end;
A34: j in dom f by A1,A2,FINSEQ_3:25;
A35: now
assume f/.(j+1)=f/.j;
then j = j+1 by A12,A34,PARTFUN2:10;
hence contradiction;
end;
A36: now
A37: j+(1+1) = j+1+1;
assume i1 = j + 1;
then q in {f/.(j+1)} by A1,A15,A20,A37,TOPREAL1:def 6;
then q = f/.(j+1) by TARSKI:def 1;
hence contradiction by A3,A4,A6,A7,A11,A35,SPPOL_1:7,TOPREAL1:6;
end;
A38: j + 1 >= i1 by A21,TOPREAL1:def 7;
then i1 + 1 = j or i1 = j or j + 1 = i1 by A30,A22,XXREAL_0:1;
then i1 <= j by A36,NAT_1:11;
hence i1 <= i2 by A29,XXREAL_0:2;
assume
A39: i1 = i2;
not p in LSeg(f/.j,q) by A4,A11,Th6;
then not LE p,q,f/.j,f/.(j+1) by JORDAN3:30;
then LT q,p,f/.j,f/.(j+1) by A3,A6,A13,A23,A30,A22,A38,A35,A36,A39,
JORDAN3:28,XXREAL_0:1;
hence thesis by A23,A30,A22,A38,A36,A39,JORDAN3:def 6,XXREAL_0:1;
end;
hence thesis by A3,A9,A10,A11,JORDAN5C:30;
end;
end;
begin :: Special circular
theorem Th24:
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;
LeftComp f is_a_component_of (L~f)` by GOBOARD9:def 1;
hence LeftComp f is open by Th8;
RightComp f is_a_component_of (L~f)` by GOBOARD9:def 2;
hence thesis by Th8;
end;
registration
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:17;
hence L~f is non vertical by SPRECT_1:15;
S-bound L~f <> N-bound L~f by TOPREAL5:16;
hence thesis by SPRECT_1:16;
end;
cluster LeftComp f -> being_Region;
coherence
proof
thus LeftComp f is open by Th24;
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 by CONNSP_1:def 6;
A is connected by A2,CONNSP_1:def 5;
hence thesis by A1,CONNSP_1:23;
end;
cluster RightComp f -> being_Region;
coherence
proof
thus RightComp f is open by Th24;
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 by CONNSP_1:def 6;
A is connected by A4,CONNSP_1:def 5;
hence thesis by A3,CONNSP_1:23;
end;
end;
theorem Th25:
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:10;
then RightComp f c= (L~f)` by XBOOLE_1:7;
hence thesis by SUBSET_1:23;
end;
theorem Th26:
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:10;
then LeftComp f c= (L~f)` by XBOOLE_1:7;
hence thesis by SUBSET_1:23;
end;
theorem Th27:
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: i_w_n f <= len G by JORDAN5D:45;
A2: G*(i_w_n f,width G) = N-min L~f by JORDAN5D:def 7;
assume
A3: i_w_n f >= i_e_n f;
A4: 1 <= i_e_n f by JORDAN5D:45;
A5: (N-min L~f)`1 < (N-max L~f)`1 by SPRECT_2:51;
A6: G*(i_e_n f,width G) = N-max L~f by JORDAN5D:def 8;
then i_w_n f <> i_e_n f by A5,JORDAN5D:def 7;
then
A7: i_w_n f > i_e_n f by A3,XXREAL_0:1;
width G > 1 by GOBOARD7:33;
hence contradiction by A1,A2,A4,A6,A5,A7,GOBOARD5:3;
end;
theorem Th28:
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:45;
i_e_n f <= len GoB f by JORDAN5D:45;
hence i < len GoB f by Th27,XXREAL_0:2;
thus thesis by JORDAN5D:def 7;
end;
theorem Th29:
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: i <= len GoB f by A1,FINSEQ_3:25;
4 < len f by GOBOARD7:34;
then
A5: len f -' 1 + 1 = len f by XREAL_1:235,XXREAL_0:2;
A6: f/.len f = f/.1 by FINSEQ_6:def 1;
A7: 1 <= len f by GOBOARD7:34,XXREAL_0:2;
then
A8: 1 in dom f by FINSEQ_3:25;
A9: 1 <= width GoB f by GOBRD11:34;
A10: f/.2 in N-most L~f by A3,SPRECT_2:30;
A11: 1+1 <= len f by GOBOARD7:34,XXREAL_0:2;
then
A12: 1+1 in dom f by FINSEQ_3:25;
then consider i1,j1 being Nat such that
A13: [i1,j1] in Indices GoB f and
A14: f/.2 = (GoB f)*(i1,j1) by GOBOARD2:14;
A15: 1 <= j1 by A13,MATRIX_0:32;
A16: j1 <= width GoB f by A13,MATRIX_0:32;
A17: 1 <= i1 by A13,MATRIX_0:32;
A18: i1 <= len GoB f by A13,MATRIX_0:32;
now
A19: (f/.2)`2 = (N-min L~f)`2 by A10,PSCOMP_1:39
.= N-bound L~f by EUCLID:52;
assume
A20: j1 < width GoB f;
(GoB f)*(i1,width GoB f)`2 = (GoB f)*(1,width GoB f)`2 by A9,A17,A18,
GOBOARD5:1
.= N-bound L~f by JORDAN5D:40;
hence contradiction by A14,A15,A17,A18,A20,A19,GOBOARD5:4;
end;
then
A21: j1 = width GoB f by A16,XXREAL_0:1;
A22: now
assume i > i1;
then (f/.2)`1 < (N-min L~f)`1 by A2,A3,A14,A4,A15,A17,A21,GOBOARD5:3;
hence contradiction by A10,PSCOMP_1:39;
end;
A23: 1 <= i by A1,FINSEQ_3:25;
then
A24: [i,width GoB f] in Indices GoB f by A9,A4,MATRIX_0:30;
|.i-i1.|+0 =|.i-i1.|+|.width GoB f-width GoB f.| by ABSVALUE:2
.= 1 by A2,A12,A13,A14,A8,A24,A21,GOBOARD5:12;
hence
A25: f/.2 = (GoB f)*(i+1,width GoB f) by A14,A21,A22,SEQM_3:41;
A26: len f -' 1 <= len f by NAT_D:44;
1 <= len f -' 1 by A11,NAT_D:49;
then
A27: len f -' 1 in dom f by A26,FINSEQ_3:25;
then consider i2,j2 being Nat such that
A28: [i2,j2] in Indices GoB f and
A29: f/.(len f -' 1) = (GoB f)*(i2,j2) by GOBOARD2:14;
A30: 1 <= i2 by A28,MATRIX_0:32;
A31: j2 <= width GoB f by A28,MATRIX_0:32;
A32: i2 <= len GoB f by A28,MATRIX_0:32;
len f in dom f by A7,FINSEQ_3:25;
then
A33: |.i2-i.|+|.j2-width GoB f.| = 1 by A2,A24,A6,A5,A27,A28,A29,GOBOARD5:12;
per cases by A33,SEQM_3:42;
suppose that
A34: |.i2-i.|=1 and
A35: j2=width GoB f;
(f/.(len f -' 1))`2 = ((GoB f)*(1,width GoB f))`2 by A9,A29,A30,A32,A35,
GOBOARD5:1
.= (N-min L~f)`2 by A2,A3,A9,A23,A4,GOBOARD5:1
.= N-bound L~f by EUCLID:52;
then
A36: f/.(len f -' 1) in N-most L~f by A11,A27,GOBOARD1:1,SPRECT_2:10;
now
per cases by A34,SEQM_3:41;
suppose
i > i2;
then (f/.(len f -' 1))`1 < (N-min L~f)`1 by A2,A3,A9,A4,A29,A30,A35,
GOBOARD5:3;
hence contradiction by A36,PSCOMP_1:39;
end;
suppose
i+1 = i2;
then 2 >= len f -' 1 by A25,A26,A29,A35,GOBOARD7:37;
then 2+1 >= len f by NAT_D:52;
hence contradiction by GOBOARD7:34,XXREAL_0:2;
end;
end;
hence thesis;
end;
suppose that
A37: |.j2-width GoB f.|=1 and
A38: i2=i;
width GoB f = j2+1 by A31,A37,SEQM_3:41;
hence thesis by A29,A38,NAT_D:34;
end;
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;
1+1 <= len f by GOBOARD7:34,XXREAL_0:2;
then
A4: f/.1 in LSeg(f,1) by TOPREAL1:21;
assume f/.1 in L~mid(f,i,j);
then consider n such that
A5: 1 <= n and
A6: n+1 <= len mid(f,i,j) and
A7: f/.1 in LSeg(mid(f,i,j),n) by SPPOL_2:13;
n < len mid(f,i,j) by A6,NAT_1:13;
then
A8: n<j-'i+1 by A1,A2,A3,FINSEQ_6:186;
then LSeg(mid(f,i,j),n)=LSeg(f,n+i-'1) by A1,A2,A3,A5,JORDAN4:19;
then
A9: f/.1 in LSeg(f,1) /\ LSeg(f,n+i-'1) by A7,A4,XBOOLE_0:def 4;
then
A10: LSeg(f,1) meets LSeg(f,n+i-'1);
assume that
A11: i <> 1 and
A12: j <> len f;
per cases by A10,GOBOARD5:def 4;
suppose
1+1 >= n+i-'1;
then
A13: n+i <= 2+1 by NAT_D:52;
i > 1 by A1,A11,XXREAL_0:1;
then
A14: i >= 1+1 by NAT_1:13;
n+i >= i+1 by A5,XREAL_1:6;
then i+1 <= 2+1 by A13,XXREAL_0:2;
then i <= 2 by XREAL_1:6;
then
A15: i = 2 by A14,XXREAL_0:1;
then n <= 1 by A13,XREAL_1:6;
then n = 1 by A5,XXREAL_0:1;
then
A16: n+i-'1 = 2 by A15,NAT_D:34;
A17: 2 < len f by GOBOARD7:34,XXREAL_0:2;
1+2 <= len f by GOBOARD7:34,XXREAL_0:2;
then LSeg(f,1) /\ LSeg(f,1+1) = {f/.(1+1)} by TOPREAL1:def 6;
then f/.1 = f/.2 by A9,A16,TARSKI:def 1;
hence contradiction by A17,GOBOARD7:36;
end;
suppose
A18: n+i-'1+1 >= len f;
n <= n+i by NAT_1:11;
then
A19: len f <= n+i by A5,A18,XREAL_1:235,XXREAL_0:2;
j-'i+1+i = j-'i+i+1 .= j+1 by A2,XREAL_1:235;
then n+i < j+1 by A8,XREAL_1:6;
then
A20: n+i <= j by NAT_1:13;
j < len f by A3,A12,XXREAL_0:1;
hence contradiction by A19,A20,XXREAL_0:2;
end;
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;
A1: N-most L~f c= LSeg(NW-corner L~f,NE-corner L~f) by XBOOLE_1:17;
assume
A2: f/.1 = N-min L~f;
then
A3: f/.2 in N-most L~f by SPRECT_2:30;
A4: LSeg(NW-corner L~f,NE-corner L~f) c= L~SpStSeq L~f by Th14;
f/.1 in LSeg(NW-corner L~f,NE-corner L~f) by A2,Th15;
then LSeg(f/.1,f/.2) c= LSeg(NW-corner L~f,NE-corner L~f) by A3,A1,TOPREAL1:6
;
hence thesis by A4;
end;
begin :: Rectangular
theorem Th32:
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:41;
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 3;
per cases by A3,XBOOLE_0:def 3;
suppose
A4: p in LSeg(NW-corner D,NE-corner D);
A5: N-bound L~SpStSeq D = N-bound D by SPRECT_1:60;
then
A6: (NE-corner D)`2 = N-bound L~f by A2,EUCLID:52;
(NW-corner D)`2 = N-bound L~f by A2,A5,EUCLID:52;
hence thesis by A4,A6,GOBOARD7:6;
end;
suppose
A7: p in LSeg(NE-corner D,SE-corner D);
A8: E-bound L~SpStSeq D = E-bound D by SPRECT_1:61;
then
A9: (SE-corner D)`1 = E-bound L~f by A2,EUCLID:52;
(NE-corner D)`1 = E-bound L~f by A2,A8,EUCLID:52;
hence thesis by A7,A9,GOBOARD7:5;
end;
suppose
A10: p in LSeg(SE-corner D,SW-corner D);
A11: S-bound L~SpStSeq D = S-bound D by SPRECT_1:59;
then
A12: (SW-corner D)`2 = S-bound L~f by A2,EUCLID:52;
(SE-corner D)`2 = S-bound L~f by A2,A11,EUCLID:52;
hence thesis by A10,A12,GOBOARD7:6;
end;
suppose
A13: p in LSeg(SW-corner D,NW-corner D);
A14: W-bound L~SpStSeq D = W-bound D by SPRECT_1:58;
then
A15: (NW-corner D)`1 = W-bound L~f by A2,EUCLID:52;
(SW-corner D)`1 = W-bound L~f by A2,A14,EUCLID:52;
hence thesis by A13,A15,GOBOARD7:5;
end;
end;
registration
cluster rectangular for special_circular_sequence;
existence
proof
set C = the non empty compact non vertical non horizontal Subset of TOP-REAL2;
SpStSeq C is special_circular_sequence;
hence thesis;
end;
end;
theorem Th33:
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;
A3: len g >= 2 by TOPREAL1:def 8;
then g/.1 in L~g by JORDAN3:1;
then g/.1 in LeftComp f /\ L~g by A1,XBOOLE_0:def 4;
then
A4: LeftComp f meets L~g;
g/.len g in L~g by A3,JORDAN3:1;
then g/.len g in RightComp f /\ L~g by A2,XBOOLE_0:def 4;
then
A5: RightComp f meets L~g;
A6: LeftComp f misses RightComp f by SPRECT_1:88;
assume L~f misses L~g;
then L~g c= (L~f)` by SUBSET_1:23;
then
A7: L~g c= LeftComp f \/ RightComp f by GOBRD12:10;
A8: L~g is_an_arc_of g/.1,g/.len g by TOPREAL1:25;
A9: RightComp f is open by Th24;
LeftComp f is open by Th24;
hence contradiction by A7,A9,A4,A5,A6,A8,JORDAN6:10,TOPREAL5:1;
end;
theorem Th34:
for f being rectangular special_circular_sequence holds SpStSeq L~f = f
proof
let f be rectangular special_circular_sequence;
set C = L~f, g = SpStSeq C;
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;
A2: 5 = len f by SPRECT_1:82;
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;
then
A3: 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 FINSEQ_1:22
.= 3+len<*SW-corner L~f,NW-corner L~f*> by FINSEQ_1:45
.= 3+2 by FINSEQ_1:44;
A4: for i being Nat st i in dom f holds f/.i = g/.i
proof
let i be Nat;
assume
A5: i in dom f;
then
A6: 0 <> i by FINSEQ_3:25;
A7: i <= len f by A5,FINSEQ_3:25;
A8: f/.1 = W-max C by SPRECT_1:83
.= NW-corner D by A1,SPRECT_1:75
.= NW-corner C by A1,SPRECT_1:62
.= g/.1 by SPRECT_1:35;
i <= 5 by A2,A7;
then i = 0 or ... or i = 5;
then per cases by A6;
suppose
i = 1;
hence thesis by A8;
end;
suppose
A9: i = 2;
hence f/.i = E-max C by SPRECT_1:84
.= NE-corner D by A1,SPRECT_1:79
.= NE-corner C by A1,SPRECT_1:63
.= g/.i by A9,SPRECT_1:36;
end;
suppose
A10: i = 3;
hence f/.i = E-min C by SPRECT_1:85
.= SE-corner D by A1,SPRECT_1:78
.= SE-corner C by A1,SPRECT_1:65
.= g/.i by A10,SPRECT_1:37;
end;
suppose
A11: i = 4;
hence f/.i = W-min C by SPRECT_1:86
.= SW-corner D by A1,SPRECT_1:74
.= SW-corner C by A1,SPRECT_1:64
.= g/.i by A11,SPRECT_1:38;
end;
suppose
A12: i = 5;
hence f/.i = f/.1 by A2,FINSEQ_6:def 1
.= g/.i by A3,A8,A12,FINSEQ_6:def 1;
end;
end;
dom f = dom g by A2,A3,FINSEQ_3:29;
hence thesis by A4,FINSEQ_5:12;
end;
theorem Th35:
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: LSeg(SE-corner C, NE-corner C) = E by SPRECT_1:23;
A2: LSeg(SW-corner C, SE-corner C) = S by SPRECT_1:24;
A3: LSeg(SW-corner C, NW-corner C) = W by SPRECT_1:26;
A4: LSeg(NW-corner C, NE-corner C) = N by SPRECT_1:25;
A5: C = L~SpStSeq C by Th34;
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 object;
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 A5,A6,
SPRECT_1:41;
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 3;
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 3;
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 A1,A2
,A4,A3;
hence thesis;
end;
let x be object;
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 A1,A2,A4,A3;
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 3;
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 3;
hence thesis by A5,SPRECT_1:41;
end;
theorem Th36:
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/.2 = N-max L~f by SPRECT_1:84;
A2: f/.1 = N-min L~f by SPRECT_1:83;
then
A3: (f/.1)`1 < (f/.2)`1 by A1,SPRECT_2:51;
A4: (f/.2)`2 = (f/.1)`2 by A2,A1,PSCOMP_1:37;
A5: f/.4 = S-min L~f by SPRECT_1:86;
A6: f/.3 = S-max L~f by SPRECT_1:85;
then
A7: (f/.3)`2 = (f/.4)`2 by A5,PSCOMP_1:53;
A8: len<*(f/.3)`1,(f/.4)`1,(f/.5)`1*> = 3 by FINSEQ_1:45;
A9: len f = 5 by SPRECT_1:82;
then
A10: f/.1 = f/.5 by FINSEQ_6:def 1;
set g = <*(f/.1)`1,(f/.2)`1*>;
reconsider h = <*(f/.1)`1,(f/.2)`1*>^<*(f/.3)`1,(f/.4)`1 ,(f/.5)`1*>
as FinSequence of REAL by RVSUM_1:145;
A11: f/.3 = E-min L~f by SPRECT_1:85;
A12: f/.2 = E-max L~f by SPRECT_1:84;
then
A13: (f/.3)`1 = (f/.2)`1 by A11,PSCOMP_1:45;
A14: len g = 2 by FINSEQ_1:44;
A15: dom g = {1,2} by FINSEQ_1:2,89;
A16: g is increasing
proof
let n,m such that
A19: n in dom g and
A20: m in dom g and
A21: n<m;
A22: m = 1 or m = 2 by A15,A20,TARSKI:def 2;
n = 1 or n = 2 by A15,A19,TARSKI:def 2;
hence g.n < g.m by A2,A1,A21,A22,SPRECT_2:51;
end;
A23: f/.4 = W-min L~f by SPRECT_1:86;
A24: len h = len <*(f/.1)`1,(f/.2)`1*> + len<*(f/.3)`1,(f/.4)`1,(f/.5)`1*>
by FINSEQ_1:22
.= len <*(f/.1)`1,(f/.2)`1*> + 3 by FINSEQ_1:45
.= 2 + 3 by FINSEQ_1:44
.= len f by SPRECT_1:82;
for n st n in dom h holds h.n = (f/.n)`1
proof
let n;
assume
A25: n in dom h;
then
A26: 1 <= n by FINSEQ_3:25;
n <= 5 by A9,A24,A25,FINSEQ_3:25;
then n = 0 or ... or n = 5;
then per cases by A26;
suppose
A27: n=1;
then n in dom g by A14,FINSEQ_3:25;
hence h.n = <*(f/.1)`1,(f/.2)`1*>.1 by A27,FINSEQ_1:def 7
.= (f/.n)`1 by A27;
end;
suppose
A28: n=2;
then n in dom g by A14,FINSEQ_3:25;
hence h.n = <*(f/.1)`1,(f/.2)`1*>.2 by A28,FINSEQ_1:def 7
.= (f/.n)`1 by A28;
end;
suppose
A29: n=3;
hence h.n = h.(2+1)
.= <*(f/.3)`1,(f/.4)`1,(f/.5)`1*>.1 by A14,A8,FINSEQ_1:65
.= (f/.n)`1 by A29;
end;
suppose
A30: n=4;
hence h.n = h.(2+2)
.= <*(f/.3)`1,(f/.4)`1,(f/.5)`1*>.2 by A14,A8,FINSEQ_1:65
.= (f/.n)`1 by A30;
end;
suppose
A31: n=5;
hence h.n = h.(2+3)
.= <*(f/.3)`1,(f/.4)`1,(f/.5)`1*>.3 by A14,A8,FINSEQ_1:65
.= (f/.n)`1 by A31;
end;
end;
then
A32: X_axis f = h by A24,GOBOARD1:def 1;
A33: rng g = { (f/.1)`1,(f/.2)`1 } by FINSEQ_2:127;
A34: f/.1 = W-max L~f by SPRECT_1:83;
then
A35: (f/.4)`2 < (f/.5)`2 by A23,A10,SPRECT_2:57;
reconsider vv1 = <*(f/.1)`1,(f/.2)`1*> as FinSequence of REAL by RVSUM_1:145;
{(f/.3)`1,(f/.4)`1,(f/.5)`1} c= { (f/.1)`1,(f/.2)`1 }
proof
let x be object;
assume
A36: x in {(f/.3)`1,(f/.4)`1,(f/.5)`1};
per cases by A36,ENUMSET1:def 1;
suppose
x = (f/.3)`1;
then x = (f/.2)`1 by A12,A11,PSCOMP_1:45;
hence thesis by TARSKI:def 2;
end;
suppose
x = (f/.4)`1;
then x = (f/.1)`1 by A34,A23,PSCOMP_1:29;
hence thesis by TARSKI:def 2;
end;
suppose
x = (f/.5)`1;
then x = (f/.1)`1 by A9,FINSEQ_6:def 1;
hence thesis by TARSKI:def 2;
end;
end;
then
A37: rng g = rng<*(f/.1)`1,(f/.2)`1*> \/ {(f/.3)`1,(f/.4)`1,(f/.5)`1} by A33,
XBOOLE_1:12
.= rng<*(f/.1)`1,(f/.2)`1*> \/ rng<*(f/.3)`1,(f/.4)`1,(f/.5)`1*> by
FINSEQ_2:128
.= rng X_axis f by A32,FINSEQ_1:31;
len g = 2 by FINSEQ_1:44
.= card rng X_axis f by A33,A37,A3,CARD_2:57;
then
A38: v1 = vv1 by A37,A16,SEQ_4:def 21;
then
A39: v1.1 = (f/.1)`1;
set g = <*(f/.4)`2,(f/.5)`2*>;
reconsider h = <*(f/.1)`2,(f/.2)`2,(f/.3)`2*>^<*(f/.4)`2,(f/.5)`2*>
as FinSequence of REAL by RVSUM_1:145;
A40: len h = len <*(f/.1)`2,(f/.2)`2,(f/.3)`2*> + len<*(f/.4)`2,(f/.5)`2*>
by FINSEQ_1:22
.= len <*(f/.4)`2,(f/.5)`2*> + 3 by FINSEQ_1:45
.= 2 + 3 by FINSEQ_1:44
.= len f by SPRECT_1:82;
A41: len<*(f/.1)`2,(f/.2)`2,(f/.3)`2*> = 3 by FINSEQ_1:45;
A42: dom g = {1,2} by FINSEQ_1:2,89;
A43: 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: m = 1 or m = 2 by A42,A47,TARSKI:def 2;
n = 1 or n = 2 by A42,A46,TARSKI:def 2;
hence g.n < g.m by A34,A23,A10,A48,A49,SPRECT_2:57;
end;
A50: v1.2 = (f/.2)`1 by A38;
A51: len g = 2 by FINSEQ_1:44;
for n st n in dom h holds h.n = (f/.n)`2
proof
let n;
assume
A52: n in dom h;
then
A53: 1 <= n by FINSEQ_3:25;
n <= 5 by A9,A40,A52,FINSEQ_3:25;
then n = 0 or ... or n = 5;
then per cases by A53;
suppose
A54: n=1;
then n in dom<*(f/.1)`2,(f/.2)`2,(f/.3)`2*> by A41,FINSEQ_3:25;
hence h.n = <*(f/.1)`2,(f/.2)`2,(f/.3)`2*>.1 by A54,FINSEQ_1:def 7
.= (f/.n)`2 by A54;
end;
suppose
A55: n=2;
then n in dom<*(f/.1)`2,(f/.2)`2,(f/.3)`2*> by A41,FINSEQ_3:25;
hence h.n = <*(f/.1)`2,(f/.2)`2,(f/.3)`2*>.2 by A55,FINSEQ_1:def 7
.= (f/.n)`2 by A55;
end;
suppose
A56: n=3;
then n in dom<*(f/.1)`2,(f/.2)`2,(f/.3)`2*> by A41,FINSEQ_3:25;
hence h.n = <*(f/.1)`2,(f/.2)`2,(f/.3)`2*>.3 by A56,FINSEQ_1:def 7
.= (f/.n)`2 by A56;
end;
suppose
A57: n=4;
hence h.n = h.(3+1) .= <*(f/.4)`2,(f/.5)`2*>.1 by A51,A41,FINSEQ_1:65
.= (f/.n)`2 by A57;
end;
suppose
A58: n=5;
hence h.n = h.(2+3) .= <*(f/.4)`2,(f/.5)`2*>.2 by A51,A41,FINSEQ_1:65
.= (f/.n)`2 by A58;
end;
end;
then
A59: Y_axis f = h by A40,GOBOARD1:def 2;
A60: rng g = { (f/.4)`2,(f/.5)`2 } by FINSEQ_2:127;
{(f/.1)`2,(f/.2)`2,(f/.3)`2} c= { (f/.4)`2,(f/.5)`2 }
proof
let x be object;
assume
A61: x in {(f/.1)`2,(f/.2)`2,(f/.3)`2};
per cases by A61,ENUMSET1:def 1;
suppose
x = (f/.1)`2;
hence thesis by A10,TARSKI:def 2;
end;
suppose
x = (f/.2)`2;
then x = (f/.1)`2 by A2,A1,PSCOMP_1:37;
hence thesis by A10,TARSKI:def 2;
end;
suppose
x = (f/.3)`2;
then x = (f/.4)`2 by A6,A5,PSCOMP_1:53;
hence thesis by TARSKI:def 2;
end;
end;
then
A62: rng g = {(f/.1)`2,(f/.2)`2,(f/.3)`2} \/ {(f/.4)`2,(f/.5)`2} by A60,
XBOOLE_1:12
.= rng<*(f/.1)`2,(f/.2)`2,(f/.3)`2*> \/ {(f/.4)`2,(f/.5)`2} by FINSEQ_2:128
.= rng<*(f/.1)`2,(f/.2)`2,(f/.3)`2*> \/ rng<*(f/.4)`2,(f/.5)`2*> by
FINSEQ_2:127
.= rng Y_axis f by A59,FINSEQ_1:31;
reconsider vv2 = <*(f/.4)`2,(f/.1)`2*> as FinSequence of REAL
by RVSUM_1:145;
len g = 2 by FINSEQ_1:44
.= card rng Y_axis f by A60,A62,A35,CARD_2:57;
then
A63: v2 = vv2 by A10,A62,A43,SEQ_4:def 21;
then
A64: v2.1 = (f/.4)`2;
A65: v2.2 = (f/.1)`2 by A63;
A66: (f/.1)`1 = (f/.4)`1 by A34,A23,PSCOMP_1:29;
A67: 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
A68: [n,m]in { [1,1], [1,2],[2,1], [2,2]} by Th2;
per cases by A68,ENUMSET1:def 2;
suppose
A69: [n,m] = [1,1];
then
A70: m = 1 by XTUPLE_0:1;
A71: n = 1 by A69,XTUPLE_0:1;
hence G*(n,m) = f/.4 by A70,MATRIX_0:50
.= |[v1.n,v2.m]| by A39,A64,A66,A71,A70,EUCLID:53;
end;
suppose
A72: [n,m] = [1,2];
then
A73: m = 2 by XTUPLE_0:1;
A74: n = 1 by A72,XTUPLE_0:1;
hence G*(n,m) = f/.1 by A73,MATRIX_0:50
.= |[v1.n,v2.m]| by A39,A65,A74,A73,EUCLID:53;
end;
suppose
A75: [n,m] = [2,1];
then
A76: m = 1 by XTUPLE_0:1;
A77: n = 2 by A75,XTUPLE_0:1;
hence G*(n,m) = f/.3 by A76,MATRIX_0:50
.= |[v1.n,v2.m]| by A50,A64,A13,A7,A77,A76,EUCLID:53;
end;
suppose
A78: [n,m] = [2,2];
then
A79: m = 2 by XTUPLE_0:1;
A80: n = 2 by A78,XTUPLE_0:1;
hence G*(n,m) = f/.2 by A79,MATRIX_0:50
.= |[v1.n,v2.m]| by A50,A65,A4,A80,A79,EUCLID:53;
end;
end;
A81: width G = 2 by MATRIX_0:47
.= len v2 by A63,FINSEQ_1:44;
len G = 2 by MATRIX_0:47
.= len v1 by A38,FINSEQ_1:44;
then GoB(v1,v2) = G by A81,A67,GOBOARD2:def 1;
hence thesis by GOBOARD2:def 2;
end;
theorem Th37:
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: S-bound L~f < N-bound L~f by SPRECT_1:32;
A2: Lf is Subset of TOP-REAL 2 from DOMAIN_1:sch 7;
A3: RC is Subset of TOP-REAL 2 from DOMAIN_1:sch 7;
A4: L~f = Lf by Th35;
LC is Subset of TOP-REAL 2 from DOMAIN_1:sch 7;
then reconsider Lc9=LC,Rc9=RC,Lf as Subset of TOP-REAL 2 by A3,A2;
reconsider Lf as Subset of TOP-REAL 2;
reconsider Lc9, Rc9 as Subset of TOP-REAL 2;
A5: W-bound L~f < E-bound L~f by SPRECT_1:31;
then reconsider Lc=Lc9, Rc=Rc9 as Subset of (TOP-REAL 2)|Lf` by A1,JORDAN1:39
,41;
reconsider Lc, Rc as Subset of (TOP-REAL 2)|Lf`;
A6: 1/2*(S-bound L~f) + 1/2*(S-bound L~f) = (S-bound L~f);
Rc = Rc9;
then Lc is a_component by A5,A1,JORDAN1:36;
then
A7: Lc9 is_a_component_of Lf` by CONNSP_1:def 6;
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));
A8: 1+1 <= len f by GOBOARD7:34,XXREAL_0:2;
A9: p`2 = q`2+|[0,1]|`2 by TOPREAL3:2
.= q`2+1 by EUCLID:52;
A10: GoB f = (f/.4,f/.1)][(f/.3,f/.2) by Th36;
then
A11: 1+1 = width GoB f by MATRIX_0:47;
then q`2 = (1/2*((GoB f)*(1,width GoB f)+f/.2))`2 by A10,MATRIX_0:50
.= (1/2*(f/.1+f/.2))`2 by A10,A11,MATRIX_0:50
.= 1/2*(f/.1+f/.2)`2 by TOPREAL3:4
.= 1/2*((f/.1)`2+(f/.2)`2) by TOPREAL3:2
.= 1/2*((N-min L~f)`2+(f/.2)`2) by SPRECT_1:83
.= 1/2*((N-min L~f)`2+(N-max L~f)`2) by SPRECT_1:84
.= 1/2*(N-bound L~f+(N-max L~f)`2) by EUCLID:52
.= 1/2*(N-bound L~f+N-bound L~f) by EUCLID:52
.= N-bound L~f;
then p`2 > 0 + N-bound L~f by A9,XREAL_1:8;
then
A12: p in LC;
A13: 1+1 = len GoB f by A10,MATRIX_0:47;
then
A14: p in Int cell(GoB f,1,1+1) by A11,GOBOARD6:32;
A15: f/.(1+1) = (GoB f)*(1+1,1+1) by A10,MATRIX_0:50;
1 < width GoB f by GOBOARD7:33;
then
A16: 1+1 <= width GoB f by NAT_1:13;
then
A17: [1+1,1+1] in Indices GoB f by A13,MATRIX_0:30;
1 <= len GoB f by GOBOARD7:32;
then
A18: [1,1+1] in Indices GoB f by A16,MATRIX_0:30;
A19: f/.1 = (GoB f)*(1,1+1) by A10,MATRIX_0:50;
then right_cell(f,1) = cell(GoB f,1,1) by A8,A18,A17,A15,GOBOARD5:28;
then
A20: Int cell(GoB f,1,1) c= RightComp f by GOBOARD9:def 2;
left_cell(f,1) = cell(GoB f,1,1+1)by A8,A18,A19,A17,A15,GOBOARD5:28;
then Int cell(GoB f,1,1+1) c= LeftComp f by GOBOARD9:def 1;
then
A21: LC meets LeftComp f by A14,A12,XBOOLE_0:3;
A22: (f/.2)`1 = (E-max L~f)`1 by SPRECT_1:84
.= E-bound L~f by EUCLID:52;
set p = 1/2*((GoB f)*(1,1)+(GoB f)*(2,2));
A23: p in Int cell(GoB f,1,1) by A13,A11,GOBOARD6:31;
A24: p = 1/2*((GoB f)*(1,1)+f/.2) by A10,MATRIX_0:50
.= 1/2*(f/.4+f/.2) by A10,MATRIX_0:50;
then
A25: p`1 = 1/2*(f/.4+f/.2)`1 by TOPREAL3:4
.= 1/2*((f/.4)`1+(f/.2)`1) by TOPREAL3:2
.= 1/2*(f/.4)`1+ 1/2*(f/.2)`1;
LeftComp f is_a_component_of (L~f)` by GOBOARD9:def 1;
hence LeftComp f = LC by A4,A7,A21,GOBOARD9:1;
A26: 1/2*(W-bound L~f) + 1/2*(W-bound L~f) = (W-bound L~f);
A27: 1/2*(E-bound L~f) + 1/2*(E-bound L~f) = (E-bound L~f);
A28: 1/2*(N-bound L~f) + 1/2*(N-bound L~f) = (N-bound L~f);
A29: (f/.4)`1 = (W-min L~f)`1 by SPRECT_1:86
.= W-bound L~f by EUCLID:52;
then 1/2*(f/.4)`1 < 1/2*E-bound L~f by SPRECT_1:31,XREAL_1:68;
then
A30: p`1 < E-bound L~f by A27,A25,A22,XREAL_1:6;
A31: p`2 = 1/2*(f/.4+f/.2)`2 by A24,TOPREAL3:4
.= 1/2*((f/.4)`2+(f/.2)`2) by TOPREAL3:2
.= 1/2*(f/.4)`2+ 1/2*(f/.2)`2;
Lc = Lc9;
then Rc is a_component by A5,A1,JORDAN1:36;
then
A32: Rc9 is_a_component_of Lf` by CONNSP_1:def 6;
A33: (f/.2)`2 = (N-max L~f)`2 by SPRECT_1:84
.= N-bound L~f by EUCLID:52;
A34: (f/.4)`2 = (S-min L~f)`2 by SPRECT_1:86
.= S-bound L~f by EUCLID:52;
then 1/2*(f/.4)`2 < 1/2*N-bound L~f by SPRECT_1:32,XREAL_1:68;
then
A35: p`2 < N-bound L~f by A28,A31,A33,XREAL_1:6;
1/2*(f/.2)`2 > 1/2*S-bound L~f by A33,SPRECT_1:32,XREAL_1:68;
then
A36: S-bound L~f < p`2 by A6,A31,A34,XREAL_1:6;
1/2*(f/.2)`1 > 1/2*W-bound L~f by A22,SPRECT_1:31,XREAL_1:68;
then W-bound L~f < p`1 by A26,A25,A29,XREAL_1:6;
then p in RC by A30,A36,A35;
then
A37: RC meets RightComp f by A23,A20,XBOOLE_0:3;
RightComp f is_a_component_of (L~f)` by GOBOARD9:def 2;
hence thesis by A4,A32,A37,GOBOARD9:1;
end;
registration
cluster clockwise_oriented for rectangular special_circular_sequence;
existence
proof
set C = the non empty compact non vertical non horizontal Subset of TOP-REAL2;
SpStSeq C is clockwise_oriented;
hence thesis;
end;
end;
registration
cluster -> clockwise_oriented for rectangular special_circular_sequence;
coherence
proof
let f be rectangular special_circular_sequence;
ex D being non vertical non horizontal non empty compact Subset of
TOP-REAL 2 st f = SpStSeq D by SPRECT_1:def 2;
hence thesis;
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,Th33;
assume
A4: Last_Point(L~g,g/.1,g/.len g,L~f) = NW-corner L~f;
set nw = NW-corner L~f, inw = Index(nw,g);
A5: len g in dom g by FINSEQ_5:6;
then
A6: g.len g = g/.len g by PARTFUN1:def 6;
A7: 1 <= inw+1 by NAT_1:11;
L~g is_an_arc_of g/.1, g/.len g by TOPREAL1:25;
then
A8: nw in L~g /\ L~f by A3,A4,JORDAN5C:def 2;
then
A9: nw in L~g by XBOOLE_0:def 4;
then
A10: 1 <= inw by JORDAN3:8;
A11: nw in LSeg(g,inw) by A9,JORDAN3:9;
A12: inw < len g by A9,JORDAN3:8;
then
A13: inw+1 <= len g by NAT_1:13;
then
A14: inw+1 in dom g by A7,FINSEQ_3:25;
A15: L~f misses RightComp f by Th25;
A16: now
A17: len g >= 1 by A13,A7,XXREAL_0:2;
assume nw <> g.(inw+1);
then
A18: nw <> g/.(inw+1) by A14,PARTFUN1:def 6;
per cases;
suppose
A19: g/.(inw+1) in L~f;
then inw+1 <> len g by A2,A15,XBOOLE_0:3;
then inw+1 < len g by A13,XXREAL_0:1;
then
A20: inw+1+1 <= len g by NAT_1:13;
then g/.(inw+1) in LSeg(g,inw+1) by A7,TOPREAL1:21;
then inw >= inw+1 by A3,A4,A10,A13,A11,A7,A18,A19,A20,JORDAN5C:28;
hence contradiction by XREAL_1:29;
end;
suppose
A21: not g/.(inw+1) in L~f;
A22: now
assume
A23: g/.(inw+1) in RightComp 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} by Th37;
then
A24: 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 A23;
A25: LSeg(g,inw) is vertical or LSeg(g,inw) is horizontal by SPPOL_1:19;
LSeg(g,inw) = LSeg(g/.inw,g/.(inw+1)) by A10,A13,TOPREAL1:def 3;
then (g/.(inw+1))`1 = nw`1 or (g/.(inw+1))`2 = nw`2 by A11,A25,
SPPOL_1:40,41;
hence contradiction by A24,EUCLID:52;
end;
then reconsider
m = mid(g,inw+1,len g) as S-Sequence_in_R2 by A2,A13,A7,A17,JORDAN3:6;
A26: inw+1<len g by A2,A13,A22,XXREAL_0:1;
g/.(inw+1) in (L~f)` by A21,SUBSET_1:29;
then g/.(inw+1) in LeftComp f \/ RightComp f by GOBRD12:10;
then g/.(inw+1) in LeftComp f by A22,XBOOLE_0:def 3;
then
A27: m/.1 in LeftComp f by A5,A14,SPRECT_2:8;
m/.len m in RightComp f by A2,A5,A14,SPRECT_2:9;
then L~f meets L~m by A27,Th33;
then consider q being object such that
A28: q in L~f and
A29: q in L~m by XBOOLE_0:3;
reconsider q as Point of TOP-REAL 2 by A29;
consider i such that
A30: 1 <= i and
A31: i+1 <= len m and
A32: q in LSeg(m,i) by A29,SPPOL_2:13;
set j = i+(inw+1)-'1;
A33: j = i+inw+1-'1 .= i+inw by NAT_D:34;
A34: len m = len g-'(inw+1)+1 by A13,A7,FINSEQ_6:186;
then len m = len g -' inw by A9,JORDAN3:8,NAT_2:7;
then len m + inw = len g by A12,XREAL_1:235;
then i+1 + inw <= len g by A31,XREAL_1:6;
then
A35: j + 1 <= len g by A33;
i < len m by A31,NAT_1:13;
then
A36: LSeg(m,i)=LSeg(g,i+(inw+1)-'1) by A7,A26,A30,A34,JORDAN4:19;
A37: j >= inw+1 by A30,A33,XREAL_1:6;
A38: now
assume nw = q;
then
A39: nw in LSeg(g,inw) /\ LSeg(g,j) by A11,A32,A36,XBOOLE_0:def 4;
then
A40: LSeg(g,inw) meets LSeg(g,j);
per cases by A37,XXREAL_0:1;
suppose
A41: inw+1 = j;
inw+1+1 <= len g by A26,NAT_1:13;
then inw + (1+1) <= len g;
then LSeg(g,inw) /\ LSeg(g,inw+1) = {g/.(inw+1)} by A10,
TOPREAL1:def 6;
hence contradiction by A18,A39,A41,TARSKI:def 1;
end;
suppose
inw+1 < j;
hence contradiction by A40,TOPREAL1:def 7;
end;
end;
0+1 <= j by A30,A33,XREAL_1:7;
then inw >= j by A3,A4,A10,A13,A11,A28,A32,A36,A35,A38,JORDAN5C:28;
then inw >= inw+1 by A37,XXREAL_0:2;
hence contradiction by XREAL_1:29;
end;
end;
nw in L~f by A8,XBOOLE_0:def 4;
then nw <> g.len g by A2,A15,A6,XBOOLE_0:3;
then
A42: inw+1 < len g by A13,A16,XXREAL_0:1;
then
A43: inw+1+1 <= len g by NAT_1:13;
then g/.(inw+1) in LSeg(g,inw+1) by A7,TOPREAL1:21;
then
A44: nw in LSeg(g,inw+1) by A14,A16,PARTFUN1:def 6;
A45: 1 <= inw+1+1 by NAT_1:11;
then
A46: len g >= 1 by A43,XXREAL_0:2;
A47: inw+1+1 in dom g by A43,A45,FINSEQ_3:25;
inw+1 < inw+1+1 by NAT_1:13;
then
A48: nw <> g.(inw+1+1) by A14,A16,A47,FUNCT_1:def 4;
then
A49: nw <> g/.(inw+1+1) by A47,PARTFUN1:def 6;
per cases;
suppose
A50: g/.(inw+1+1) in L~f;
A51: nw <> g/.(inw+1+1) by A47,A48,PARTFUN1:def 6;
inw+1+1 <> len g by A2,A15,A50,XBOOLE_0:3;
then inw+1+1 < len g by A43,XXREAL_0:1;
then
A52: inw+1+1+1 <= len g by NAT_1:13;
then g/.(inw+1+1) in LSeg(g,inw+1+1) by A45,TOPREAL1:21;
then inw+1 >= inw+1+1 by A3,A4,A7,A43,A45,A44,A50,A52,A51,JORDAN5C:28;
hence contradiction by XREAL_1:29;
end;
suppose
A53: not g/.(inw+1+1) in L~f;
A54: now
assume
A55: g/.(inw+1+1) in RightComp 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} by Th37;
then
A56: 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 A55;
A57: LSeg(g,inw+1) is vertical or LSeg(g,inw+1) is horizontal by SPPOL_1:19;
LSeg(g,inw+1) = LSeg(g/.(inw+1),g/.(inw+1+1)) by A7,A43,TOPREAL1:def 3;
then (g/.(inw+1+1))`1 = nw`1 or (g/.(inw+1+1))`2 = nw`2 by A44,A57,
SPPOL_1:40,41;
hence contradiction by A56,EUCLID:52;
end;
then reconsider
m = mid(g,inw+1+1,len g) as S-Sequence_in_R2 by A2,A43,A45,A46,JORDAN3:6;
A58: inw+1+1<len g by A2,A43,A54,XXREAL_0:1;
g/.(inw+1+1) in (L~f)` by A53,SUBSET_1:29;
then g/.(inw+1+1) in LeftComp f \/ RightComp f by GOBRD12:10;
then g/.(inw+1+1) in LeftComp f by A54,XBOOLE_0:def 3;
then
A59: m/.1 in LeftComp f by A5,A47,SPRECT_2:8;
m/.len m in RightComp f by A2,A5,A47,SPRECT_2:9;
then L~f meets L~m by A59,Th33;
then consider q being object such that
A60: q in L~f and
A61: q in L~m by XBOOLE_0:3;
reconsider q as Point of TOP-REAL 2 by A61;
consider i such that
A62: 1 <= i and
A63: i+1 <= len m and
A64: q in LSeg(m,i) by A61,SPPOL_2:13;
set j = i+(inw+1+1)-'1;
A65: len m = len g-'(inw+1+1)+1 by A43,A45,FINSEQ_6:186;
then len m = len g -' (inw+1) by A42,NAT_2:7;
then len m + (inw+1) = len g by A13,XREAL_1:235;
then i+ 1 + (inw +1) <= len g by A63,XREAL_1:6;
then
A66: i+ 1 + inw +1 <= len g;
i < len m by A63,NAT_1:13;
then
A67: LSeg(m,i)=LSeg(g,i+(inw+1+1)-'1) by A45,A58,A62,A65,JORDAN4:19;
A68: j = i+inw+1+1-'1 .= i+inw+1 by NAT_D:34;
then j = i+(inw+1);
then
A69: j >= inw+1+1 by A62,XREAL_1:6;
A70: now
assume nw = q;
then
A71: nw in LSeg(g,inw+1) /\ LSeg(g,j) by A44,A64,A67,XBOOLE_0:def 4;
then
A72: LSeg(g,inw+1) meets LSeg(g,j);
per cases by A69,XXREAL_0:1;
suppose
A73: inw+1+1 = j;
inw+1+1+1 <= len g by A58,NAT_1:13;
then inw+1 + (1+1) <= len g;
then LSeg(g,inw+1) /\ LSeg(g,inw+1+1) = {g/.(inw+1+1)} by A7,
TOPREAL1:def 6;
hence contradiction by A49,A71,A73,TARSKI:def 1;
end;
suppose
inw+1+1 < j;
hence contradiction by A72,TOPREAL1:def 7;
end;
end;
0+1 <= j by A68,NAT_1:11;
then inw+1 >= j by A3,A4,A7,A43,A44,A60,A64,A67,A68,A66,A70,JORDAN5C:28;
then inw+1 >= inw+1+1 by A69,XXREAL_0:2;
hence contradiction by XREAL_1:29;
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) <> 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,Th33;
assume
A4: Last_Point(L~g,g/.1,g/.len g,L~f) = SE-corner L~f;
set se = SE-corner L~f, ise = Index(se,g);
A5: len g in dom g by FINSEQ_5:6;
then
A6: g.len g = g/.len g by PARTFUN1:def 6;
A7: 1 <= ise+1 by NAT_1:11;
L~g is_an_arc_of g/.1, g/.len g by TOPREAL1:25;
then
A8: se in L~g /\ L~f by A3,A4,JORDAN5C:def 2;
then
A9: se in L~g by XBOOLE_0:def 4;
then
A10: 1 <= ise by JORDAN3:8;
A11: se in LSeg(g,ise) by A9,JORDAN3:9;
A12: ise < len g by A9,JORDAN3:8;
then
A13: ise+1 <= len g by NAT_1:13;
then
A14: ise+1 in dom g by A7,FINSEQ_3:25;
A15: L~f misses RightComp f by Th25;
A16: now
A17: len g >= 1 by A13,A7,XXREAL_0:2;
assume se <> g.(ise+1);
then
A18: se <> g/.(ise+1) by A14,PARTFUN1:def 6;
per cases;
suppose
A19: g/.(ise+1) in L~f;
then ise+1 <> len g by A2,A15,XBOOLE_0:3;
then ise+1 < len g by A13,XXREAL_0:1;
then
A20: ise+1+1 <= len g by NAT_1:13;
then g/.(ise+1) in LSeg(g,ise+1) by A7,TOPREAL1:21;
then ise >= ise+1 by A3,A4,A10,A13,A11,A7,A18,A19,A20,JORDAN5C:28;
hence contradiction by XREAL_1:29;
end;
suppose
A21: not g/.(ise+1) in L~f;
A22: now
assume
A23: g/.(ise+1) in RightComp 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} by Th37;
then
A24: 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 A23;
A25: LSeg(g,ise) is vertical or LSeg(g,ise) is horizontal by SPPOL_1:19;
LSeg(g,ise) = LSeg(g/.ise,g/.(ise+1)) by A10,A13,TOPREAL1:def 3;
then (g/.(ise+1))`1 = se`1 or (g/.(ise+1))`2 = se`2 by A11,A25,
SPPOL_1:40,41;
hence contradiction by A24,EUCLID:52;
end;
then reconsider
m = mid(g,ise+1,len g) as S-Sequence_in_R2 by A2,A13,A7,A17,JORDAN3:6;
A26: ise+1<len g by A2,A13,A22,XXREAL_0:1;
g/.(ise+1) in (L~f)` by A21,SUBSET_1:29;
then g/.(ise+1) in LeftComp f \/ RightComp f by GOBRD12:10;
then g/.(ise+1) in LeftComp f by A22,XBOOLE_0:def 3;
then
A27: m/.1 in LeftComp f by A5,A14,SPRECT_2:8;
m/.len m in RightComp f by A2,A5,A14,SPRECT_2:9;
then L~f meets L~m by A27,Th33;
then consider q being object such that
A28: q in L~f and
A29: q in L~m by XBOOLE_0:3;
reconsider q as Point of TOP-REAL 2 by A29;
consider i such that
A30: 1 <= i and
A31: i+1 <= len m and
A32: q in LSeg(m,i) by A29,SPPOL_2:13;
set j = i+(ise+1)-'1;
A33: j = i+ise+1-'1 .= i+ise by NAT_D:34;
A34: len m = len g-'(ise+1)+1 by A13,A7,FINSEQ_6:186;
then len m = len g -' ise by A9,JORDAN3:8,NAT_2:7;
then len m + ise = len g by A12,XREAL_1:235;
then i+1 + ise <= len g by A31,XREAL_1:6;
then
A35: j + 1 <= len g by A33;
i < len m by A31,NAT_1:13;
then
A36: LSeg(m,i)=LSeg(g,i+(ise+1)-'1) by A7,A26,A30,A34,JORDAN4:19;
A37: j >= ise+1 by A30,A33,XREAL_1:6;
A38: now
assume se = q;
then
A39: se in LSeg(g,ise) /\ LSeg(g,j) by A11,A32,A36,XBOOLE_0:def 4;
then
A40: LSeg(g,ise) meets LSeg(g,j);
per cases by A37,XXREAL_0:1;
suppose
A41: ise+1 = j;
ise+1+1 <= len g by A26,NAT_1:13;
then ise + (1+1) <= len g;
then LSeg(g,ise) /\ LSeg(g,ise+1) = {g/.(ise+1)} by A10,
TOPREAL1:def 6;
hence contradiction by A18,A39,A41,TARSKI:def 1;
end;
suppose
ise+1 < j;
hence contradiction by A40,TOPREAL1:def 7;
end;
end;
0+1 <= j by A30,A33,XREAL_1:7;
then ise >= j by A3,A4,A10,A13,A11,A28,A32,A36,A35,A38,JORDAN5C:28;
then ise >= ise+1 by A37,XXREAL_0:2;
hence contradiction by XREAL_1:29;
end;
end;
se in L~f by A8,XBOOLE_0:def 4;
then se <> g.len g by A2,A15,A6,XBOOLE_0:3;
then
A42: ise+1 < len g by A13,A16,XXREAL_0:1;
then
A43: ise+1+1 <= len g by NAT_1:13;
then g/.(ise+1) in LSeg(g,ise+1) by A7,TOPREAL1:21;
then
A44: se in LSeg(g,ise+1) by A14,A16,PARTFUN1:def 6;
A45: 1 <= ise+1+1 by NAT_1:11;
then
A46: len g >= 1 by A43,XXREAL_0:2;
A47: ise+1+1 in dom g by A43,A45,FINSEQ_3:25;
ise+1 < ise+1+1 by NAT_1:13;
then
A48: se <> g.(ise+1+1) by A14,A16,A47,FUNCT_1:def 4;
then
A49: se <> g/.(ise+1+1) by A47,PARTFUN1:def 6;
per cases;
suppose
A50: g/.(ise+1+1) in L~f;
A51: se <> g/.(ise+1+1) by A47,A48,PARTFUN1:def 6;
ise+1+1 <> len g by A2,A15,A50,XBOOLE_0:3;
then ise+1+1 < len g by A43,XXREAL_0:1;
then
A52: ise+1+1+1 <= len g by NAT_1:13;
then g/.(ise+1+1) in LSeg(g,ise+1+1) by A45,TOPREAL1:21;
then ise+1 >= ise+1+1 by A3,A4,A7,A43,A45,A44,A50,A52,A51,JORDAN5C:28;
hence contradiction by XREAL_1:29;
end;
suppose
A53: not g/.(ise+1+1) in L~f;
A54: now
assume
A55: g/.(ise+1+1) in RightComp 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} by Th37;
then
A56: 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 A55;
A57: LSeg(g,ise+1) is vertical or LSeg(g,ise+1) is horizontal by SPPOL_1:19;
LSeg(g,ise+1) = LSeg(g/.(ise+1),g/.(ise+1+1)) by A7,A43,TOPREAL1:def 3;
then (g/.(ise+1+1))`1 = se`1 or (g/.(ise+1+1))`2 = se`2 by A44,A57,
SPPOL_1:40,41;
hence contradiction by A56,EUCLID:52;
end;
then reconsider
m = mid(g,ise+1+1,len g) as S-Sequence_in_R2 by A2,A43,A45,A46,JORDAN3:6;
A58: ise+1+1<len g by A2,A43,A54,XXREAL_0:1;
g/.(ise+1+1) in (L~f)` by A53,SUBSET_1:29;
then g/.(ise+1+1) in LeftComp f \/ RightComp f by GOBRD12:10;
then g/.(ise+1+1) in LeftComp f by A54,XBOOLE_0:def 3;
then
A59: m/.1 in LeftComp f by A5,A47,SPRECT_2:8;
m/.len m in RightComp f by A2,A5,A47,SPRECT_2:9;
then L~f meets L~m by A59,Th33;
then consider q being object such that
A60: q in L~f and
A61: q in L~m by XBOOLE_0:3;
reconsider q as Point of TOP-REAL 2 by A61;
consider i such that
A62: 1 <= i and
A63: i+1 <= len m and
A64: q in LSeg(m,i) by A61,SPPOL_2:13;
set j = i+(ise+1+1)-'1;
A65: len m = len g-'(ise+1+1)+1 by A43,A45,FINSEQ_6:186;
then len m = len g -' (ise+1) by A42,NAT_2:7;
then len m + (ise+1) = len g by A13,XREAL_1:235;
then i+ 1 + (ise +1) <= len g by A63,XREAL_1:6;
then
A66: i+ 1 + ise +1 <= len g;
i < len m by A63,NAT_1:13;
then
A67: LSeg(m,i)=LSeg(g,i+(ise+1+1)-'1) by A45,A58,A62,A65,JORDAN4:19;
A68: j = i+ise+1+1-'1 .= i+ise+1 by NAT_D:34;
then j = i+(ise+1);
then
A69: j >= ise+1+1 by A62,XREAL_1:6;
A70: now
assume se = q;
then
A71: se in LSeg(g,ise+1) /\ LSeg(g,j) by A44,A64,A67,XBOOLE_0:def 4;
then
A72: LSeg(g,ise+1) meets LSeg(g,j);
per cases by A69,XXREAL_0:1;
suppose
A73: ise+1+1 = j;
ise+1+1+1 <= len g by A58,NAT_1:13;
then ise+1 + (1+1) <= len g;
then LSeg(g,ise+1) /\ LSeg(g,ise+1+1) = {g/.(ise+1+1)} by A7,
TOPREAL1:def 6;
hence contradiction by A49,A71,A73,TARSKI:def 1;
end;
suppose
ise+1+1 < j;
hence contradiction by A72,TOPREAL1:def 7;
end;
end;
0+1 <= j by A68,NAT_1:11;
then ise+1 >= j by A3,A4,A7,A43,A44,A60,A64,A67,A68,A66,A70,JORDAN5C:28;
then ise+1 >= ise+1+1 by A69,XXREAL_0:2;
hence contradiction by XREAL_1:29;
end;
end;
theorem Th40:
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 Th37;
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;
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 DOMAIN_1:sch 7;
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 DOMAIN_1:sch 7;
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 DOMAIN_1:sch 7;
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 DOMAIN_1:sch 7;
A2: W-bound L~SpStSeq L~f = W-bound L~f by SPRECT_1:58;
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 thesis by JORDAN5D:40;
end;
then
A3: P2 misses L~f by GOBOARD8:24;
A4: 1+1 <= len f by GOBOARD7:34,XXREAL_0:2;
A5: width GoB f -' 1 + 1 = width GoB f by GOBRD11:34,XREAL_1:235;
consider i such that
A6: 1 <= i and
A7: i < len GoB f and
A8: N-min L~f = (GoB f)*(i,width GoB f) by Th28;
A9: i+1 <= len GoB f by A7,NAT_1:13;
A10: i in dom GoB f by A6,A7,FINSEQ_3:25;
then
A11: f/.2 = (GoB f)*(i+1,width GoB f) by A1,A8,Th29;
A12: width GoB f >= 1 by GOBRD11:34;
then
A13: [i,width GoB f] in Indices GoB f by A6,A7,MATRIX_0:30;
A14: 1 <= i+1 by A6,NAT_1:13;
then
A15: (f/.2)`2 = ((GoB f)*(1,width GoB f))`2 by A11,A12,A9,GOBOARD5:1
.= (N-min L~f)`2 by A6,A7,A8,A12,GOBOARD5:1
.= N-bound L~f by EUCLID:52;
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`2 = q`2+|[0,1]|`2 by TOPREAL3:2
.= q`2+1 by EUCLID:52;
q`2 = (1/2*((GoB f)*(i,width GoB f)+f/.2))`2 by A1,A8,A10,Th29
.= 1/2*(f/.1+f/.2)`2 by A1,A8,TOPREAL3:4
.= 1/2*((f/.1)`2+(f/.2)`2) by TOPREAL3:2
.= 1/2*(N-bound L~f+N-bound L~f) by A1,A15,EUCLID:52
.= N-bound L~f;
then a`2 > 0 + N-bound L~f by A16,XREAL_1:8;
then
A17: a`2 > N-bound L~SpStSeq L~f by SPRECT_1:60;
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 Th37;
then
A18: a in LeftComp SpStSeq L~f by A17;
[i+1,width GoB f] in Indices GoB f by A12,A14,A9,MATRIX_0:30;
then left_cell(f,1) = cell(GoB f,i,width GoB f) by A1,A8,A11,A5,A4,A13,
GOBOARD5:28;
then
A19: Int cell(GoB f,i,width GoB f) c= LeftComp f by GOBOARD9:def 1;
a in Int cell(GoB f,i,width GoB f) by A6,A9,GOBOARD6:32;
then
A20: LeftComp f meets LeftComp SpStSeq L~f by A19,A18,XBOOLE_0:3;
A21: S-bound L~SpStSeq L~f = S-bound L~f by SPRECT_1:59;
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 thesis by JORDAN5D:37;
end;
then
A22: P4 misses L~f by GOBOARD8:21;
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 thesis by JORDAN5D:39;
end;
then P3 misses L~f by GOBOARD8:22;
then
A23: P3 \/ P4 misses L~f by A22,XBOOLE_1:70;
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
A24: B1 = LeftComp SpStSeq L~f and
A25: B1 is a_component by CONNSP_1:def 6;
B1 is connected by A25,CONNSP_1:def 5;
then
A26: LeftComp SpStSeq L~f is connected by A24,CONNSP_1:23;
A27: E-bound L~SpStSeq L~f = E-bound L~f by SPRECT_1:61;
A28: N-bound L~SpStSeq L~f = N-bound L~f by SPRECT_1:60;
A29: LeftComp SpStSeq L~f = P1 \/ P2 \/ (P3 \/ P4)
proof
thus LeftComp SpStSeq L~f c= P1 \/ P2 \/ (P3 \/ P4)
proof
let x be object;
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 A28,A2,A21,A27,Th37;
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 3;
hence thesis by XBOOLE_0:def 3;
end;
let x be object;
assume x in P1 \/ P2 \/ (P3 \/ P4);
then
A30: x in P1 \/ P2 or x in P3 \/ P4 by XBOOLE_0:def 3;
per cases by A30,XBOOLE_0:def 3;
suppose
x in P1;
then ex p st x = p & p`2 < S-bound L~f;
hence thesis by A21,Th40;
end;
suppose
x in P2;
then ex p st x = p & p`2 > N-bound L~f;
hence thesis by A28,Th40;
end;
suppose
x in P3;
then ex p st x = p & p`1 > E-bound L~f;
hence thesis by A27,Th40;
end;
suppose
x in P4;
then ex p st x = p & p`1 < W-bound L~f;
hence thesis by A2,Th40;
end;
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 thesis by JORDAN5D:38;
end;
then P1 misses L~f by GOBOARD8:23;
then P1 \/ P2 misses L~f by A3,XBOOLE_1:70;
then LeftComp SpStSeq L~f misses L~f by A29,A23,XBOOLE_1:70;
then
A31: LeftComp SpStSeq L~f c= (L~f)` by SUBSET_1:23;
LeftComp f is_a_component_of (L~f)` by GOBOARD9:def 1;
hence thesis by A26,A20,A31,GOBOARD9:4;
end;
begin :: In the area
theorem Th42:
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
A1: dom<*p,q*> = {1,2} by FINSEQ_1:2,89;
then
A2: 1 in dom<*p,q*> by TARSKI:def 2;
assume
A3: <*p,q*> is_in_the_area_of f;
A4: <*p,q*>/.1 = p by FINSEQ_4:17;
then
A5: p`1 <= E-bound L~f by A3,A2;
A6: p`2 <= N-bound L~f by A3,A2,A4;
A7: S-bound L~f <= p`2 by A3,A2,A4;
A8: W-bound L~f <= p`1 by A3,A2,A4;
thus <*p*> is_in_the_area_of f
proof
let i;
assume i in dom<*p*>;
then i in {1} by FINSEQ_1:2,38;
then i = 1 by TARSKI:def 1;
hence thesis by A8,A5,A7,A6,FINSEQ_4:16;
end;
let i;
assume i in dom<*q*>;
then i in {1} by FINSEQ_1:2,38;
then
A9: i = 1 by TARSKI:def 1;
A10: <*p,q*>/.2 = q by FINSEQ_4:17;
A11: 2 in dom<*p,q*> by A1,TARSKI:def 2;
then
A12: q`1 <= E-bound L~f by A3,A10;
A13: q`2 <= N-bound L~f by A3,A11,A10;
A14: S-bound L~f <= q`2 by A3,A11,A10;
W-bound L~f <= q`1 by A3,A11,A10;
hence thesis by A12,A14,A13,A9,FINSEQ_4:16;
end;
A15: <*p*>/.1 = p by FINSEQ_4:16;
dom<*q*> = {1} by FINSEQ_1:2,38;
then
A16: 1 in dom<*q*> by TARSKI:def 1;
dom<*p*> = {1} by FINSEQ_1:2,38;
then
A17: 1 in dom<*p*> by TARSKI:def 1;
assume
A18: <*p*> is_in_the_area_of f;
then
A19: p`1 <= E-bound L~f by A17,A15;
A20: p`2 <= N-bound L~f by A18,A17,A15;
A21: S-bound L~f <= p`2 by A18,A17,A15;
A22: <*q*>/.1 = q by FINSEQ_4:16;
assume
A23: <*q*> is_in_the_area_of f;
then
A24: W-bound L~f <= q`1 by A16,A22;
A25: q`1 <= E-bound L~f by A23,A16,A22;
let i;
assume i in dom<*p,q*>;
then i in {1,2} by FINSEQ_1:2,89;
then
A26: i =1 or i =2 by TARSKI:def 2;
A27: q`2 <= N-bound L~f by A23,A16,A22;
A28: S-bound L~f <= q`2 by A23,A16,A22;
W-bound L~f <= p`1 by A18,A17,A15;
hence thesis by A19,A21,A20,A24,A25,A28,A27,A26,FINSEQ_4:17;
end;
theorem Th43:
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;
A1: <*p*>/.1 = p by FINSEQ_4:16;
dom<*p*> = {1} by FINSEQ_1:2,38;
then
A2: 1 in dom<*p*> by TARSKI:def 1;
assume
A3: <*p*> is_in_the_area_of f;
then
A4: W-bound L~f <= p`1 by A2,A1;
A5: p`2 <= N-bound L~f by A3,A2,A1;
A6: S-bound L~f <= p`2 by A3,A2,A1;
A7: p`1 <= E-bound L~f by A3,A2,A1;
consider D being non vertical non horizontal non empty compact Subset of
TOP-REAL 2 such that
A8: f = SpStSeq D by SPRECT_1:def 2;
A9: E-bound L~SpStSeq D = E-bound D by SPRECT_1:61;
A10: N-bound L~SpStSeq D = N-bound D by SPRECT_1:60;
A11: S-bound L~SpStSeq D = S-bound D by SPRECT_1:59;
A12: W-bound L~SpStSeq D = W-bound D by SPRECT_1:58;
A13: 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 A8,
SPRECT_1:41;
assume
A14: 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 A14;
suppose
A15: p`1 = W-bound L~f;
A16: (NW-corner D)`1 = W-bound D by EUCLID:52;
A17: (NW-corner D)`2 = N-bound D by EUCLID:52;
A18: (SW-corner D)`2 = S-bound D by EUCLID:52;
(SW-corner D)`1 = W-bound D by EUCLID:52;
then p in LSeg(SW-corner D,NW-corner D) by A6,A5,A8,A12,A11,A10,A15,A16,A18
,A17,GOBOARD7:7;
then p in LSeg(SE-corner D,SW-corner D) \/ LSeg(SW-corner D,NW-corner D)
by XBOOLE_0:def 3;
hence thesis by A13,XBOOLE_0:def 3;
end;
suppose
A19: p`1 = E-bound L~f;
A20: (SE-corner D)`1 = E-bound D by EUCLID:52;
A21: (SE-corner D)`2 = S-bound D by EUCLID:52;
A22: (NE-corner D)`2 = N-bound D by EUCLID:52;
(NE-corner D)`1 = E-bound D by EUCLID:52;
then p in LSeg(NE-corner D,SE-corner D) by A6,A5,A8,A11,A10,A9,A19,A20,A22
,A21,GOBOARD7:7;
then p in LSeg(NW-corner D,NE-corner D) \/ LSeg(NE-corner D,SE-corner D)
by XBOOLE_0:def 3;
hence thesis by A13,XBOOLE_0:def 3;
end;
suppose
A23: p`2 = S-bound L~f;
A24: (SW-corner D)`1 = W-bound D by EUCLID:52;
A25: (SW-corner D)`2 = S-bound D by EUCLID:52;
A26: (SE-corner D)`2 = S-bound D by EUCLID:52;
(SE-corner D)`1 = E-bound D by EUCLID:52;
then p in LSeg(SE-corner D,SW-corner D) by A4,A7,A8,A12,A11,A9,A23,A24,A26
,A25,GOBOARD7:8;
then p in LSeg(SE-corner D,SW-corner D) \/ LSeg(SW-corner D,NW-corner D)
by XBOOLE_0:def 3;
hence thesis by A13,XBOOLE_0:def 3;
end;
suppose
A27: p`2 = N-bound L~f;
A28: (NE-corner D)`1 = E-bound D by EUCLID:52;
A29: (NE-corner D)`2 = N-bound D by EUCLID:52;
A30: (NW-corner D)`2 = N-bound D by EUCLID:52;
(NW-corner D)`1 = W-bound D by EUCLID:52;
then p in LSeg(NW-corner D,NE-corner D) by A4,A7,A8,A12,A10,A9,A27,A28,A30
,A29,GOBOARD7:8;
then p in LSeg(NW-corner D,NE-corner D) \/ LSeg(NE-corner D,SE-corner D)
by XBOOLE_0:def 3;
hence thesis by A13,XBOOLE_0:def 3;
end;
end;
theorem Th44:
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;
A4: dom<*p,q*> = {1,2} by FINSEQ_1:2,89;
then
A5: 2 in dom<*p,q*> by TARSKI:def 2;
A6: <*p,q*>/.2 = q by FINSEQ_4:17;
then W-bound L~f <= q`1 by A3,A5;
then
A7: r*W-bound L~f <= r*q`1 by A1,XREAL_1:64;
q`1 <= E-bound L~f by A3,A5,A6;
then
A8: r*q`1<= r*E-bound L~f by A1,XREAL_1:64;
A9: <*p,q*>/.1 = p by FINSEQ_4:17;
A10: 1-r >= 0 by A2,XREAL_1:48;
A11: 1 in dom<*p,q*> by A4,TARSKI:def 2;
then W-bound L~f <= p`1 by A3,A9;
then
A12: (1-r)*W-bound L~f <= (1-r)*p`1 by A10,XREAL_1:64;
p`1 <= E-bound L~f by A3,A11,A9;
then
A13: (1-r)*p`1 <= (1-r)*E-bound L~f by A10,XREAL_1:64;
S-bound L~f <= p`2 by A3,A11,A9;
then
A14: (1-r)*S-bound L~f <= (1-r)*p`2 by A10,XREAL_1:64;
A15: ((1-r)*p+r*q)`1 = ((1-r)*p)`1+(r*q)`1 by TOPREAL3:2
.= (1-r)*p`1+(r*q)`1 by TOPREAL3:4
.= (1-r)*p`1+r*q`1 by TOPREAL3:4;
p`2 <= N-bound L~f by A3,A11,A9;
then
A16: (1-r)*p`2 <= (1-r)*N-bound L~f by A10,XREAL_1:64;
let n;
A17: dom <*(1-r)*p+r*q*> = {1} by FINSEQ_1:2,38;
assume n in dom <*(1-r)*p+r*q*>;
then
A18: n = 1 by A17,TARSKI:def 1;
(1-r)*W-bound L~f+r*W-bound L~f = 1*W-bound L~f;
then W-bound L~f <= (1-r)*p`1+r*q`1 by A7,A12,XREAL_1:7;
hence W-bound L~f <= (<*(1-r)*p+r*q*>/.n)`1 by A18,A15,FINSEQ_4:16;
(1-r)*E-bound L~f+r*E-bound L~f = 1*E-bound L~f;
then (1-r)*p`1+r*q`1 <= E-bound L~f by A8,A13,XREAL_1:7;
hence (<*(1-r)*p+r*q*>/.n)`1 <= E-bound L~f by A18,A15,FINSEQ_4:16;
A19: ((1-r)*p+r*q)`2 = ((1-r)*p)`2+(r*q)`2 by TOPREAL3:2
.= (1-r)*p`2+(r*q)`2 by TOPREAL3:4
.= (1-r)*p`2+r*q`2 by TOPREAL3:4;
q`2 <= N-bound L~f by A3,A5,A6;
then
A20: r*q`2<= r*N-bound L~f by A1,XREAL_1:64;
S-bound L~f <= q`2 by A3,A5,A6;
then
A21: r*S-bound L~f <= r*q`2 by A1,XREAL_1:64;
(1-r)*S-bound L~f+r*S-bound L~f = 1*S-bound L~f;
then S-bound L~f <= (1-r)*p`2+r*q`2 by A21,A14,XREAL_1:7;
hence S-bound L~f <= (<*(1-r)*p+r*q*>/.n)`2 by A18,A19,FINSEQ_4:16;
(1-r)*N-bound L~f+r*N-bound L~f = 1*N-bound L~f;
then (1-r)*p`2+r*q`2 <= N-bound L~f by A20,A16,XREAL_1:7;
hence thesis by A18,A19,FINSEQ_4:16;
end;
theorem Th45:
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;
A3: dom <*g/.i*> = {1} by FINSEQ_1:2,38;
assume n in dom <*g/.i*>;
then n = 1 by A3,TARSKI:def 1;
then <*g/.i*>/.n = g/.i by FINSEQ_4:16;
hence thesis by A1,A2;
end;
theorem Th46:
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;
A5: ex r being Real st p = (1-r)*g/.i+r*g/.(i+1) & 0<=r & r<=1 by A4;
i <= i+1 by NAT_1:11;
then i <= len g by A3,XXREAL_0:2;
then i in dom g by A2,FINSEQ_3:25;
then
A6: <*g/.i*> is_in_the_area_of f by A1,Th45;
1 <= i+1 by NAT_1:11;
then i+1 in dom g by A3,FINSEQ_3:25;
then <*g/.(i+1)*> is_in_the_area_of f by A1,Th45;
then <*g/.i,g/.(i+1)*> is_in_the_area_of f by A6,Th42;
hence thesis by A5,Th44;
end;
theorem Th47:
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;
A3: dom <*p,q*> = {1,2} by FINSEQ_1:2,89;
then
A4: 2 in dom <*p,q*> by TARSKI:def 2;
A5: <*p,q*>/.2 = q by FINSEQ_4:17;
then
A6: W-bound L~f <= q`1 by A2,A4;
A7: <*q*> is_in_the_area_of f by A2,Th42;
then q`1 <> W-bound L~f by A1,Th43;
then
A8: W-bound L~f < q`1 by A6,XXREAL_0:1;
A9: q`2 <= N-bound L~f by A2,A4,A5;
q`2 <> N-bound L~f by A1,A7,Th43;
then
A10: q`2 < N-bound L~f by A9,XXREAL_0:1;
let x be object;
A11: <*p,q*>/.1 = p by FINSEQ_4:17;
A12: q`1 <= E-bound L~f by A2,A4,A5;
q`1 <> E-bound L~f by A1,A7,Th43;
then
A13: q`1 < E-bound L~f by A12,XXREAL_0:1;
assume
A14: x in LSeg(p,q) /\ L~f;
then reconsider p9 = x as Point of TOP-REAL 2;
A15: p9 in L~f by A14,XBOOLE_0:def 4;
A16: 1 in dom <*p,q*> by A3,TARSKI:def 2;
then
A17: W-bound L~f <= p`1 by A2,A11;
A18: p`2 <= N-bound L~f by A2,A16,A11;
A19: S-bound L~f <= p`2 by A2,A16,A11;
A20: p`1 <= E-bound L~f by A2,A16,A11;
A21: S-bound L~f <= q`2 by A2,A4,A5;
q`2 <> S-bound L~f by A1,A7,Th43;
then
A22: S-bound L~f < q`2 by A21,XXREAL_0:1;
x in LSeg(p,q) by A14,XBOOLE_0:def 4;
then consider r being Real such that
A23: p9 = (1-r)*p+r*q and
A24: 0<=r and
A25: r<=1;
A26: p9`1 = ((1-r)*p)`1+(r*q)`1 by A23,TOPREAL3:2
.= (1-r)*p`1+(r*q)`1 by TOPREAL3:4
.= (1-r)*p`1+r*q`1 by TOPREAL3:4;
A27: p9`2 = ((1-r)*p)`2+(r*q)`2 by A23,TOPREAL3:2
.= (1-r)*p`2+(r*q)`2 by TOPREAL3:4
.= (1-r)*p`2+r*q`2 by TOPREAL3:4;
per cases by A15,Th32;
suppose
p9`1 = W-bound L~f;
then r = 0 by A17,A8,A24,A25,A26,XREAL_1:180;
then p9 = 1*p+0.TOP-REAL 2 by A23,RLVECT_1:10
.= 1*p by RLVECT_1:4
.= p by RLVECT_1:def 8;
hence thesis by ZFMISC_1:31;
end;
suppose
p9`1 = E-bound L~f;
then r = 0 by A20,A13,A24,A25,A26,XREAL_1:179;
then p9 = 1*p+0.TOP-REAL 2 by A23,RLVECT_1:10
.= 1*p by RLVECT_1:4
.= p by RLVECT_1:def 8;
hence thesis by ZFMISC_1:31;
end;
suppose
p9`2 = S-bound L~f;
then r = 0 by A19,A22,A24,A25,A27,XREAL_1:180;
then p9 = 1*p+0.TOP-REAL 2 by A23,RLVECT_1:10
.= 1*p by RLVECT_1:4
.= p by RLVECT_1:def 8;
hence thesis by ZFMISC_1:31;
end;
suppose
p9`2 = N-bound L~f;
then r = 0 by A18,A10,A24,A25,A27,XREAL_1:179;
then p9 = 1*p+0.TOP-REAL 2 by A23,RLVECT_1:10
.= 1*p by RLVECT_1:4
.= p by RLVECT_1:def 8;
hence thesis by ZFMISC_1:31;
end;
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;
A4: <*p,q*> = <*p*>^<*q*> by FINSEQ_1:def 9;
<*p*> is_in_the_area_of f by A1,Th46,SPRECT_2:21;
hence LSeg(p,q) /\ L~f c= {p} by A2,A3,A4,Th47,SPRECT_2:24;
p in LSeg(p,q) by RLTOPSP1:68;
then p in LSeg(p,q) /\ L~f by A1,XBOOLE_0:def 4;
hence thesis by ZFMISC_1:31;
end;
theorem Th49:
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 and
A2: i <= len GoB f and
A3: 1 <= j and
A4: j <= width GoB f;
set G = GoB f;
A5: 1 <= width G by A3,A4,XXREAL_0:2;
A6: 1 <= len G by A1,A2,XXREAL_0:2;
A7: N-bound L~f = (G)*(1,width G)`2 by JORDAN5D:40
.= (G)*(i,width G)`2 by A1,A2,A5,GOBOARD5:1;
A8: j = 1 or j > 1 by A3,XXREAL_0:1;
A9: S-bound L~f = (G)*(1,1)`2 by JORDAN5D:38
.= (G)*(i,1)`2 by A1,A2,A5,GOBOARD5:1;
A10: i = 1 or i > 1 by A1,XXREAL_0:1;
A11: E-bound L~f = (G)*(len G,1)`1 by JORDAN5D:39
.= (G)*(len G,j)`1 by A3,A4,A6,GOBOARD5:2;
A12: j = width G or j < width G by A4,XXREAL_0:1;
A13: i = len G or i < len G by A2,XXREAL_0:1;
let n;
set p = (GoB f)*(i,j);
assume n in dom<*(GoB f)*(i,j)*>;
then n in {1} by FINSEQ_1:2,38;
then n = 1 by TARSKI:def 1;
then
A14: <*p*>/.n = p by FINSEQ_4:16;
W-bound L~f = G*(1,1)`1 by JORDAN5D:37
.= G*(1,j)`1 by A3,A4,A6,GOBOARD5:2;
hence thesis by A14,A10,A9,A8,A11,A13,A7,A12,GOBOARD5:3,4;
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 RLVECT_1:def 5;
hence thesis by Th44;
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;
let n such that
A3: n in dom Rev g;
n >= 1 by A3,FINSEQ_3:25;
then
A4: n-1 >= 0 by XREAL_1:48;
set i = len g + 1 -' n;
A5: len Rev g = len g by FINSEQ_5:def 3;
then
A6: n <= len g by A3,FINSEQ_3:25;
then
A7: i = len g -' n + 1 by NAT_D:38;
then i = len g - n + 1 by A6,XREAL_1:233
.= len g - (n-1);
then
A8: i <= len g - 0 by A4,XREAL_1:13;
1 <= i by A7,NAT_1:11;
then
A9: i in dom g by A8,FINSEQ_3:25;
len g <= len g + 1 by NAT_1:11;
then n + i = len g + 1 by A6,XREAL_1:235,XXREAL_0:2;
then (Rev g)/.n = g/.i by A2,A5,A3,FINSEQ_5:66;
hence thesis by A1,A9;
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 being_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 being_S-Seq;
2 <= len g by A3,TOPREAL1:def 8;
then 1 <= len g by XXREAL_0:2;
then
A5: 1 in dom g by FINSEQ_3:25;
assume
A6: p in L~g;
then
A7: Index(p,g) < len g by JORDAN3:8;
1<=Index(p,g) by A6,JORDAN3:8;
then
A8: Index(p,g) in dom g by A7,FINSEQ_3:25;
per cases;
suppose
p<>g.1;
then
A9: R_Cut(g,p) = mid(g,1,Index(p,g))^<*p*> by JORDAN3:def 4;
mid(g,1,Index(p,g)) is_in_the_area_of f by A1,A5,A8,SPRECT_2:22;
hence thesis by A2,A9,SPRECT_2:24;
end;
suppose
p=g.1;
then R_Cut(g,p) = <*g.1*> by JORDAN3:def 4
.= mid(g,1,1) by A5,FINSEQ_6:193;
hence thesis by A1,A5,SPRECT_2:22;
end;
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: S-bound L~SpStSeq L~f = S-bound L~f by SPRECT_1:59;
A2: N-bound L~SpStSeq L~f = N-bound L~f by SPRECT_1:60;
A3: E-bound L~SpStSeq L~f = E-bound L~f by SPRECT_1:61;
A4: W-bound L~SpStSeq L~f = W-bound L~f by SPRECT_1:58;
thus g is_in_the_area_of f implies g is_in_the_area_of SpStSeq L~f
by A4,A1,A2,A3;
assume
A5: g is_in_the_area_of SpStSeq L~f;
let n;
thus thesis by A4,A1,A2,A3,A5;
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;
A3: L~g meets L~f by A1,A2,Th33;
1 in dom g by FINSEQ_5:6;
then
A4: len g >= 1 by FINSEQ_3:25;
set lp = Last_Point(L~g,g/.1,g/.len g,L~f), ilp = Index(lp,g), h = L_Cut(g,
lp);
L~g is_an_arc_of g/.1,g/.len g by TOPREAL1:25;
then
A5: lp in L~g /\ L~f by A3,JORDAN5C:def 2;
then
A6: lp in L~g by XBOOLE_0:def 4;
then
A7: 1 <= ilp by JORDAN3:8;
A8: lp in LSeg(g,ilp) by A6,JORDAN3:9;
A9: ilp < len g by A6,JORDAN3:8;
then
A10: ilp+1<=len g by NAT_1:13;
given n such that
A11: n in dom h and
A12: 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;
A13: 1 <= n by A11,FINSEQ_3:25;
then
A14: ilp+n-'1 = ilp+(n-'1) by NAT_D:38;
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 Th37;
then
A15: h/.n in LeftComp f by A12;
A16: 1<=ilp+1 by NAT_1:11;
then
A17: ilp+1 in dom g by A10,FINSEQ_3:25;
A18: LeftComp f misses RightComp f by SPRECT_1:88;
A19: L~f misses LeftComp f by Th26;
A20: len g in dom g by FINSEQ_5:6;
A21: lp in L~f by A5,XBOOLE_0:def 4;
now
assume
A22: n = 1;
per cases;
suppose
lp <> g.(ilp+1);
then h = <*lp*>^mid(g,ilp+1,len g) by JORDAN3:def 3;
then h/.n = lp by A22,FINSEQ_5:15;
hence contradiction by A19,A21,A15,XBOOLE_0:3;
end;
suppose
A23: lp = g.(ilp+1);
then h = mid(g,ilp+1,len g) by JORDAN3:def 3;
then h/.n = g/.(1+(ilp+1)-'1) by A20,A11,A10,A17,A22,SPRECT_2:3
.= g/.(ilp+1) by NAT_D:34
.= lp by A17,A23,PARTFUN1:def 6;
hence contradiction by A19,A21,A15,XBOOLE_0:3;
end;
end;
then
A24: n > 1 by A13,XXREAL_0:1;
then
A25: 1+1 < ilp+n by A7,XREAL_1:8;
then
A26: 1 <= ilp+n-'1 by NAT_D:49;
set m = mid(g,ilp+n,len g);
A27: len<*lp*> = 1 by FINSEQ_1:39;
A28: n <= len h by A11,FINSEQ_3:25;
then
A29: n+ilp <= len h + ilp by XREAL_1:6;
A30: n = n -'1 +1 by A13,XREAL_1:235;
then
A31: 1 <= n-'1 by A24,NAT_1:13;
A32: len mid(g,ilp+1,len g)=len g-'(ilp+1)+1 by A10,A16,FINSEQ_6:186
.= len g -' ilp by A6,JORDAN3:8,NAT_2:7;
then
A33: ilp + len mid(g,ilp+1,len g) + 1 = len g + 1 by A9,XREAL_1:235;
now
A34: ilp+1 <= ilp+n-'1 by A14,A31,XREAL_1:6;
assume
A35: lp <> g.(ilp+1);
then
A36: h = <*lp*>^mid(g,ilp+1,len g) by JORDAN3:def 3;
then
A37: len h = 1 + len mid(g,ilp+1,len g) by A27,FINSEQ_1:22;
then
A38: ilp+n-'1 <= len g by A33,A29,NAT_D:53;
A39: len h -' 1 = len mid(g,ilp+1,len g) by A37,NAT_D:34;
then n-'1 <= len mid(g,ilp+1,len g) by A28,NAT_D:42;
then
A40: n-'1 in dom mid(g,ilp+1,len g) by A31,FINSEQ_3:25;
h/.n = (mid(g,ilp+1,len g))/.(n-'1) by A28,A30,A27,A31,A36,A39,NAT_D:42
,SEQ_4:136;
then
A41: h/.n = g/.(n-'1+(ilp+1)-'1) by A20,A10,A17,A40,SPRECT_2:3
.= g/.(n+ilp-'1) by A30;
then
A42: ilp+n-'1<>len g by A2,A15,A18,XBOOLE_0:3;
then
A43: ilp+n-'1<len g by A38,XXREAL_0:1;
reconsider m = mid(g,ilp+n-'1,len g) as S-Sequence_in_R2 by A4,A26,A38,A42,
JORDAN3:6;
A44: ilp+n-'1 in dom g by A26,A38,FINSEQ_3:25;
then
A45: m/.len m in RightComp f by A2,A20,SPRECT_2:9;
m/.1 in LeftComp f by A20,A15,A41,A44,SPRECT_2:8;
then L~f meets L~m by A45,Th33;
then consider q being object 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 and
A49: i+1 <= len m and
A50: q in LSeg(m,i) by A47,SPPOL_2:13;
A51: len m = len g-'(ilp+n-'1)+1 by A26,A38,FINSEQ_6:186;
then i <= len g-'(ilp+n-'1) by A49,XREAL_1:6;
then
A52: i+(ilp+n-'1) <= len g by A38,NAT_D:54;
i < len m by A49,NAT_1:13;
then
A53: LSeg(m,i)=LSeg(g,i+(ilp+n-'1)-'1) by A26,A48,A51,A43,JORDAN4:19;
set j = i+(ilp+n-'1)-'1;
i <= i+(ilp+n-'1) by NAT_1:11;
then
A54: j + 1 <= len g by A48,A52,XREAL_1:235,XXREAL_0:2;
j = i-'1+(ilp+n-'1) by A48,NAT_D:38;
then j >= ilp+n-'1 by NAT_1:11;
then
A55: ilp +1 <= j by A34,XXREAL_0:2;
A56: lp <> g/.(ilp+1) by A17,A35,PARTFUN1:def 6;
A57: now
assume lp = q;
then
A58: lp in LSeg(g,ilp) /\ LSeg(g,j) by A8,A50,A53,XBOOLE_0:def 4;
then
A59: LSeg(g,ilp) meets LSeg(g,j);
per cases by A55,XXREAL_0:1;
suppose
A60: ilp+1 = j;
then ilp + (1+1) <= len g by A54;
then LSeg(g,ilp) /\ LSeg(g,ilp+1) = {g/.(ilp+1)} by A7,TOPREAL1:def 6;
hence contradiction by A56,A58,A60,TARSKI:def 1;
end;
suppose
ilp+1 < j;
hence contradiction by A59,TOPREAL1:def 7;
end;
end;
1 <= j by A16,A55,XXREAL_0:2;
then ilp >= j by A3,A8,A10,A7,A46,A50,A53,A54,A57,JORDAN5C:28;
then ilp >= ilp+1 by A55,XXREAL_0:2;
hence contradiction by XREAL_1:29;
end;
then
A61: h = mid(g,ilp+1,len g) by JORDAN3:def 3;
then
A62: ilp + len h = len g by A9,A32,XREAL_1:235;
then
A63: m = g/^(ilp+n-'1) by A29,FINSEQ_6:117;
A64: 1 <= ilp+n by A25,XXREAL_0:2;
ilp+n -' 1 + 1 = ilp+n by A25,XREAL_1:235,XXREAL_0:2;
then ilp+n-'1 < len g by A29,A62,NAT_1:13;
then
A65: m/.len m in RightComp f by A2,A63,FINSEQ_6:185;
A66: h/.n = g/.(n+(ilp+1)-'1) by A20,A11,A10,A17,A61,SPRECT_2:3
.= g/.(n+ilp+1-'1)
.= g/.(ilp+n) by NAT_D:34;
then
A67: ilp+n <> len g by A2,A15,A18,XBOOLE_0:3;
then reconsider m as S-Sequence_in_R2 by A4,A29,A62,A64,JORDAN3:6;
ilp+n in dom g by A29,A62,A64,FINSEQ_3:25;
then m/.1 in LeftComp f by A20,A15,A66,SPRECT_2:8;
then L~f meets L~m by A65,Th33;
then consider q being object such that
A68: q in L~f and
A69: q in L~m by XBOOLE_0:3;
reconsider q as Point of TOP-REAL 2 by A69;
consider i such that
A70: 1 <= i and
A71: i+1 <= len m and
A72: q in LSeg(m,i) by A69,SPPOL_2:13;
set j = i+(ilp+n)-'1;
A73: j = i-'1+(ilp+n) by A70,NAT_D:38;
then
A74: j >= ilp+n by NAT_1:11;
len m = len g -' (ilp+n) + 1 by A4,A29,A62,A64,FINSEQ_6:118;
then
A75: i < len g -'(ilp+n) +1 by A71,NAT_1:13;
then i-'1 < len g-'(ilp+n) by A70,NAT_D:54;
then i-'1+(ilp+n) < len g by NAT_D:53;
then
A76: j + 1 <= len g by A73,NAT_1:13;
ilp+n < len g by A29,A62,A67,XXREAL_0:1;
then
A77: LSeg(m,i) = LSeg(g,i+(ilp+n)-'1) by A64,A70,A75,JORDAN4:19;
ilp+1 < ilp+n by A24,XREAL_1:6;
then
A78: j > ilp+1 by A74,XXREAL_0:2;
A79: now
assume lp = q;
then lp in LSeg(g,ilp) /\ LSeg(g,j) by A8,A72,A77,XBOOLE_0:def 4;
then LSeg(g,ilp) meets LSeg(g,j);
hence contradiction by A78,TOPREAL1:def 7;
end;
1 <= j by A64,A74,XXREAL_0:2;
then ilp >= j by A3,A8,A10,A7,A68,A72,A77,A79,A76,JORDAN5C:28;
then ilp >= ilp+1 by A78,XXREAL_0:2;
hence contradiction by XREAL_1:29;
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 and
A2: i < len GoB f and
A3: 1 <= j and
A4: j < width GoB f;
A5: i+1 <= len GoB f by A2,NAT_1:13;
set G = GoB f;
A6: 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,A3,A4,GOBOARD6:26;
A7: N-bound L~SpStSeq L~f = N-bound L~f by SPRECT_1:60;
A8: 1 <= width GoB f by GOBRD11:34;
then
A9: <*(GoB f)*(i,1)*> is_in_the_area_of f by A1,A2,Th49;
1 <= i+1 by A1,NAT_1:13;
then
A10: <*(GoB f)*(i+1,1)*> is_in_the_area_of f by A8,A5,Th49;
assume Int cell(GoB f,i,j) meets L~SpStSeq L~f;
then consider x being object such that
A11: x in Int cell(GoB f,i,j) and
A12: x in L~SpStSeq L~f by XBOOLE_0:3;
A13: W-bound L~SpStSeq L~f = W-bound L~f by SPRECT_1:58;
A14: 1 <= len GoB f by GOBRD11:34;
then
A15: <*(GoB f)*(1,j)*> is_in_the_area_of f by A3,A4,Th49;
A16: j+1 <= width GoB f by A4,NAT_1:13;
1 <= j+1 by A3,NAT_1:13;
then
A17: <*(GoB f)*(1,j+1)*> is_in_the_area_of f by A14,A16,Th49;
A18: 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 Th35;
A19: E-bound L~SpStSeq L~f = E-bound L~f by SPRECT_1:61;
consider p such that
A20: p = x and
A21: 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
A12,A18;
A22: S-bound L~SpStSeq L~f = S-bound L~f by SPRECT_1:59;
consider r,s being Real such that
A23: x = |[r,s]| and
A24: G*(i,1)`1 < r and
A25: r < G*(i+1,1)`1 and
A26: G*(1,j)`2 < s and
A27: s < G*(1,j+1)`2 by A6,A11;
A28: p`1 = r by A23,A20,EUCLID:52;
A29: p`2 = s by A23,A20,EUCLID:52;
per cases by A21;
suppose
A30: p`1 = W-bound L~SpStSeq L~f;
A31: 1 in dom<*G*(i,1)*> by FINSEQ_5:6;
<*G*(i,1)*>/.1 = G*(i,1) by FINSEQ_4:16;
hence contradiction by A24,A9,A28,A13,A30,A31;
end;
suppose
A32: p`2 = N-bound L~SpStSeq L~f;
A33: 1 in dom<*G*(1,j+1)*> by FINSEQ_5:6;
<*G*(1,j+1)*>/.1 = G*(1,j+1) by FINSEQ_4:16;
hence contradiction by A27,A17,A29,A7,A32,A33;
end;
suppose that
A34: p`2 = S-bound L~SpStSeq L~f;
A35: 1 in dom<*G*(1,j)*> by FINSEQ_5:6;
<*G*(1,j)*>/.1 = G*(1,j) by FINSEQ_4:16;
hence contradiction by A26,A15,A29,A22,A34,A35;
end;
suppose that
A36: p`1 = E-bound L~SpStSeq L~f;
A37: 1 in dom<*G*(i+1,1)*> by FINSEQ_5:6;
<*G*(i+1,1)*>/.1 = G*(i+1,1) by FINSEQ_4:16;
hence contradiction by A25,A10,A28,A19,A36,A37;
end;
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 being_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 being_S-Seq;
2 <= len g by A3,TOPREAL1:def 8;
then 1 <= len g by XXREAL_0:2;
then
A4: len g in dom g by FINSEQ_3:25;
assume p in L~g;
then Index(p,g) < len g by JORDAN3:8;
then
A5: Index(p,g)+1 <= len g by NAT_1:13;
1<=Index(p,g)+1 by NAT_1:11;
then
A6: Index(p,g)+1 in dom g by A5,FINSEQ_3:25;
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 3;
mid(g,Index(p,g)+1,len g) is_in_the_area_of f by A1,A4,A6,SPRECT_2:22;
hence thesis by A2,A7,SPRECT_2:24;
end;
suppose
p=g.(Index(p,g)+1);
then L_Cut(g,p) = mid(g,Index(p,g)+1,len g) by JORDAN3:def 3;
hence thesis by A1,A4,A6,SPRECT_2:22;
end;
end;