:: Special Polygons
:: by Czes\law Byli\'nski and Yatsuka Nakamura
::
:: Received January 30, 1995
:: Copyright (c) 1995-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies NUMBERS, SUBSET_1, EUCLID, FINSEQ_1, PRE_TOPC, NAT_1, ARYTM_3,
RLTOPSP1, FINSEQ_5, XXREAL_0, RELAT_1, PARTFUN1, CARD_1, XBOOLE_0,
RFINSEQ, ARYTM_1, ORDINAL4, FINSEQ_4, TOPREAL1, STRUCT_0, TARSKI,
MCART_1, FUNCT_1, ZFMISC_1, TOPREAL4, XXREAL_1, RCOMP_1, BORSUK_1,
TOPS_2, ORDINAL2, SPPOL_2, REAL_1;
notations TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, XREAL_0,
XXREAL_0, NAT_1, FUNCT_1, PARTFUN1, FINSEQ_1, ZFMISC_1, FINSEQ_4,
RFINSEQ, STRUCT_0, PRE_TOPC, COMPTS_1, TOPS_2, RLTOPSP1, EUCLID,
BORSUK_1, TOPREAL1, TOPREAL4, FINSEQ_5;
constructors XXREAL_0, NAT_1, FINSEQ_4, ZFMISC_1, RFINSEQ, BINARITH, FINSEQ_5,
TOPS_2, COMPTS_1, TOPMETR, TOPREAL1, TOPREAL4, REAL_1, CONVEX1;
registrations XBOOLE_0, RELAT_1, ORDINAL1, XREAL_0, FINSEQ_1, FINSEQ_5,
STRUCT_0, PRE_TOPC, EUCLID, TOPREAL1, NAT_1, INT_1, CARD_1, RLTOPSP1,
SPPOL_1;
requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM;
definitions TARSKI, TOPREAL1, TOPREAL4, XBOOLE_0;
equalities TOPREAL1;
expansions TARSKI, TOPREAL1, TOPREAL4, XBOOLE_0;
theorems TARSKI, ENUMSET1, ZFMISC_1, NAT_1, FINSEQ_1, FINSEQ_2, FINSEQ_3,
FINSEQ_4, TOPS_2, HEINE, TOPMETR, COMPTS_1, RFINSEQ, EUCLID, TOPREAL1,
TOPREAL3, TOPREAL4, GOBOARD1, FINSEQ_5, RELAT_1, PARTFUN2, INT_1,
XBOOLE_0, XBOOLE_1, XREAL_1, XXREAL_0, ORDINAL1, PARTFUN1, RLTOPSP1,
SEQ_4, NAT_D;
schemes FINSEQ_2;
begin :: Segments in TOP-REAL 2
reserve P for Subset of TOP-REAL 2,
f,f1,f2,g for FinSequence of TOP-REAL 2,
p,p1,p2,q,q1,q2 for Point of TOP-REAL 2,
r1,r2,r19,r29 for Real,
i,j,k,n for Nat;
theorem
|[ r1,r2 ]| = |[ r19,r29 ]| implies r1 = r19 & r2 = r29 by FINSEQ_1:77;
theorem Th2:
for i, j being Nat holds i+j = len f implies LSeg(f,i) = LSeg(Rev f,j)
proof
let i, j be Nat;
assume
A1: i+j = len f;
per cases;
suppose that
A2: 1 <= i and
A3: i + 1 <= len f;
A4: i+(j+1) = len f + 1 by A1;
A5: i in dom f by A2,A3,SEQ_4:134;
then j+1 in dom Rev f by A4,FINSEQ_5:59;
then
A6: j+1 <= len Rev f by FINSEQ_3:25;
A7: i+1+j = len f + 1 by A1;
A8: i+1 in dom f by A2,A3,SEQ_4:134;
then j in dom Rev f by A7,FINSEQ_5:59;
then
A9: 1 <= j by FINSEQ_3:25;
thus LSeg(f,i) = LSeg(f/.i,f/.(i+1)) by A2,A3,TOPREAL1:def 3
.= LSeg((Rev f)/.(j+1),f/.(i+1)) by A5,A4,FINSEQ_5:66
.= LSeg((Rev f)/.j,(Rev f)/.(j+1)) by A8,A7,FINSEQ_5:66
.= LSeg(Rev f,j) by A6,A9,TOPREAL1:def 3;
end;
suppose
A10: not 1 <= i;
then i = 0 by NAT_1:14;
then not j+1 <= len f by A1,NAT_1:13;
then
A11: not j+1 <= len Rev f by FINSEQ_5:def 3;
LSeg(f,i) = {} by A10,TOPREAL1:def 3;
hence thesis by A11,TOPREAL1:def 3;
end;
suppose
A12: not i+1 <= len f;
then
A13: LSeg(f,i) = {} by TOPREAL1:def 3;
j < 1 by A1,A12,XREAL_1:6;
hence thesis by A13,TOPREAL1:def 3;
end;
end;
theorem Th3:
for i, n being Nat holds i+1 <= len(f|n) implies LSeg(f|n,i) = LSeg(f,i)
proof
let i,n be Nat;
assume
A1: i+1 <= len(f|n);
per cases;
suppose
i <> 0;
then
A2: 1 <= i by NAT_1:14;
then
A3: i in dom(f|n) by A1,SEQ_4:134;
len(f|n) <= len f by FINSEQ_5:16;
then
A4: i+1 <= len f by A1,XXREAL_0:2;
A5: i+1 in dom(f|n) by A1,A2,SEQ_4:134;
thus LSeg(f|n,i) = LSeg((f|n)/.i,(f|n)/.(i+1)) by A1,A2,TOPREAL1:def 3
.= LSeg(f/.i,(f|n)/.(i+1)) by A3,FINSEQ_4:70
.= LSeg(f/.i,f/.(i+1)) by A5,FINSEQ_4:70
.= LSeg(f,i) by A2,A4,TOPREAL1:def 3;
end;
suppose
A6: i = 0;
hence LSeg(f|n,i) = {} by TOPREAL1:def 3
.= LSeg(f,i) by A6,TOPREAL1:def 3;
end;
end;
theorem Th4:
for i, n being Nat holds n <= len f & 1 <= i implies LSeg(f/^n,i)
= LSeg(f,n+i)
proof
let i,n be Nat;
assume that
A1: n <= len f and
A2: 1 <= i;
per cases;
suppose
A3: i+1 <= len f - n;
1<=i+1 by NAT_1:11;
then 1 <= len f - n by A3,XXREAL_0:2;
then
A4: 1+n <= len f by XREAL_1:19;
n <= 1+n by NAT_1:11;
then n <= len f by A4,XXREAL_0:2;
then
A5: len(f/^n) = len f - n by RFINSEQ:def 1;
then
A6: i in dom(f/^n) by A2,A3,SEQ_4:134;
A7: i+1+n <= len f by A3,XREAL_1:19;
i <= i+n by NAT_1:11;
then
A8: 1 <= i+n by A2,XXREAL_0:2;
A9: i+1 in dom(f/^n) by A2,A3,A5,SEQ_4:134;
thus LSeg(f/^n,i) = LSeg((f/^n)/.i,(f/^n)/.(i+1)) by A2,A3,A5,
TOPREAL1:def 3
.= LSeg(f/.(i+n),(f/^n)/.(i+1)) by A6,FINSEQ_5:27
.= LSeg(f/.(i+n),f/.(i+1+n)) by A9,FINSEQ_5:27
.= LSeg(f/.(i+n),f/.(i+n+1))
.= LSeg(f,n+i) by A8,A7,TOPREAL1:def 3;
end;
suppose
A10: i+1 > len f - n;
then n+(i+1) > len f by XREAL_1:19;
then
A11: n+i+1 > len f;
i+1 > len(f/^n) by A1,A10,RFINSEQ:def 1;
hence LSeg(f/^n,i) = {} by TOPREAL1:def 3
.= LSeg(f,n+i) by A11,TOPREAL1:def 3;
end;
end;
theorem Th5:
for i, n being Nat holds 1 <= i & i+1 <= len f - n implies LSeg(f
/^n,i) = LSeg(f,n+i)
proof
let i, n be Nat;
assume
A1: 1 <= i;
A2: n <= i+1+n by NAT_1:11;
assume i+1 <= len f - n;
then i+1+n <= len f by XREAL_1:19;
then n <= len f by A2,XXREAL_0:2;
hence thesis by A1,Th4;
end;
theorem Th6:
for i being Nat holds i+1 <= len f implies LSeg(f^g,i) = LSeg(f,i )
proof
let i be Nat;
assume
A1: i+1 <= len f;
per cases;
suppose
i <> 0;
then
A2: 1 <= i by NAT_1:14;
then
A3: i in dom f by A1,SEQ_4:134;
len(f^g) = len f + len g by FINSEQ_1:22;
then len(f^g) >= len f by NAT_1:11;
then
A4: i+1 <= len(f^g) by A1,XXREAL_0:2;
A5: i+1 in dom f by A1,A2,SEQ_4:134;
thus LSeg(f,i) = LSeg(f/.i,f/.(i+1)) by A1,A2,TOPREAL1:def 3
.= LSeg((f^g)/.i,f/.(i+1)) by A3,FINSEQ_4:68
.= LSeg((f^g)/.i,(f^g)/.(i+1)) by A5,FINSEQ_4:68
.= LSeg(f^g,i) by A2,A4,TOPREAL1:def 3;
end;
suppose
A6: i = 0;
hence LSeg(f^g,i) = {} by TOPREAL1:def 3
.= LSeg(f,i) by A6,TOPREAL1:def 3;
end;
end;
theorem Th7:
for i being Nat holds 1 <= i implies LSeg(f^g,len f + i) = LSeg(g ,i)
proof
let i be Nat;
assume
A1: 1 <= i;
per cases;
suppose
A2: i+1 <= len g;
len f +(i+1) = len f+i+1;
then len f +i+1 <= len f + len g by A2,XREAL_1:6;
then
A3: len f+i+1 <= len(f^g) by FINSEQ_1:22;
i <= len f+i by NAT_1:11;
then
A4: 1 <= len f+i by A1,XXREAL_0:2;
A5: i+1 in dom g by A1,A2,SEQ_4:134;
A6: i in dom g by A1,A2,SEQ_4:134;
thus LSeg(g,i) = LSeg(g/.i,g/.(i+1)) by A1,A2,TOPREAL1:def 3
.= LSeg((f^g)/.(len f+i),g/.(i+1)) by A6,FINSEQ_4:69
.= LSeg((f^g)/.(len f+i), (f^g)/.(len f + (i+1))) by A5,FINSEQ_4:69
.= LSeg(f^g,len f + i) by A4,A3,TOPREAL1:def 3;
end;
suppose
A7: i+1 > len g;
then len f + (i + 1) > len f + len g by XREAL_1:6;
then len f + i + 1 > len(f^g) by FINSEQ_1:22;
hence LSeg(f^g,len f + i) = {} by TOPREAL1:def 3
.= LSeg(g,i) by A7,TOPREAL1:def 3;
end;
end;
theorem Th8:
f is non empty & g is non empty implies LSeg(f^g,len f) = LSeg(f
/.len f,g/.1)
proof
assume that
A1: f is non empty and
A2: g is non empty;
A3: 1 in dom g by A2,FINSEQ_5:6;
then 1 <= len g by FINSEQ_3:25;
then len f + 1 <= len f + len g by XREAL_1:6;
then
A4: len f + 1 <= len(f^g) by FINSEQ_1:22;
A5: len f in dom f by A1,FINSEQ_5:6;
then 1 <= len f by FINSEQ_3:25;
hence LSeg(f^g,len f) = LSeg((f^g)/.(len f),(f^g)/.(len f+1)) by A4,
TOPREAL1:def 3
.= LSeg(f/.len f,(f^g)/.(len f+1)) by A5,FINSEQ_4:68
.= LSeg(f/.len f,g/.1) by A3,FINSEQ_4:69;
end;
theorem Th9:
for i being Nat holds i+1 <= len(f-:p) implies LSeg(f-:p,i) = LSeg(f,i)
proof
let i be Nat;
f-:p = f|(p..f) by FINSEQ_5:def 1;
hence thesis by Th3;
end;
theorem Th10:
for i being Nat holds p in rng f implies LSeg(f:-p,i+1) = LSeg(f ,i+p..f)
proof
let i be Nat;
A1: 1 <= i+1 by NAT_1:11;
assume
A2: p in rng f;
then
A3: len (f:-p) = len f - p..f + 1 by FINSEQ_5:50;
A4: i+(1+1) = i+1+1;
per cases;
suppose
A5: i+2 <= len(f:-p);
then i+1 <= len f - p..f by A4,A3,XREAL_1:6;
then
A6: i+1+p..f <= len f by XREAL_1:19;
1 <= p..f by A2,FINSEQ_4:21;
then i+1 <= i+p..f by XREAL_1:6;
then
A7: 1 <= i+p..f by A1,XXREAL_0:2;
A8: i+1 in dom(f:-p) by A1,A4,A5,SEQ_4:134;
A9: i+1+1 in dom(f:-p) by A1,A5,SEQ_4:134;
thus LSeg(f:-p,i+1) = LSeg((f:-p)/.(i+1),(f:-p)/.(i+1+1)) by A1,A5,
TOPREAL1:def 3
.= LSeg(f/.(i+p..f),(f:-p)/.(i+1+1)) by A2,A8,FINSEQ_5:52
.= LSeg(f/.(i+p..f),f/.(i+1+p..f)) by A2,A9,FINSEQ_5:52
.= LSeg(f/.(i+p..f),f/.(i+p..f+1))
.= LSeg(f,i+p..f) by A7,A6,TOPREAL1:def 3;
end;
suppose
A10: i+2 > len(f:-p);
then i+1 > len f - p..f by A4,A3,XREAL_1:6;
then p..f+(i+1) > len f by XREAL_1:19;
then i+p..f+1 > len f;
hence LSeg(f,i+p..f) = {} by TOPREAL1:def 3
.= LSeg(f:-p,i+1) by A4,A10,TOPREAL1:def 3;
end;
end;
theorem Th11:
L~<*>(the carrier of TOP-REAL 2) = {} by TOPREAL1:22;
theorem Th12:
L~<*p*> = {}
by FINSEQ_1:39,TOPREAL1:22;
theorem Th13:
p in L~f implies ex i st 1 <= i & i+1 <= len f & p in LSeg(f,i)
proof
set X = { LSeg(f,i) : 1 <= i & i+1 <= len f};
assume p in L~f;
then consider Y being set such that
A1: p in Y and
A2: Y in X by TARSKI:def 4;
ex i st Y = LSeg(f,i) & 1 <= i & i+1 <= len f by A2;
hence thesis by A1;
end;
theorem Th14:
p in L~f implies ex i st 1 <= i & i+1 <= len f & p in LSeg(f/.i, f/.(i+1))
proof
assume p in L~f;
then consider i such that
A1: 1 <= i and
A2: i+1 <= len f and
A3: p in LSeg(f,i) by Th13;
take i;
thus 1 <= i & i+1 <= len f by A1,A2;
thus thesis by A1,A2,A3,TOPREAL1:def 3;
end;
theorem Th15:
1 <= i & i+1 <= len f & p in LSeg(f/.i,f/.(i+1)) implies p in L~ f
proof
assume that
A1: 1 <= i and
A2: i+1 <= len f and
A3: p in LSeg(f/.i,f/.(i+1));
set X = { LSeg(f,j) : 1 <= j & j+1 <= len f };
A4: LSeg(f,i) in X by A1,A2;
LSeg(f,i) = LSeg(f/.i,f/.(i+1)) by A1,A2,TOPREAL1:def 3;
hence thesis by A3,A4,TARSKI:def 4;
end;
theorem
1 <= i & i+1 <= len f implies LSeg(f/.i,f/.(i+1)) c= L~f
proof
assume that
A1: 1 <= i and
A2: i+1 <= len f;
LSeg(f,i) = LSeg(f/.i,f/.(i+1)) by A1,A2,TOPREAL1:def 3;
hence thesis by TOPREAL3:19;
end;
theorem
p in LSeg(f,i) implies p in L~f
proof
LSeg(f,i) c= L~f by TOPREAL3:19;
hence thesis;
end;
theorem Th18:
len f >= 2 implies rng f c= L~f
proof
assume
A1: len f >= 2;
let x be object;
assume x in rng f;
then consider i being Element of NAT such that
A2: i in dom f and
A3: f/.i = x by PARTFUN2:2;
A4: 1 <= i by A2,FINSEQ_3:25;
A5: i <= len f by A2,FINSEQ_3:25;
A6: f/.i in LSeg(f/.i,f/.(i+1)) by RLTOPSP1:68;
per cases;
suppose
A7: i = len f;
then consider j be Nat such that
A8: j+1 = i by A1,NAT_1:6;
reconsider j as Element of NAT by ORDINAL1:def 12;
1+1 <= j+1 by A1,A7,A8;
then
A9: 1 <= j by XREAL_1:6;
f/.(j+1) in LSeg(f/.j,f/.(j+1)) by RLTOPSP1:68;
hence thesis by A3,A7,A8,A9,Th15;
end;
suppose
i <> len f;
then i < len f by A5,XXREAL_0:1;
then i+1 <= len f by NAT_1:13;
hence thesis by A3,A4,A6,Th15;
end;
end;
theorem Th19:
f is non empty implies L~(f^<*p*>) = L~f \/ LSeg(f/.len f,p)
proof
set fp = f^<*p*>;
A1: len f + 1 <= len fp by FINSEQ_2:16;
1 <= len f + 1 by NAT_1:11;
then
A2: len f + 1 in dom fp by A1,FINSEQ_3:25;
A3: fp/.(len f + 1) = p by FINSEQ_4:67;
len fp = len f + 1 by FINSEQ_2:16;
then
A4: fp|(len f + 1) = fp by FINSEQ_1:58;
A5: dom f c= dom(fp) by FINSEQ_1:26;
A6: fp|len f = f by FINSEQ_5:23;
assume f is non empty;
then
A7: len f in dom f by FINSEQ_5:6;
then fp/.len f = f/.len f by FINSEQ_4:68;
hence thesis by A2,A7,A3,A4,A5,A6,TOPREAL3:38;
end;
theorem Th20:
f is non empty implies L~(<*p*>^f) = LSeg(p,f/.1) \/ L~f
proof
set q = f/.1;
A1: len <*p*> = 1 by FINSEQ_1:39;
then
A2: len (<*p*>^f) = 1 + len f by FINSEQ_1:22;
assume that
A3: f is non empty;
hereby
let x be object;
assume
A4: x in L~(<*p*>^f);
then reconsider r = x as Point of TOP-REAL 2;
consider i such that
A5: 1 <= i and
A6: i+1 <= len (<*p*>^f) and
A7: r in LSeg((<*p*>^f)/.i,(<*p*>^f)/.(i+1)) by A4,Th14;
now
per cases by A5,XXREAL_0:1;
case
A8: i = 1;
then
A9: p = (<*p*>^f)/.i by FINSEQ_5:15;
i in dom f by A3,A8,FINSEQ_5:6;
hence r in LSeg(p,q) by A1,A7,A8,A9,FINSEQ_4:69;
end;
case
A10: i > 1;
then consider j be Nat such that
A11: i = j + 1 by NAT_1:6;
reconsider j as Element of NAT by ORDINAL1:def 12;
A12: 1 <= j by A10,A11,NAT_1:13;
A13: j+1 <= len f by A2,A6,A11,XREAL_1:6;
then j+1 in dom f by A12,SEQ_4:134;
then
A14: (<*p*>^f)/.(i+1) = f/.(j+1) by A1,A11,FINSEQ_4:69;
j in dom f by A12,A13,SEQ_4:134;
then (<*p*>^f)/.i = f/.j by A1,A11,FINSEQ_4:69;
hence r in L~f by A7,A12,A13,A14,Th15;
end;
end;
hence x in LSeg(p,q) \/ L~f by XBOOLE_0:def 3;
end;
let x be object;
assume
A15: x in LSeg(p,q) \/ L~f;
then reconsider r = x as Point of TOP-REAL 2;
per cases by A15,XBOOLE_0:def 3;
suppose
A16: r in LSeg(p,q);
set i = 1;
i <= len f by A3,NAT_1:14;
then
A17: i+1 <= len(<*p*>^f) by A2,XREAL_1:6;
i in dom f by A3,FINSEQ_5:6;
then
A18: q = (<*p*>^f)/.(i+1) by A1,FINSEQ_4:69;
p = (<*p*>^f)/.i by FINSEQ_5:15;
hence thesis by A16,A17,A18,Th15;
end;
suppose
r in L~f;
then consider j such that
A19: 1 <= j and
A20: j+1 <= len f and
A21: r in LSeg(f/.j,f/.(j+1)) by Th14;
set i = j + 1;
j in dom f by A19,A20,SEQ_4:134;
then
A22: (<*p*>^f)/.i = f/.j by A1,FINSEQ_4:69;
j+1 in dom f by A19,A20,SEQ_4:134;
then
A23: (<*p*>^f)/.(i+1) = f/.(j+1) by A1,FINSEQ_4:69;
i+1 <= len (<*p*>^f) by A2,A20,XREAL_1:6;
hence thesis by A21,A22,A23,Th15,NAT_1:12;
end;
end;
theorem Th21:
L~<*p,q*> = LSeg(p,q)
proof
set f = <*p*>;
A1: len f = 1 by FINSEQ_1:39;
thus L~<*p,q*> = L~(f^<*q*>) by FINSEQ_1:def 9
.= L~f \/ LSeg(f/.len f,q) by Th19
.= L~f \/ LSeg(p,q) by A1,FINSEQ_4:16
.= {} \/ LSeg(p,q) by A1,TOPREAL1:22
.= LSeg(p,q);
end;
theorem Th22:
L~f = L~(Rev f)
proof
defpred P[FinSequence of TOP-REAL 2] means L~$1 = L~(Rev $1);
A1: for f,p st P[f] holds P[f^<*p*>]
proof
let f,p such that
A2: P[f];
per cases;
suppose
A3: f is empty;
hence L~(f^<*p*>) = L~<*p*> by FINSEQ_1:34
.= L~(Rev <*p*>) by FINSEQ_5:60
.= L~(Rev(f^<*p*>)) by A3,FINSEQ_1:34;
end;
suppose
A4: f is non empty;
set q9 = (Rev f)/.1;
set q = f/.len f;
len f = len Rev f by FINSEQ_5:def 3;
then
A5: Rev f is non empty by A4;
q = q9 by A4,FINSEQ_5:65;
hence L~(f^<*p*>) = LSeg(p,q9) \/ L~(Rev f) by A2,A4,Th19
.= L~(<*p*>^(Rev f)) by A5,Th20
.= L~(Rev(f^<*p*>)) by FINSEQ_5:63;
end;
end;
A6: P[<*>(the carrier of TOP-REAL 2)];
for f holds P[f] from FINSEQ_2:sch 2(A6,A1);
hence thesis;
end;
theorem Th23:
f1 is non empty & f2 is non empty implies L~(f1^f2) = L~f1 \/
LSeg(f1/.len f1,f2/.1) \/ L~f2
proof
set p = f1/.len f1, q = f2/.1;
defpred P[FinSequence of TOP-REAL 2] means L~(f1^<*q*>^$1) = L~f1 \/ LSeg(p,
q) \/ L~(<*q*>^$1);
assume
A1: f1 is non empty;
A2: for f for o being Point of TOP-REAL 2 st P[f] holds P[f^<*o*>]
proof
let f;
let o be Point of TOP-REAL 2 such that
A3: P[f];
per cases;
suppose
f is empty;
then
A4: (f^<*o*>) = <*o*> by FINSEQ_1:34;
len(f1^<*q*>) = len f1 + 1 by FINSEQ_2:16;
then (f1^<*q*>)/.len(f1^<*q*>) = q by FINSEQ_4:67;
hence L~(f1^<*q*>^(f^<*o*>)) = L~(f1^<*q*>) \/ LSeg(q,o) by A4,Th19
.= L~f1 \/ LSeg(p,q) \/ LSeg(q,o) by A1,Th19
.= L~f1 \/ LSeg(p,q) \/ L~<*q,o*> by Th21
.= L~f1 \/ LSeg(p,q) \/ L~(<*q*>^(f^<*o*>)) by A4,FINSEQ_1:def 9;
end;
suppose
A5: f is non empty;
set g = f1^<*q*>^f, h = <*q*>^f;
len f <> 0 by A5;
then consider
f9 being FinSequence of TOP-REAL 2, d being Point of TOP-REAL 2
such that
A6: f = f9^<*d*> by FINSEQ_2:19;
A7: h = <*q*>^f9^<*d*> by A6,FINSEQ_1:32;
then len h = len(<*q*>^f9)+1 by FINSEQ_2:16;
then
A8: h/.len h = d by A7,FINSEQ_4:67;
A9: g = f1^<*q*>^f9^<*d*> by A6,FINSEQ_1:32;
then len g = len(f1^<*q*>^f9)+1 by FINSEQ_2:16;
then g/.len g = d by A9,FINSEQ_4:67;
then
A10: L~h \/ LSeg(g/.len g,o) = L~(h^<*o*>) by A8,Th19
.= L~(<*q*>^(f^<*o*>)) by FINSEQ_1:32;
thus L~(f1^<*q*>^(f^<*o*>)) = L~(g^<*o*>) by FINSEQ_1:32
.= L~g \/ LSeg(g/.len g,o) by Th19
.= L~f1 \/ LSeg(p,q) \/ L~(<*q*>^(f^<*o*>)) by A3,A10,XBOOLE_1:4;
end;
end;
assume f2 is non empty;
then
A11: f2 = <*q*>^(f2/^1) by FINSEQ_5:29;
A12: P[<*>(the carrier of TOP-REAL 2)]
proof
set O = <*>(the carrier of TOP-REAL 2);
thus L~(f1^<*q*>^O) = L~(f1^<*q*>) by FINSEQ_1:34
.= L~f1 \/ LSeg(p,q) \/ {} by A1,Th19
.= L~f1 \/ LSeg(p,q) \/ L~<*q*> by Th12
.= L~f1 \/ LSeg(p,q) \/ L~(<*q*>^O) by FINSEQ_1:34;
end;
for f holds P[f] from FINSEQ_2:sch 2(A12,A2);
then L~(f1^<*q*>^(f2/^1)) = L~f1 \/ LSeg(p,q) \/ L~(<*q*>^(f2/^1));
hence thesis by A11,FINSEQ_1:32;
end;
Lm1: L~(f|n) c= L~f
proof
now
per cases;
suppose
A1: n = 0;
thus thesis by A1,Th11;
end;
suppose
A2: n <> 0;
now
per cases;
suppose
A3: n < len f;
then len(f/^n) = len f - n by RFINSEQ:def 1;
then len(f/^n) <> 0 by A3;
then
A4: f/^n is non empty;
len(f|n) = n by A3,FINSEQ_1:59;
then
A5: f|n is non empty by A2;
(f|n)^(f/^n) = f by RFINSEQ:8;
then
L~f = L~(f|n) \/ LSeg((f|n)/.len(f|n),(f/^n)/.1) \/ L~(f/^n) by A5,A4
,Th23
.= L~(f|n) \/ (LSeg((f|n)/.len(f|n),(f/^n)/.1) \/ L~(f/^n)) by
XBOOLE_1:4;
hence thesis by XBOOLE_1:7;
end;
suppose
n >= len f;
hence thesis by FINSEQ_1:58;
end;
end;
hence thesis;
end;
end;
hence thesis;
end;
theorem Th24:
q in rng f implies L~f = L~(f-:q) \/ L~(f:-q)
proof
set n = q..f;
assume
A1: q in rng f;
then
A2: n <= len f by FINSEQ_4:21;
per cases by A2,XXREAL_0:1;
suppose
A3: n < len f;
then len(f/^n) = len f - n by RFINSEQ:def 1;
then len(f/^n) <> 0 by A3;
then
A4: f/^n is non empty;
A5: len(f|n) = n by A3,FINSEQ_1:59;
f|n = f-:q by FINSEQ_5:def 1;
then
A6: (f|n)/.len(f|n) = q by A1,A5,FINSEQ_5:45;
A7: (f|n)^(f/^n) = f by RFINSEQ:8;
f|n is non empty by A1,A5,FINSEQ_4:21;
hence L~f = L~(f|n) \/ LSeg((f|n)/.len(f|n),(f/^n)/.1) \/ L~(f/^n) by A4,A7
,Th23
.= L~(f|n) \/ (LSeg((f|n)/.len(f|n),(f/^n)/.1) \/ L~(f/^n)) by XBOOLE_1:4
.= L~(f|n) \/ L~(<*(f|n)/.len(f|n)*>^(f/^n)) by A4,Th20
.= L~(f|n) \/ L~(f:-q) by A6,FINSEQ_5:def 2
.= L~(f-:q) \/ L~(f:-q) by FINSEQ_5:def 1;
end;
suppose
A8: n = len f;
then len(f/^n) = len f - n by RFINSEQ:def 1
.= 0 by A8;
then
A9: f/^n is empty;
f:-q = <*q*>^(f/^n) by FINSEQ_5:def 2
.= <*q*> by A9,FINSEQ_1:34;
then
A10: L~(f:-q) is empty by Th12;
L~f = L~(f|n) by A8,FINSEQ_1:58
.= L~(f-:q) by FINSEQ_5:def 1;
hence thesis by A10;
end;
end;
theorem Th25:
p in LSeg(f,n) implies L~f = L~Ins(f,n,p)
proof
set f1 = f|n, g1 = f1^<*p*>, f2 = f/^n;
A1: g1/.len g1 = g1/.(len f1 + 1) by FINSEQ_2:16
.= p by FINSEQ_4:67;
assume
A2: p in LSeg(f,n);
then
A3: n+1 <= len f by TOPREAL1:def 3;
then
A4: 1 <= len f - n by XREAL_1:19;
A5: n <= n+1 by NAT_1:11;
then
A6: len f1 = n by A3,FINSEQ_1:59,XXREAL_0:2;
then
A7: f1 is non empty by A2,TOPREAL1:def 3;
A8: 1 <= n by A2,TOPREAL1:def 3;
then
A9: n in dom f1 by A6,FINSEQ_3:25;
n <= len f by A3,A5,XXREAL_0:2;
then 1 <= len f2 by A4,RFINSEQ:def 1;
then
A10: 1 in dom f2 by FINSEQ_3:25;
A11: LSeg(f,n) = LSeg(f/.n,f/.(n+1)) by A8,A3,TOPREAL1:def 3
.= LSeg(f1/.len f1,f/.(n+1)) by A6,A9,FINSEQ_4:70
.= LSeg(f1/.len f1,f2/.1) by A10,FINSEQ_5:27;
thus L~Ins(f,n,p) = L~(g1^f2) by FINSEQ_5:def 4
.= L~g1 \/ LSeg(g1/.len g1,f2/.1) \/ L~f2 by A10,Th23,RELAT_1:38
.= L~f1 \/ LSeg(f1/.len f1,p) \/ LSeg(g1/.len g1,f2/.1) \/ L~f2 by A9,Th19,
RELAT_1:38
.= L~f1 \/ (LSeg(f1/.len f1,p) \/ LSeg(g1/.len g1,f2/.1)) \/ L~f2 by
XBOOLE_1:4
.= L~f1 \/ LSeg(f1/.len f1,f2/.1) \/ L~f2 by A2,A1,A11,TOPREAL1:5
.= L~(f1^f2) by A7,A10,Th23,RELAT_1:38
.= L~f by RFINSEQ:8;
end;
begin
registration
cluster being_S-Seq for FinSequence of TOP-REAL 2;
existence
proof
set p = |[ 0,0 ]|, q = |[ 1,1 ]|;
A1: p`2 = 0 by EUCLID:52;
A2: q`1 = 1 by EUCLID:52;
A3: q`2 = 1 by EUCLID:52;
p`1 = 0 by EUCLID:52;
then <* p,|[p`1,q`2]|,q *> is being_S-Seq by A1,A2,A3,TOPREAL3:34;
hence thesis;
end;
cluster being_S-Seq -> one-to-one unfolded s.n.c. special non trivial
for FinSequence of TOP-REAL 2;
coherence
by NAT_D:60;
cluster one-to-one unfolded s.n.c. special non trivial -> being_S-Seq
for FinSequence of TOP-REAL 2;
coherence
by NAT_D:60;
cluster being_S-Seq -> non empty for FinSequence of TOP-REAL 2;
coherence;
end;
registration
cluster one-to-one unfolded s.n.c. special non trivial for FinSequence of
TOP-REAL 2;
existence
proof
set f = the being_S-Seq FinSequence of TOP-REAL 2;
f is one-to-one unfolded s.n.c. special non trivial;
hence thesis;
end;
end;
theorem Th26:
len f <= 2 implies f is unfolded
proof
assume
A1: len f <= 2;
let i be Nat such that
A2: 1 <= i;
assume i+2 <= len f;
then i+2 <= 2 by A1,XXREAL_0:2;
then i <= 2-2 by XREAL_1:19;
hence thesis by A2,XXREAL_0:2;
end;
Lm2: <*p,q*> is unfolded
proof
len <*p,q*> = 2 by FINSEQ_1:44;
hence thesis by Th26;
end;
Lm3: f is unfolded implies f|n is unfolded
proof
assume
A1: f is unfolded;
set h = f|n;
let i be Nat such that
A2: 1 <= i and
A3: i + 2 <= len h;
A4: i+1 in dom h by A2,A3,SEQ_4:135;
len h <= len f by FINSEQ_5:16;
then
A5: i+2 <= len f by A3,XXREAL_0:2;
A6: i+1+1 = i+(1+1);
i+1 <= i+2 by XREAL_1:6;
hence LSeg(h,i) /\ LSeg(h,i+1) = LSeg(f,i) /\ LSeg(h,i+1) by A3,Th3,
XXREAL_0:2
.= LSeg(f,i) /\ LSeg(f,i+1) by A3,A6,Th3
.= {f/.(i+1)} by A1,A2,A5
.= {h/.(i+1)} by A4,FINSEQ_4:70;
end;
Lm4: f is unfolded implies f/^n is unfolded
proof
assume
A1: f is unfolded;
per cases;
suppose
A2: n <= len f;
set h = f/^n;
let i be Nat such that
A3: 1 <= i and
A4: i + 2 <= len h;
A5: i+1 in dom h by A3,A4,SEQ_4:135;
A6: len h = len f - n by A2,RFINSEQ:def 1;
then n+(i+2) <= len f by A4,XREAL_1:19;
then
A7: n+i+2 <= len f;
i <= n+i by NAT_1:11;
then
A8: 1 <= n+i by A3,XXREAL_0:2;
A9: i+1+1 = i+(1+1);
i+1 <= i+2 by XREAL_1:6;
then i+1 <= len h by A4,XXREAL_0:2;
hence LSeg(h,i) /\ LSeg(h,i+1) = LSeg(f,n+i) /\ LSeg(h,i+1) by A3,A6,Th5
.= LSeg(f,n+i) /\ LSeg(f,n+(i+1)) by A4,A9,A6,Th5,NAT_1:11
.= {f/.(n+i+1)} by A1,A7,A8
.= {f/.(n+(i+1))}
.= {h/.(i+1)} by A5,FINSEQ_5:27;
end;
suppose
n > len f;
then f/^n = <*>(the carrier of TOP-REAL 2) by RFINSEQ:def 1;
then len(f/^n) = 0;
hence thesis;
end;
end;
registration
let f be unfolded FinSequence of TOP-REAL 2, n;
cluster f|n -> unfolded for FinSequence of TOP-REAL 2;
coherence by Lm3;
cluster f/^n -> unfolded for FinSequence of TOP-REAL 2;
coherence by Lm4;
end;
theorem Th27:
p in rng f & f is unfolded implies f:-p is unfolded
proof
assume p in rng f;
then ex i being Element of NAT st i+1 = p..f & f:-p = f/^i by FINSEQ_5:49;
hence thesis;
end;
Lm5: f is unfolded implies f-:p is unfolded
proof
f-:p = f|(p..f) by FINSEQ_5:def 1;
hence thesis;
end;
registration
let f be unfolded FinSequence of TOP-REAL 2, p;
cluster f-:p -> unfolded;
coherence by Lm5;
end;
theorem Th28:
f is unfolded implies Rev f is unfolded
proof
assume
A1: f is unfolded;
A2: dom f = Seg len f by FINSEQ_1:def 3;
let i be Nat such that
A3: 1 <= i and
A4: i + 2 <= len Rev f;
A5: len Rev f = len f by FINSEQ_5:def 3;
then
A6: i+1 in dom f by A3,A4,SEQ_4:135;
i+1 <= i+1+1 by NAT_1:11;
then reconsider j9 = len f - (i+1) as Element of NAT by A4,A5,INT_1:5
,XXREAL_0:2;
i <= i+2 by NAT_1:11;
then reconsider j = len f - i as Element of NAT by A4,A5,INT_1:5,XXREAL_0:2;
A7: j9+(i+1) = len f;
i in dom f by A3,A4,A5,SEQ_4:135;
then j + 1 in dom f by A2,FINSEQ_5:2;
then
A8: j9+2 <= len f by FINSEQ_3:25;
A9: j + (i+1) = len f + 1;
i+(1+1) = i+1+1;
then
A10: 1 <= j9 by A4,A5,XREAL_1:19;
j+i = len f;
hence LSeg(Rev f,i) /\ LSeg(Rev f,i+1) = LSeg(f,j) /\ LSeg(Rev f,i+1) by Th2
.= LSeg(f,j9+1) /\ LSeg(f,j9) by A7,Th2
.= {f/.(j9+1)} by A1,A10,A8
.= {(Rev f)/.(i+1)} by A9,A2,A6,FINSEQ_5:2,66;
end;
theorem Th29:
g is unfolded & LSeg(p,g/.1) /\ LSeg(g,1) = {g/.1} implies <*p*>
^g is unfolded
proof
set f = <*p*>;
A1: len f = 1 by FINSEQ_1:39;
A2: f/.1 = p by FINSEQ_4:16;
A3: len(f^g) = len f + len g by FINSEQ_1:22;
assume that
A4: g is unfolded and
A5: LSeg(p,g/.1) /\ LSeg(g,1) = {g/.1};
let i be Nat such that
A6: 1 <= i and
A7: i + 2 <= len(f^g);
A8: i+(1+1) = i+1+1;
per cases;
suppose
A9: i = len f;
then
A10: LSeg(f^g,i+1) = LSeg(g,1) by Th7;
now
i <= i+1 by NAT_1:11;
then
A11: i < i+(1+1) by A8,NAT_1:13;
assume len g = 0;
hence contradiction by A1,A6,A7,A3,A11,XXREAL_0:2;
end;
then 1 <= len g by NAT_1:14;
then
A12: 1 in dom g by FINSEQ_3:25;
then LSeg(f^g,i) = LSeg(f/.len f,g/.1) by A9,Th8,RELAT_1:38;
hence thesis by A1,A5,A2,A9,A12,A10,FINSEQ_4:69;
end;
suppose
A13: i <> len f;
reconsider j = i - len f as Element of NAT by A1,A6,INT_1:5;
i > len f by A1,A6,A13,XXREAL_0:1;
then len f + 1 <= i by NAT_1:13;
then
A14: 1 <= j by XREAL_1:19;
A15: i+2-len f <= len g by A7,A3,XREAL_1:20;
then
A16: j+(1+1) <= len g;
j+1 <= j+1+1 by NAT_1:11;
then j+1 <= len g by A15,XXREAL_0:2;
then
A17: j+1 in dom g by A14,SEQ_4:134;
A18: len f + (j+1) = i+1;
len f + j = i;
hence LSeg(f^g,i) /\ LSeg(f^g,i+1) = LSeg(g,j) /\ LSeg(f^g,i+1) by A14,Th7
.= LSeg(g,j) /\ LSeg(g,j+1) by A18,Th7,NAT_1:11
.= {g/.(j+1)} by A4,A14,A16
.= {(f^g)/.(i+1)} by A18,A17,FINSEQ_4:69;
end;
end;
theorem Th30:
f is unfolded & k+1 = len f & LSeg(f,k) /\ LSeg(f/.len f,p) = {f
/.len f} implies f^<*p*> is unfolded
proof
set g = <*p*>;
assume that
A1: f is unfolded and
A2: k+1 = len f and
A3: LSeg(f,k) /\ LSeg(f/.len f,p) = {f/.len f};
A4: len g = 1 by FINSEQ_1:39;
A5: g/.1 = p by FINSEQ_4:16;
A6: len(f^g) = len f + len g by FINSEQ_1:22;
let i be Nat such that
A7: 1 <= i and
A8: i + 2 <= len(f^g);
A9: i+(1+1) = i+1+1;
per cases;
suppose
A10: i+2 <= len f;
then
A11: i+1 in dom f by A7,SEQ_4:135;
i+1 <= i+1+1 by NAT_1:11;
hence LSeg(f^g,i) /\ LSeg(f^g,i+1) = LSeg(f,i) /\ LSeg(f^g,i+1) by A10,Th6,
XXREAL_0:2
.= LSeg(f,i) /\ LSeg(f,i+1) by A9,A10,Th6
.= {f/.(i+1)} by A1,A7,A10
.= {(f^g)/.(i+1)} by A11,FINSEQ_4:68;
end;
suppose
i + 2 > len f;
then
A12: len f <= i+1 by A9,NAT_1:13;
A13: f is non empty by A4,A8,A6,A9,XREAL_1:6;
then
A14: len f in dom f by FINSEQ_5:6;
i+1 <= len f by A4,A8,A6,A9,XREAL_1:6;
then
A15: i+1 = len f by A12,XXREAL_0:1;
then
A16: LSeg(f^g,i+1) = LSeg(f/.len f,g/.1) by A13,Th8;
LSeg(f^g,i) = LSeg(f,k) by A2,A15,Th6;
hence thesis by A3,A5,A15,A16,A14,FINSEQ_4:68;
end;
end;
theorem Th31:
f is unfolded & g is unfolded & k+1 = len f & LSeg(f,k) /\ LSeg(
f/.len f,g/.1) = {f/.len f} & LSeg(f/.len f,g/.1) /\ LSeg(g,1) = {g/.1} implies
f^g is unfolded
proof
assume that
A1: f is unfolded and
A2: g is unfolded and
A3: k+1 = len f and
A4: LSeg(f,k) /\ LSeg(f/.len f,g/.1) = {f/.len f} and
A5: LSeg(f/.len f,g/.1) /\ LSeg(g,1) = {g/.1};
let i be Nat such that
A6: 1 <= i and
A7: i + 2 <= len(f^g);
A8: len(f^g) = len f + len g by FINSEQ_1:22;
per cases;
suppose
A9: i+2 <= len f;
then
A10: i+1 in dom f by A6,SEQ_4:135;
A11: i+(1+1) = i+1+1;
i+1 <= i+1+1 by NAT_1:11;
hence LSeg(f^g,i) /\ LSeg(f^g,i+1) = LSeg(f,i) /\ LSeg(f^g,i+1) by A9,Th6,
XXREAL_0:2
.= LSeg(f,i) /\ LSeg(f,i+1) by A9,A11,Th6
.= {f/.(i+1)} by A1,A6,A9
.= {(f^g)/.(i+1)} by A10,FINSEQ_4:68;
end;
suppose
A12: i + 2 > len f;
A13: i+(1+1) = i+1+1;
now
per cases;
suppose
A14: i <= len f;
len g <> 0 by A7,A8,A12;
then 1 <= len g by NAT_1:14;
then
A15: 1 in dom g by FINSEQ_3:25;
A16: f is non empty by A6,A14;
now
per cases;
suppose
A17: i = len f;
then
A18: LSeg(f^g,i+1) = LSeg(g,1) by Th7;
LSeg(f^g,i) = LSeg(f/.len f,g/.1) by A16,A15,A17,Th8,RELAT_1:38;
hence thesis by A5,A15,A17,A18,FINSEQ_4:69;
end;
suppose
i <> len f;
then i < len f by A14,XXREAL_0:1;
then
A19: i+1 <= len f by NAT_1:13;
len f <= i+1 by A12,A13,NAT_1:13;
then
A20: i+1 = len f by A19,XXREAL_0:1;
then
A21: LSeg(f^g,i) = LSeg(f,k) by A3,Th6;
A22: len f in dom f by A16,FINSEQ_5:6;
LSeg(f^g,i+1) = LSeg(f/.len f,g/.1) by A16,A15,A20,Th8,RELAT_1:38;
hence thesis by A4,A20,A21,A22,FINSEQ_4:68;
end;
end;
hence thesis;
end;
suppose
A23: i > len f;
then reconsider j = i - len f as Element of NAT by INT_1:5;
len f + 1 <= i by A23,NAT_1:13;
then
A24: 1 <= j by XREAL_1:19;
A25: i+2-len f <= len g by A7,A8,XREAL_1:20;
then
A26: j+(1+1) <= len g;
j+1 <= j+1+1 by NAT_1:11;
then j+1 <= len g by A25,XXREAL_0:2;
then
A27: j+1 in dom g by A24,SEQ_4:134;
A28: len f + (j+1) = i+1;
len f + j = i;
hence LSeg(f^g,i) /\ LSeg(f^g,i+1) = LSeg(g,j) /\ LSeg(f^g,i+1) by A24
,Th7
.= LSeg(g,j) /\ LSeg(g,j+1) by A28,Th7,NAT_1:11
.= {g/.(j+1)} by A2,A24,A26
.= {(f^g)/.(i+1)} by A28,A27,FINSEQ_4:69;
end;
end;
hence thesis;
end;
end;
theorem Th32:
f is unfolded & p in LSeg(f,n) implies Ins(f,n,p) is unfolded
proof
assume that
A1: f is unfolded and
A2: p in LSeg(f,n);
set f1 = f|n, g1 = f1^<*p*>, f2 = f/^n;
A3: n+1 <= len f by A2,TOPREAL1:def 3;
A4: n <= n+1 by NAT_1:11;
then
A5: len f1 = n by A3,FINSEQ_1:59,XXREAL_0:2;
then
A6: n+1 = len g1 by FINSEQ_2:16;
A7: n <= len f by A3,A4,XXREAL_0:2;
1 <= len f - n by A3,XREAL_1:19;
then
A8: 1 <= len f2 by A7,RFINSEQ:def 1;
then ZZ: 1 in dom f2 by FINSEQ_3:25;
then
A9: f/.(n+1) = f2/.1 by FINSEQ_5:27;
A10: 1 <= n by A2,TOPREAL1:def 3;
then
A11: LSeg(f,n) = LSeg(f/.n,f/.(n+1)) by A3,TOPREAL1:def 3;
A12: n in dom f1 by A10,A5,FINSEQ_3:25;
then
A13: f/.n = f1/.len f1 by A5,FINSEQ_4:70;
A14: g1/.len g1 = g1/.(len f1 + 1) by FINSEQ_2:16
.= p by FINSEQ_4:67;
then
A15: LSeg(f1/.len f1,p) \/ LSeg(g1/.len g1,f2/.1) = LSeg(f1/.len f1,f2/.1)
by A2,A11,A13,A9,TOPREAL1:5;
A16: now
len f1 <> 0 by A2,A5,TOPREAL1:def 3;
then consider k be Nat such that
A17: k+1 = len f1 by NAT_1:6;
reconsider k as Element of NAT by ORDINAL1:def 12;
A18: k+(1+1) <= len f by A3,A5,A17;
per cases;
suppose
k <> 0;
then
A19: 1 <= k by NAT_1:14;
LSeg(f1,k) = LSeg(f,k) by A17,Th3;
then
A20: LSeg(f1,k) /\ LSeg(f,n) = {f/.n} by A1,A5,A17,A18,A19;
now
let x be object;
hereby
assume
A21: x in LSeg(f1,k) /\ LSeg(f1/.len f1,p);
then x in LSeg(f1/.len f1,p) by XBOOLE_0:def 4;
then
A22: x in LSeg(f,n) by A11,A13,A9,A15,XBOOLE_0:def 3;
x in LSeg(f1,k) by A21,XBOOLE_0:def 4;
then x in LSeg(f1,k) /\ LSeg(f,n) by A22,XBOOLE_0:def 4;
hence x = f/.n by A20,TARSKI:def 1;
end;
assume
A23: x = f/.n;
then x in LSeg(f1,k) /\ LSeg(f,n) by A20,TARSKI:def 1;
then
A24: x in LSeg(f1,k) by XBOOLE_0:def 4;
x in LSeg(f1/.len f1,p) by A13,A23,RLTOPSP1:68;
hence x in LSeg(f1,k) /\ LSeg(f1/.len f1,p) by A24,XBOOLE_0:def 4;
end;
then LSeg(f1,k) /\ LSeg(f1/.len f1,p) = {f1/.len f1} by A13,TARSKI:def 1;
hence g1 is unfolded by A1,A17,Th30;
end;
suppose
k = 0;
then len g1 = 1+1 by A17,FINSEQ_2:16;
hence g1 is unfolded by Th26;
end;
end;
f1/.len f1 = g1/.n by A5,A12,FINSEQ_4:68;
then LSeg(g1,n) = LSeg(f1/.len f1,g1/.len g1) by A10,A6,TOPREAL1:def 3;
then
A25: LSeg(g1,n) /\ LSeg(g1/.len g1,f2/.1) = {g1/.len g1} by A2,A14,A11,A13,A9,
TOPREAL1:8;
now
per cases;
suppose
len f2 = 1;
then f2 = <*f2.1*> by FINSEQ_5:14 .= <*f2/.1*> by ZZ,PARTFUN1:def 6;
hence g1^f2 is unfolded by A16,A6,A25,Th30;
end;
suppose
len f2 <> 1;
then len f2 > 1 by A8,XXREAL_0:1;
then
A26: 1+1 <= len f2 by NAT_1:13;
then LSeg(f2,1) = LSeg(f2/.1,f2/.(1+1)) by TOPREAL1:def 3;
then
A27: f2/.1 in LSeg(f2,1) by RLTOPSP1:68;
A28: 1+1 <= len f - n by A7,A26,RFINSEQ:def 1;
then n+(1+1) <= len f by XREAL_1:19;
then
A29: {f/.(n+1)} = LSeg(f,n) /\ LSeg(f,n+1) by A1,A10
.= LSeg(f,n) /\ LSeg(f2,1) by A28,Th5;
now
let x be object;
hereby
assume
A30: x in LSeg(g1/.len g1,f2/.1) /\ LSeg(f2,1);
then x in LSeg(g1/.len g1,f2/.1) by XBOOLE_0:def 4;
then
A31: x in LSeg(f,n) by A11,A13,A9,A15,XBOOLE_0:def 3;
x in LSeg(f2,1) by A30,XBOOLE_0:def 4;
then x in LSeg(f,n) /\ LSeg(f2,1) by A31,XBOOLE_0:def 4;
hence x = f2/.1 by A9,A29,TARSKI:def 1;
end;
assume
A32: x = f2/.1;
then x in LSeg(g1/.len g1,f2/.1) by RLTOPSP1:68;
hence x in LSeg(g1/.len g1,f2/.1) /\ LSeg(f2,1) by A27,A32,
XBOOLE_0:def 4;
end;
then LSeg(g1/.len g1,f2/.1) /\ LSeg(f2,1) = {f2/.1} by TARSKI:def 1;
hence g1^f2 is unfolded by A1,A16,A6,A25,Th31;
end;
end;
hence thesis by FINSEQ_5:def 4;
end;
theorem Th33:
len f <= 2 implies f is s.n.c.
proof
assume
A1: len f <= 2;
let i,j be Nat such that
A2: i+1 < j;
now
assume that
A3: 1 <= i and
A4: i+1 <= len f and
A5: 1 <= j and
A6: j+1 <= len f;
j+1 <= 1+1 by A1,A6,XXREAL_0:2;
then j <= 1 by XREAL_1:6;
then
A7: j = 1 by A5,XXREAL_0:1;
i+1 <= 1+1 by A1,A4,XXREAL_0:2;
then i <= 1 by XREAL_1:6;
then i = 1 by A3,XXREAL_0:1;
hence contradiction by A2,A7;
end;
then LSeg(f,i) = {} or LSeg(f,j) = {} by TOPREAL1:def 3;
hence LSeg(f,i) /\ LSeg(f,j) = {};
end;
Lm6: <*p,q*> is s.n.c.
proof
len <*p,q*> = 2 by FINSEQ_1:44;
hence thesis by Th33;
end;
Lm7: f is s.n.c. implies f|n is s.n.c.
proof
assume
A1: f is s.n.c.;
let i,j be Nat such that
A2: i+1 < j;
per cases;
suppose
A3: i = 0 or j+1 > len(f|n);
now
per cases by A3;
case
i = 0;
hence LSeg(f|n,i) = {} by TOPREAL1:def 3;
end;
case
j+1 > len(f|n);
hence LSeg(f|n,j) = {} by TOPREAL1:def 3;
end;
end;
then LSeg(f|n,i) /\ LSeg(f|n,j) = {};
hence thesis;
end;
suppose that
i <> 0 and
A4: j+1 <= len(f|n);
A5: LSeg(f,i) misses LSeg(f,j) by A1,A2;
j <= j+1 by NAT_1:11;
then i+1 < j+1 by A2,XXREAL_0:2;
then LSeg(f|n,i) /\ LSeg(f|n,j) = LSeg(f,i) /\ LSeg(f|n,j) by A4,Th3,
XXREAL_0:2
.= {} by A5,A4,Th3;
hence thesis;
end;
end;
Lm8: f is s.n.c. implies f/^n is s.n.c.
proof
assume
A1: f is s.n.c.;
per cases;
suppose
A2: n <= len f;
let i,j be Nat such that
A3: i+1 < j;
now
per cases;
suppose
A4: i = 0 or j+1 > len(f/^n);
now
per cases by A4;
case
i = 0;
hence LSeg(f/^n,i) = {} by TOPREAL1:def 3;
end;
case
j+1 > len(f/^n);
hence LSeg(f/^n,j) = {} by TOPREAL1:def 3;
end;
end;
then LSeg(f/^n,i) /\ LSeg(f/^n,j) = {};
hence thesis;
end;
suppose that
A5: i <> 0 and
A6: j+1 <= len(f/^n);
A7: i <= j by A3,NAT_1:13;
1 <= i by A5,NAT_1:14;
then
A8: 1 <= j by A7,XXREAL_0:2;
n+(i+1) < n+j by A3,XREAL_1:6;
then n+i+1 < n+j;
then
A9: LSeg(f,n+i) misses LSeg(f,n+j) by A1;
A10: len(f/^n) = len f - n by A2,RFINSEQ:def 1;
j <= j+1 by NAT_1:11;
then i+1 < j+1 by A3,XXREAL_0:2;
then i+1 <= len(f/^n) by A6,XXREAL_0:2;
then
LSeg(f/^n,i) /\ LSeg(f/^n,j) = LSeg(f,n+i) /\ LSeg(f/^n,j) by A5,A10
,Th5,NAT_1:14
.= {} by A9,A6,A10,A8,Th5;
hence thesis;
end;
end;
hence thesis;
end;
suppose
n > len f;
then f/^n = <*>(the carrier of TOP-REAL 2) by RFINSEQ:def 1;
then len(f/^n) = 0;
hence thesis by Th33;
end;
end;
registration
let f be s.n.c. FinSequence of TOP-REAL 2, n;
cluster f|n -> s.n.c. for FinSequence of TOP-REAL 2;
coherence by Lm7;
cluster f/^n -> s.n.c. for FinSequence of TOP-REAL 2;
coherence by Lm8;
end;
Lm9: f is s.n.c. implies f-:p is s.n.c.
proof
f-:p = f|(p..f) by FINSEQ_5:def 1;
hence thesis;
end;
registration
let f be s.n.c. FinSequence of TOP-REAL 2, p;
cluster f-:p -> s.n.c.;
coherence by Lm9;
end;
theorem Th34:
p in rng f & f is s.n.c. implies f:-p is s.n.c.
proof
assume p in rng f;
then ex i being Element of NAT st i+1 = p..f & f:-p = f/^i by FINSEQ_5:49;
hence thesis;
end;
theorem Th35:
f is s.n.c. implies Rev f is s.n.c.
proof
assume
A1: f is s.n.c.;
let i,j be Nat such that
A2: i+1 < j;
per cases;
suppose
A3: i = 0 or j+1 > len(Rev f);
now
per cases by A3;
case
i = 0;
hence LSeg(Rev f,i) = {} by TOPREAL1:def 3;
end;
case
j+1 > len(Rev f);
hence LSeg(Rev f,j) = {} by TOPREAL1:def 3;
end;
end;
then LSeg(Rev f,i) /\ LSeg(Rev f,j) = {};
hence thesis;
end;
suppose that
i <> 0 and
A4: j+1 <= len(Rev f);
A5: j <= j+1 by NAT_1:11;
i <= i+1 by NAT_1:11;
then
A6: i < j by A2,XXREAL_0:2;
A7: len Rev f = len f by FINSEQ_5:def 3;
then reconsider j9 = len f - j as Element of NAT by A4,A5,INT_1:5
,XXREAL_0:2;
j <= len f by A4,A7,A5,XXREAL_0:2;
then reconsider i9 = len f - i as Element of NAT by A6,INT_1:5,XXREAL_0:2;
A8: j9+j = len f;
len f - (i+1) > j9 by A2,XREAL_1:10;
then i9 - 1 + 1 > j9+1 by XREAL_1:6;
then
A9: LSeg(f,i9) misses LSeg(f,j9) by A1;
i9+i = len f;
hence LSeg(Rev f,i) /\ LSeg(Rev f,j) = LSeg(f,i9) /\ LSeg(Rev f,j) by Th2
.= {} by A9,A8,Th2;
end;
end;
theorem Th36:
f is s.n.c. & g is s.n.c. & L~f misses L~g & (for i st 1<=i & i+
2 <= len f holds LSeg(f,i) misses LSeg(f/.len f,g/.1)) & (for i st 2<=i & i+1
<= len g holds LSeg(g,i) misses LSeg(f/.len f,g/.1)) implies f^g is s.n.c.
proof
assume that
A1: f is s.n.c. and
A2: g is s.n.c. and
A3: L~f /\ L~g = {} and
A4: for i st 1<=i & i+2<= len f holds LSeg(f,i) misses LSeg(f/.len f,g/. 1) and
A5: for i st 2<=i & i+1 <= len g holds LSeg(g,i) misses LSeg(f/.len f,g /.1);
let i,j be Nat such that
A6: i+1 < j;
per cases;
suppose
A7: i = 0 or j+1 > len(f^g);
now
per cases by A7;
case
i = 0;
hence LSeg(f^g,i) = {} by TOPREAL1:def 3;
end;
case
j+1 > len(f^g);
hence LSeg(f^g,j) = {} by TOPREAL1:def 3;
end;
end;
then LSeg(f^g,i) /\ LSeg(f^g,j) = {};
hence thesis;
end;
suppose that
A8: i <> 0 and
A9: j+1 <= len(f^g);
A10: len(f^g) = len f + len g by FINSEQ_1:22;
i <= i+1 by NAT_1:11;
then
A11: i < j by A6,XXREAL_0:2;
A12: 1 <= i by A8,NAT_1:14;
now
per cases;
suppose
A13: j+1 <= len f;
j <= j+1 by NAT_1:11;
then i < j+1 by A11,XXREAL_0:2;
then i < len f by A13,XXREAL_0:2;
then i+1 <= len f by NAT_1:13;
then
A14: LSeg(f^g,i) = LSeg(f,i) by Th6;
LSeg(f^g,j) = LSeg(f,j) by A13,Th6;
hence thesis by A1,A6,A14;
end;
suppose
j+1 > len f;
then
A15: len f <= j by NAT_1:13;
then reconsider j9 = j - len f as Element of NAT by INT_1:5;
j+1-len f <= len g by A9,A10,XREAL_1:20;
then
A16: j9+1 <= len g;
A17: len f + j9 = j;
now
per cases;
suppose
A18: i <= len f;
then
A19: f is non empty by A12;
now
per cases;
suppose
A20: i = len f;
g is non empty by A16;
then
A21: LSeg(f^g,i) = LSeg(f/.len f,g/.1) by A19,A20,Th8;
len f +1+1 <= j by A6,A20,NAT_1:13;
then len f +(1+1) <= j;
then
A22: 1+1 <= j9 by XREAL_1:19;
then LSeg(f^g,j) = LSeg(g,j9) by A17,Th7,XXREAL_0:2;
hence thesis by A5,A16,A22,A21;
end;
suppose
i <> len f;
then i < len f by A18,XXREAL_0:1;
then i+1 <= len f by NAT_1:13;
then
A23: LSeg(f^g,i) = LSeg(f,i) by Th6;
now
per cases;
suppose
A24: j = len f;
then i+1+1 <= len f by A6,NAT_1:13;
then
A25: i+(1+1) <= len f;
g is non empty by A9,A10,A24,XREAL_1:6;
then
A26: LSeg(f^g,j) = LSeg(f/.len f,g/.1) by A19,A24,Th8;
thus thesis by A4,A8,A23,A25,A26,NAT_1:14;
end;
suppose
j <> len f;
then len f < j by A15,XXREAL_0:1;
then len f+1 <= j by NAT_1:13;
then 1 <= j9 by XREAL_1:19;
then LSeg(f^g,len f+j9) = LSeg(g,j9) by Th7;
then
A27: LSeg(f^g,j) c= L~g by TOPREAL3:19;
LSeg(f^g,i) c= L~f by A23,TOPREAL3:19;
then LSeg(f^g,i) /\ LSeg(f^g,j) = {} by A3,A27,XBOOLE_1:3
,27;
hence thesis;
end;
end;
hence thesis;
end;
end;
hence thesis;
end;
suppose
A28: i > len f;
then j <> len f by A6,NAT_1:13;
then len f < j by A15,XXREAL_0:1;
then len f+1 <= j by NAT_1:13;
then 1 <= j9 by XREAL_1:19;
then
A29: LSeg(f^g,len f+j9) = LSeg(g,j9) by Th7;
reconsider i9 = i - len f as Element of NAT by A28,INT_1:5;
len f + 1 <= i by A28,NAT_1:13;
then 1 <= i9 by XREAL_1:19;
then
A30: LSeg(f^g,len f+i9) = LSeg(g,i9) by Th7;
i+1-len f < j9 by A6,XREAL_1:9;
then i9+1 < j9;
hence thesis by A2,A30,A29;
end;
end;
hence thesis;
end;
end;
hence thesis;
end;
end;
theorem Th37:
f is unfolded s.n.c. & p in LSeg(f,n) & not p in rng f implies
Ins(f,n,p) is s.n.c.
proof
assume that
A1: f is unfolded and
A2: f is s.n.c. and
A3: p in LSeg(f,n) and
A4: not p in rng f;
set fp = Ins(f,n,p);
let i,j be Nat such that
A5: i+1 < j;
per cases;
suppose
A6: i = 0 or j+1 > len fp;
now
per cases by A6;
case
i = 0;
hence LSeg(fp,i) = {} by TOPREAL1:def 3;
end;
case
j+1 > len fp;
hence LSeg(fp,j) = {} by TOPREAL1:def 3;
end;
end;
then LSeg(fp,i) /\ LSeg(fp,j) = {};
hence thesis;
end;
suppose that
A7: i <> 0 and
A8: j+1 <= len fp;
A9: 1 <= i by A7,NAT_1:14;
set f1 = f|n, g1 = f1^<*p*>, f2 = f/^n;
A10: fp = g1^f2 by FINSEQ_5:def 4;
i <= i+1 by NAT_1:11;
then
A11: i < j by A5,XXREAL_0:2;
A12: i+1 <= i+1+1 by NAT_1:11;
A13: len fp = len f + 1 by FINSEQ_5:69;
A14: 1 <= n by A3,TOPREAL1:def 3;
A15: n+1 <= len f by A3,TOPREAL1:def 3;
A16: len g1 = len f1 + 1 by FINSEQ_2:16;
then
A17: g1/.len g1 = p by FINSEQ_4:67;
A18: n <= n+1 by NAT_1:11;
then
A19: n <= len f by A15,XXREAL_0:2;
A20: len f1 = n by A15,A18,FINSEQ_1:59,XXREAL_0:2;
i+1+1 <= j by A5,NAT_1:13;
then i+1+1+1 <= j+1 by XREAL_1:6;
then
A21: i+1+1+1 <= len f + 1 by A8,A13,XXREAL_0:2;
then i+1+1 <= len f by XREAL_1:6;
then
A22: i+1 <= len f by A12,XXREAL_0:2;
now
per cases;
suppose
A23: j+1 <= n;
then
A24: LSeg(fp,j) = LSeg(g1,j) by A10,A16,A18,A20,Th6,XXREAL_0:2
.= LSeg(f1,j) by A20,A23,Th6
.= LSeg(f,j) by A20,A23,Th3;
j <= j+1 by NAT_1:11;
then i < j+1 by A11,XXREAL_0:2;
then i < n by A23,XXREAL_0:2;
then
A25: i+1 <= n by NAT_1:13;
then LSeg(fp,i) = LSeg(g1,i) by A10,A16,A18,A20,Th6,XXREAL_0:2
.= LSeg(f1,i) by A20,A25,Th6
.= LSeg(f,i) by A20,A25,Th3;
hence thesis by A2,A5,A24;
end;
suppose
j+1 > n;
then
A26: n <= j by NAT_1:13;
now
per cases;
suppose
A27: i <= n+1;
A28: 1 <= n+1 by NAT_1:11;
1 <= len f - n by A15,XREAL_1:19;
then 1 <= len f2 by A19,RFINSEQ:def 1;
then 1 in dom f2 by FINSEQ_3:25;
then
A29: f/.(n+1) = f2/.1 by FINSEQ_5:27;
len g1 in dom g1 by FINSEQ_5:6;
then
A30: fp/.(n+1) = g1/.len g1 by A10,A16,A20,FINSEQ_4:68;
Z1: n+1 in dom f by A15,A28,FINSEQ_3:25;
Z2: n+1+1 >= 1 by NAT_1:11;
n+1+1 <= len f + 1 by A15,XREAL_1:6; then
n+1+1 <= len fp by A13; then
n+1+1 in dom fp by Z2,FINSEQ_3:25; then
A31: fp/.(n+1+1) = fp.(n+1+1) by PARTFUN1:def 6
.= f.(n+1) by A15,FINSEQ_5:74
.= f/.(n+1) by Z1,PARTFUN1:def 6;
A32: n in dom f1 by A14,A20,FINSEQ_3:25;
then
A33: f/.n = f1/.len f1 by A20,FINSEQ_4:70;
n+1+1 <= len fp by A13,A15,XREAL_1:6;
then
A34: LSeg(fp,n+1) = LSeg(p,f2/.1) by A17,A29,A31,A28,A30,TOPREAL1:def 3;
A35: f1/.len f1 = g1/.len f1 by A20,A32,FINSEQ_4:68;
A36: LSeg(fp,n) = LSeg(g1,n) by A10,A16,A20,Th6
.= LSeg(f1/.len f1,p) by A16,A17,A14,A20,A35,TOPREAL1:def 3;
A37: LSeg(f,n) = LSeg(f/.n,f/.(n+1)) by A14,A15,TOPREAL1:def 3;
then
A38: LSeg(f1/.len f1,p) \/ LSeg(g1/.len g1,f2/.1) = LSeg(f1/.len
f1,f2/.1) by A3,A17,A33,A29,TOPREAL1:5;
A39: LSeg(f1/.len f1,p) /\ LSeg(p,f2/.1) = {p} by A3,A37,A33,A29,
TOPREAL1:8;
now
per cases by XXREAL_0:1;
suppose
i < n;
then
A40: i+1 <= n by NAT_1:13;
then
A41: LSeg(fp,i) = LSeg(g1,i) by A10,A16,A18,A20,Th6,XXREAL_0:2
.= LSeg(f1,i) by A20,A40,Th6
.= LSeg(f,i) by A20,A40,Th3;
now
per cases;
suppose
A42: j = n;
then
A43: LSeg(f,i) misses LSeg(f,n) by A2,A5;
LSeg(fp,i) /\ LSeg(fp,j) c= LSeg(f,i) /\ LSeg(f,n) by A37
,A33,A29,A38,A36,A41,A42,XBOOLE_1:7,26;
then LSeg(fp,i) /\ LSeg(fp,j) c= {} by A43;
then LSeg(fp,i) /\ LSeg(fp,j) = {} by XBOOLE_1:3;
hence thesis;
end;
suppose
j <> n;
then n < j by A26,XXREAL_0:1;
then
A44: n+1 <= j by NAT_1:13;
now
per cases;
suppose
A45: j = n+1;
now
per cases;
suppose
A46: i+1 = n;
A47: i+(1+1) <= len f by A21,XREAL_1:6;
LSeg(fp,i) = LSeg( g1,i) by A10,A16,A20,A46,Th6,
NAT_1:11
.= LSeg(f1,i) by A20,A46,Th6
.= LSeg(f,i) by A20,A46,Th3;
then
A48: LSeg(fp,i) /\ LSeg (f,n) = {f/.n} by A1,A9,A46,A47;
assume not thesis;
then consider x being object such that
A49: x in LSeg(fp,i) /\ LSeg(fp,j) by XBOOLE_0:4;
A50: x in LSeg(fp,i) by A49,XBOOLE_0:def 4;
A51: x in LSeg(fp,j) by A49,XBOOLE_0:def 4;
then
x in LSeg(f,n) by A17,A37,A33,A29,A38,A34,A45,
XBOOLE_0:def 3;
then x in {f/.n} by A48,A50,XBOOLE_0:def 4;
then
A52: x = f/.n by TARSKI:def 1;
then x in LSeg(fp,n) by A33,A36,RLTOPSP1:68;
then x in LSeg(fp,n) /\ LSeg(fp,n+1) by A45,A51,
XBOOLE_0:def 4;
then
A53: p = f/.n by A36,A34,A39,A52,TARSKI:def 1;
n in dom f by A14,A15,SEQ_4:134;
hence contradiction by A4,A53,PARTFUN2:2;
end;
suppose
i+1 <> n;
then i+1 < n by A40,XXREAL_0:1;
then
A54: LSeg(f,i) misses LSeg(f,n) by A2;
LSeg(fp,i) /\ LSeg(fp,j) c= LSeg(f,i) /\ LSeg
(f,n) by A17,A37,A33,A29,A38,A34,A41,A45,XBOOLE_1:7,26;
then LSeg(fp,i) /\ LSeg(fp,j) c= {} by A54;
then LSeg(fp,i) /\ LSeg(fp,j) = {} by XBOOLE_1:3;
hence thesis;
end;
end;
hence thesis;
end;
suppose
A55: j <> n+1;
reconsider nj = j-(n+1) as Element of NAT by A44,
INT_1:5;
A56: n+1 < j by A44,A55,XXREAL_0:1;
then n+1+1 <= j by NAT_1:13;
then
A57: 1 <= nj by XREAL_1:19;
reconsider j9 = j - 1 as Element of NAT by A9,A11,
INT_1:5,XXREAL_0:2;
A58: n+nj = j9;
i+1+1 <= n+1 by A40,XREAL_1:6;
then i+1+1 < j by A56,XXREAL_0:2;
then
A59: i+1 < j9 by XREAL_1:20;
j = nj+(n+1);
then LSeg(fp,j) = LSeg(f2,nj) by A10,A16,A20,A57,Th7
.= LSeg(f,j9) by A19,A57,A58,Th4;
hence thesis by A2,A41,A59;
end;
end;
hence thesis;
end;
end;
hence thesis;
end;
suppose
A60: i = n;
then reconsider nj = j-(n+1) as Element of NAT by A5,INT_1:5;
A61: n+1+1 <= j by A5,A60,NAT_1:13;
then
A62: 1 <= nj by XREAL_1:19;
reconsider j9 = j - 1 as Element of NAT by A9,A11,INT_1:5
,XXREAL_0:2;
A63: n+nj = j9;
j = nj+(n+1);
then
A64: LSeg(fp,j) = LSeg(f2,nj) by A10,A16,A20,A62,Th7
.= LSeg(f,j9) by A19,A62,A63,Th4;
now
per cases;
suppose
j <> n+1+1;
then n+1+1 < j by A61,XXREAL_0:1;
then i+1 < j9 by A60,XREAL_1:20;
then
A65: LSeg(f,i) misses LSeg(f,j9) by A2;
LSeg(fp,i) /\ LSeg(fp,j) c= LSeg(f,i) /\ LSeg(f,j9)
by A37,A33,A29,A38,A36,A60,A64,XBOOLE_1:7,26;
then LSeg(fp,i) /\ LSeg(fp,j) c= {} by A65;
then LSeg(fp,i) /\ LSeg(fp,j) = {} by XBOOLE_1:3;
hence thesis;
end;
suppose
A66: j = n+1+1;
then n+(1+1) <= len f by A8,A13,XREAL_1:6;
then
A67: LSeg(f,n) /\ LSeg(f,j9) = {f/.j9} by A1,A14,A66;
assume not thesis;
then consider x being object such that
A68: x in LSeg(fp,i) /\ LSeg(fp,j) by XBOOLE_0:4;
A69: x in LSeg(fp,j) by A68,XBOOLE_0:def 4;
A70: x in LSeg(fp,i) by A68,XBOOLE_0:def 4;
then x in LSeg(f,n) by A37,A33,A29,A38,A36,A60,
XBOOLE_0:def 3;
then x in {f/.(n+1)} by A64,A66,A67,A69,XBOOLE_0:def 4;
then
A71: x = f/.(n+1) by TARSKI:def 1;
then x in LSeg(fp,n+1) by A29,A34,RLTOPSP1:68;
then x in LSeg(fp,n) /\ LSeg(fp,n+1) by A60,A70,
XBOOLE_0:def 4;
then
A72: p = f/.(n+1) by A36,A34,A39,A71,TARSKI:def 1;
n+1 in dom f by A14,A15,SEQ_4:134;
hence contradiction by A4,A72,PARTFUN2:2;
end;
end;
hence thesis;
end;
suppose
A73: i>n;
reconsider j9 = j - 1 as Element of NAT by A9,A11,INT_1:5
,XXREAL_0:2;
i>=n+1 by A73,NAT_1:13;
then
A74: i = n+1 by A27,XXREAL_0:1;
then n+1 < j9 by A5,XREAL_1:20;
then
A75: LSeg(f,n) misses LSeg(f,j9) by A2;
n+1 <= n+1+1 by NAT_1:11;
then reconsider nj = j-(n+1) as Element of NAT by A5,A74,
INT_1:5,XXREAL_0:2;
A76: 1 <= nj by A5,A74,XREAL_1:19;
A77: n+nj = j9;
j = nj+(n+1);
then LSeg(fp,j) = LSeg(f2,nj) by A10,A16,A20,A76,Th7
.= LSeg(f,j9) by A19,A76,A77,Th4;
then LSeg(fp,n+1) /\ LSeg(fp,j) c= LSeg(f,n) /\ LSeg(f,j9) by
A17,A37,A33,A29,A38,A34,XBOOLE_1:7,26;
then LSeg(fp,n+1) /\ LSeg(fp,j) c= {} by A75;
then LSeg(fp,n+1) /\ LSeg(fp,j) = {} by XBOOLE_1:3;
hence thesis by A74;
end;
end;
hence thesis;
end;
suppose
A78: i > n+1;
then reconsider nj = j-(n+1) as Element of NAT by A11,INT_1:5
,XXREAL_0:2;
n+1 < j by A11,A78,XXREAL_0:2;
then n+1+1 <= j by NAT_1:13;
then
A79: 1 <= nj by XREAL_1:19;
reconsider ni = i - (n+1) as Element of NAT by A78,INT_1:5;
n+1+1 <= i by A78,NAT_1:13;
then
A80: 1 <= ni by XREAL_1:19;
len f <= len f+1 by NAT_1:11;
then i+1 <= len f+1 by A22,XXREAL_0:2;
then i+1-(n+1) <= len f+1- (n+1) by XREAL_1:9;
then
A81: ni+1 <= len f - n;
reconsider i9 = i - 1 as Element of NAT by A7,INT_1:5,NAT_1:14;
reconsider j9 = j - 1 as Element of NAT by A9,A11,INT_1:5
,XXREAL_0:2;
A82: n+ni = i9;
i+1-1 < j9 by A5,XREAL_1:9;
then
A83: i9+1 < j9;
A84: n+nj = j9;
j = nj+(n+1);
then
A85: LSeg(fp,j) = LSeg(f2,nj) by A10,A16,A20,A79,Th7
.= LSeg(f,j9) by A19,A79,A84,Th4;
i = ni+(n+1);
then LSeg(fp,i) = LSeg(f2,ni) by A10,A16,A20,A80,Th7
.= LSeg(f,i9) by A80,A81,A82,Th5;
hence thesis by A2,A83,A85;
end;
end;
hence thesis;
end;
end;
hence thesis;
end;
end;
registration
cluster <*>(the carrier of TOP-REAL 2) -> special;
coherence;
end;
registration
let p;
cluster <*p*> -> special for FinSequence of TOP-REAL 2;
coherence
proof
set f = <*p*>;
f is special
proof
let i be Nat such that
A1: 1 <= i and
A2: i+1 <= len f;
len f = 0+1 by FINSEQ_1:39;
hence thesis by A1,A2,XREAL_1:6;
end;
hence thesis;
end;
end;
theorem Th38:
p`1 = q`1 or p`2 = q`2 implies <*p,q*> is special
proof
assume
A1: p`1 = q`1 or p`2 = q`2;
set f = <*p,q*>;
let i be Nat such that
A2: 1 <= i and
A3: i+1 <= len f;
len f = 1+1 by FINSEQ_1:44;
then i <= 1 by A3,XREAL_1:6;
then
A4: i = 1 by A2,XXREAL_0:1;
then f/.i = p by FINSEQ_4:17;
hence thesis by A1,A4,FINSEQ_4:17;
end;
Lm10: f is special implies f|n is special
proof
assume
A1: f is special;
let i be Nat such that
A2: 1 <= i and
A3: i+1 <= len(f|n);
i in dom(f|n) by A2,A3,SEQ_4:134;
then
A4: (f|n)/.i = f/.i by FINSEQ_4:70;
i+1 in dom(f|n) by A2,A3,SEQ_4:134;
then
A5: (f|n)/.(i+1) = f/.(i+1) by FINSEQ_4:70;
len(f|n) <= len f by FINSEQ_5:16;
then i+1 <= len f by A3,XXREAL_0:2;
hence thesis by A1,A2,A4,A5;
end;
Lm11: f is special implies f/^n is special
proof
assume
A1: f is special;
per cases;
suppose
A2: n <= len f;
let i be Nat such that
A3: 1 <= i and
A4: i+1 <= len(f/^n);
i in dom(f/^n) by A3,A4,SEQ_4:134;
then
A5: (f/^n)/.i = f/.(n+i) by FINSEQ_5:27;
i <= n+i by NAT_1:11;
then
A6: 1 <= n+i by A3,XXREAL_0:2;
i+1 in dom(f/^n) by A3,A4,SEQ_4:134;
then
A7: (f/^n)/.(i+1) = f/.(n+(i+1)) by FINSEQ_5:27
.= f/.(n+i+1);
len(f/^n) = len f - n by A2,RFINSEQ:def 1;
then n+(i+1) <= len f by A4,XREAL_1:19;
hence thesis by A1,A5,A7,A6;
end;
suppose
n > len f;
then f/^n = <*>(the carrier of TOP-REAL 2) by RFINSEQ:def 1;
hence thesis;
end;
end;
registration
let f be special FinSequence of TOP-REAL 2, n;
cluster f|n -> special for FinSequence of TOP-REAL 2;
coherence by Lm10;
cluster f/^n -> special for FinSequence of TOP-REAL 2;
coherence by Lm11;
end;
theorem Th39:
p in rng f & f is special implies f:-p is special
proof
assume p in rng f;
then ex i being Element of NAT st i+1 = p..f & f:-p = f/^i by FINSEQ_5:49;
hence thesis;
end;
Lm12: f is special implies f-:p is special
proof
f-:p = f|(p..f) by FINSEQ_5:def 1;
hence thesis;
end;
registration
let f be special FinSequence of TOP-REAL 2, p;
cluster f-:p -> special;
coherence by Lm12;
end;
theorem Th40:
f is special implies Rev f is special
proof
assume
A1: f is special;
A2: len Rev f = len f by FINSEQ_5:def 3;
let i be Nat such that
A3: 1 <= i and
A4: i+1 <= len(Rev f);
i <= i+1 by NAT_1:11;
then reconsider j = len f - i as Element of NAT by A4,A2,INT_1:5,XXREAL_0:2;
j <= len f - 1 by A3,XREAL_1:10;
then
A5: j+1 <= len f - 1 + 1 by XREAL_1:6;
A6: 1+i+j = len f + 1;
A7: i+1-i <= j by A4,A2,XREAL_1:9;
then j in dom f by A5,SEQ_4:134;
then
A8: (Rev f)/.(i+1) = f/.j by A6,FINSEQ_5:66;
A9: i+(j+1) = len f + 1;
j+1 in dom f by A5,A7,SEQ_4:134;
then (Rev f)/.i = f/.(j+1) by A9,FINSEQ_5:66;
hence thesis by A1,A5,A7,A8;
end;
Lm13: f is special & g is special & ((f/.len f)`1 = (g/.1)`1 or (f/.len f)`2 =
(g/.1)`2) implies f^g is special
proof
assume that
A1: f is special and
A2: g is special and
A3: (f/.len f)`1 = (g/.1)`1 or (f/.len f)`2 = (g/.1)`2;
let i be Nat such that
A4: 1 <= i and
A5: i+1 <= len(f^g);
A6: len(f^g) = len f + len g by FINSEQ_1:22;
per cases by XXREAL_0:1;
suppose
i < len f;
then
A7: i+1 <= len f by NAT_1:13;
then i+1 in dom f by A4,SEQ_4:134;
then
A8: (f^g)/.(i+1)=f/.(i+1) by FINSEQ_4:68;
i in dom f by A4,A7,SEQ_4:134;
then (f^g)/.i=f/.i by FINSEQ_4:68;
hence thesis by A1,A4,A7,A8;
end;
suppose
A9: i = len f;
then i in dom f by A4,FINSEQ_3:25;
then
A10: (f^g)/.i = f/.i by FINSEQ_4:68;
1 <= len g by A5,A6,A9,XREAL_1:6;
then 1 in dom g by FINSEQ_3:25;
hence thesis by A3,A9,A10,FINSEQ_4:69;
end;
suppose
A11: i > len f;
then reconsider j = i - len f as Element of NAT by INT_1:5;
len f + 1 <= i by A11,NAT_1:13;
then
A12: 1 <= j by XREAL_1:19;
A13: len f + (j+1) = i+1;
A14: i+1-len f <= len g by A5,A6,XREAL_1:20;
then j+1 in dom g by A12,SEQ_4:134;
then
A15: (f^g)/.(i+1)= g/.(j+1) by A13,FINSEQ_4:69;
A16: len f + j = i;
j+1 <= len g by A14;
then j in dom g by A12,SEQ_4:134;
then (f^g)/.i= g/.j by A16,FINSEQ_4:69;
hence thesis by A2,A12,A14,A15;
end;
end;
theorem Th41:
f is special & p in LSeg(f,n) implies Ins(f,n,p) is special
proof
assume that
A1: f is special and
A2: p in LSeg(f,n);
A3: n+1 <= len f by A2,TOPREAL1:def 3;
then
A4: 1 <= len f - n by XREAL_1:19;
A5: 1 <= n by A2,TOPREAL1:def 3;
then
A6: LSeg(f,n) = LSeg(f/.n,f/.(n+1)) by A3,TOPREAL1:def 3;
set f1 = f|n, g1 = f1^<*p*>, f2 = f/^n;
set p1 = f1/.len f1, p2 = f2/.1;
A7: p1 = |[p1`1, p1`2]| by EUCLID:53;
A8: n <= n+1 by NAT_1:11;
then n <= len f by A3,XXREAL_0:2;
then 1 <= len f2 by A4,RFINSEQ:def 1;
then 1 in dom f2 by FINSEQ_3:25;
then
A9: f/.(n+1) = f2/.1 by FINSEQ_5:27;
A10: len f1 = n by A3,A8,FINSEQ_1:59,XXREAL_0:2;
then n in dom f1 by A5,FINSEQ_3:25;
then
A11: f/.n = f1/.len f1 by A10,FINSEQ_4:70;
then
A12: p1`1 = p2`1 or p1`2 = p2`2 by A1,A5,A3,A9;
set q1 = g1/.len g1;
A13: p2 = |[p2`1, p2`2]| by EUCLID:53;
<*p*>/.1 = p by FINSEQ_4:16;
then p1`1 = (<*p*>/.1)`1 or p1`2 = (<*p*>/.1)`2 by A2,A6,A11,A9,A12,A7,A13,
TOPREAL3:11,12;
then
A14: g1 is special by A1,Lm13;
g1/.len g1 = g1/.(len f1 + 1) by FINSEQ_2:16
.= p by FINSEQ_4:67;
then q1`1 = p2`1 or q1`2 = p2`2 by A2,A6,A11,A9,A12,A7,A13,TOPREAL3:11,12;
then g1^f2 is special by A1,A14,Lm13;
hence thesis by FINSEQ_5:def 4;
end;
theorem Th42:
q in rng f & 1<>q..f & q..f<>len f & f is unfolded s.n.c.
implies L~(f-:q) /\ L~(f:-q) = {q}
proof
assume that
A1: q in rng f and
A2: 1 <> q..f and
A3: q..f <> len f and
A4: f is unfolded and
A5: f is s.n.c.;
A6: (f:-q)/.1 = q by FINSEQ_5:53;
q..f <= len f by A1,FINSEQ_4:21;
then q..f < len f by A3,XXREAL_0:1;
then q..f+1 <= len f by NAT_1:13;
then
A7: 1 <= len f - q..f by XREAL_1:19;
len(f:-q) = len f - q..f + 1 by A1,FINSEQ_5:50;
then 1+1<=len(f:-q) by A7,XREAL_1:6;
then
A8: rng(f:-q) c= L~(f:-q) by Th18;
1 in dom(f:-q) by FINSEQ_5:6;
then
A9: q in rng(f:-q) by A6,PARTFUN2:2;
f-:q is non empty by A1,FINSEQ_5:47;
then
A10: len(f-:q) in dom(f-:q) by FINSEQ_5:6;
A11: len(f-:q) = q..f by A1,FINSEQ_5:42;
thus L~(f-:q) /\ L~(f:-q) c= {q}
proof
let x be object;
assume
A12: x in L~(f-:q) /\ L~(f:-q);
then reconsider p = x as Point of TOP-REAL 2;
p in L~(f-:q) by A12,XBOOLE_0:def 4;
then consider i such that
A13: 1 <= i and
A14: i+1 <= len(f-:q) and
A15: p in LSeg((f-:q),i) by Th13;
A16: LSeg(f-:q,i) = LSeg(f,i) by A14,Th9;
p in L~(f:-q) by A12,XBOOLE_0:def 4;
then consider j such that
A17: 1 <= j and
j+1 <= len(f:-q) and
A18: p in LSeg((f:-q),j) by Th13;
consider j9 being Nat such that
A19: j=j9+1 by A17,NAT_1:6;
reconsider j9 as Element of NAT by ORDINAL1:def 12;
A20: LSeg(f:-q,j) = LSeg(f,j9+q..f) by A1,A19,Th10;
per cases;
suppose that
A21: i+1 = len(f-:q) and
A22: j9 = 0;
q..f <= len f by A1,FINSEQ_4:21;
then q..f < len f by A3,XXREAL_0:1;
then i+1+1 <= len f by A11,A21,NAT_1:13;
then i+(1+1) <= len f;
then LSeg((f-:q),i) /\ LSeg(f:-q,j) = {f/.(q..f)} by A4,A11,A13,A16,A20
,A21,A22
.= {q} by A1,FINSEQ_5:38;
hence thesis by A15,A18,XBOOLE_0:def 4;
end;
suppose that
A23: i+1 = len(f-:q) and
A24: j9 <> 0;
1 <= j9 by A24,NAT_1:14;
then i+1+1 <= j9+q..f by A11,A23,XREAL_1:7;
then i+1 < j9+q..f by NAT_1:13;
then LSeg((f-:q),i) misses LSeg(f:-q,j) by A5,A16,A20;
then LSeg((f-:q),i) /\ LSeg(f:-q,j) = {};
hence thesis by A15,A18,XBOOLE_0:def 4;
end;
suppose
A25: i+1 <> len(f-:q);
A26: q..f <= j9+q..f by NAT_1:11;
i+1 < q..f by A11,A14,A25,XXREAL_0:1;
then i+1 < j9+q..f by A26,XXREAL_0:2;
then LSeg((f-:q),i) misses LSeg(f:-q,j) by A5,A16,A20;
then LSeg((f-:q),i) /\ LSeg(f:-q,j) = {};
hence thesis by A15,A18,XBOOLE_0:def 4;
end;
end;
1 <= q..f by A1,FINSEQ_4:21;
then 1 < q..f by A2,XXREAL_0:1;
then 1+1 <= q..f by NAT_1:13;
then
A27: rng(f-:q) c= L~(f-:q) by A11,Th18;
(f-:q)/.(q..f) = q by A1,FINSEQ_5:45;
then q in rng(f-:q) by A11,A10,PARTFUN2:2;
then q in L~(f-:q) /\ L~(f:-q) by A27,A9,A8,XBOOLE_0:def 4;
hence thesis by ZFMISC_1:31;
end;
theorem Th43:
p <> q & (p`1 = q`1 or p`2 = q`2) implies <*p,q*> is being_S-Seq
by FINSEQ_3:94,FINSEQ_1:44,Lm2,Lm6,Th38;
definition
mode S-Sequence_in_R2 is being_S-Seq FinSequence of TOP-REAL 2;
end;
registration
let f be S-Sequence_in_R2;
cluster Rev f -> being_S-Seq for FinSequence of TOP-REAL 2;
coherence
proof
set g = Rev f;
g is being_S-Seq
proof
thus g is one-to-one;
len g = len f by FINSEQ_5:def 3;
hence len g >= 2 by TOPREAL1:def 8;
thus thesis by Th28,Th35,Th40;
end;
hence thesis;
end;
end;
theorem
for f being S-Sequence_in_R2 st i in dom f holds f/.i in L~f
proof
let f be S-Sequence_in_R2;
len f >= 2 by TOPREAL1:def 8;
hence thesis by GOBOARD1:1;
end;
theorem
p <> q & (p`1 = q`1 or p`2 = q`2) implies LSeg(p,q) is being_S-P_arc
proof
assume that
A1: p <> q and
A2: p`1 = q`1 or p`2 = q`2;
take f = <*p,q*>;
thus f is being_S-Seq by A1,A2,Th43;
thus thesis by Th21;
end;
Lm14: p in rng f implies L~(f-:p) c= L~f
proof
assume p in rng f;
then L~f = L~(f-:p) \/ L~(f:-p) by Th24;
hence thesis by XBOOLE_1:7;
end;
Lm15: p in rng f implies L~(f:-p) c= L~f
proof
assume p in rng f;
then L~f = L~(f-:p) \/ L~(f:-p) by Th24;
hence thesis by XBOOLE_1:7;
end;
theorem Th46:
for f being S-Sequence_in_R2 st p in rng f & p..f <> 1 holds f-:
p is being_S-Seq
proof
let f be S-Sequence_in_R2 such that
A1: p in rng f and
A2: p..f <> 1;
thus f-:p is one-to-one;
1 <= p..f by A1,FINSEQ_4:21;
then 1 < p..f by A2,XXREAL_0:1;
then 1+1 <= p..f by NAT_1:13;
hence len(f-:p) >= 2 by A1,FINSEQ_5:42;
thus thesis;
end;
theorem
for f being S-Sequence_in_R2 st p in rng f & p..f <> len f holds f:-p
is being_S-Seq
proof
let f be S-Sequence_in_R2 such that
A1: p in rng f and
A2: p..f <> len f;
thus f:-p is one-to-one by A1,FINSEQ_5:56;
hereby
p..f <= len f by A1,FINSEQ_4:21;
then p..f < len f by A2,XXREAL_0:1;
then 1 + p..f <= len f by NAT_1:13;
then
A3: len f - p..f >= 1 by XREAL_1:19;
assume len(f:-p) < 2;
then len f - p..f + 1 < 1 + 1 by A1,FINSEQ_5:50;
hence contradiction by A3,XREAL_1:6;
end;
thus thesis by A1,Th27,Th34,Th39;
end;
theorem Th48:
for f being S-Sequence_in_R2 st p in LSeg(f,i) & not p in rng f
holds Ins(f,i,p) is being_S-Seq
proof
let f be S-Sequence_in_R2 such that
A1: p in LSeg(f,i) and
A2: not p in rng f;
set g = Ins(f,i,p);
thus g is one-to-one by A2,FINSEQ_5:76;
len g = len f + 1 by FINSEQ_5:69;
then
A3: len g >= len f by NAT_1:11;
len f >= 2 by TOPREAL1:def 8;
hence len g >= 2 by A3,XXREAL_0:2;
thus g is unfolded by A1,Th32;
thus g is s.n.c. by A1,A2,Th37;
thus thesis by A1,Th41;
end;
begin :: Special Polygons in TOP-REAL 2
registration
cluster being_S-P_arc for Subset of TOP-REAL 2;
existence
proof
set p = |[ 0,0 ]|, q = |[ 1,1 ]|, f = <* p,|[p`1,q`2]|,q *>;
A1: p`2 = 0 by EUCLID:52;
A2: q`1 = 1 by EUCLID:52;
A3: q`2 = 1 by EUCLID:52;
p`1 = 0 by EUCLID:52;
then f is being_S-Seq by A1,A2,A3,TOPREAL3:34;
then L~f is being_S-P_arc;
hence thesis;
end;
end;
theorem
P is_S-P_arc_joining p1,p2 implies P is_S-P_arc_joining p2,p1
proof
given f such that
A1: f is being_S-Seq and
A2: P = L~f and
A3: p1=f/.1 and
A4: p2 = f/.len f;
take g = Rev f;
thus g is being_S-Seq & P = L~g by A1,A2,Th22;
len g = len f by FINSEQ_5:def 3;
hence thesis by A1,A3,A4,FINSEQ_5:65;
end;
definition
let p1,p2;
let P be Subset of TOP-REAL 2;
pred p1,p2 split P means
p1 <> p2 & ex f1,f2 being S-Sequence_in_R2
st p1 = f1/.1 & p1 = f2/.1 & p2 = f1/.len f1 & p2 = f2/.len f2 & L~f1 /\ L~f2 =
{p1,p2} & P = L~f1 \/ L~f2;
end;
theorem Th50:
p1,p2 split P implies p2,p1 split P
proof
assume
A1: p1 <> p2;
given f1,f2 being S-Sequence_in_R2 such that
A2: p1 = f1/.1 and
A3: p1 = f2/.1 and
A4: p2 = f1/.len f1 and
A5: p2 = f2/.len f2 and
A6: L~f1 /\ L~f2 = {p1,p2} and
A7: P = L~f1 \/ L~f2;
thus p2 <> p1 by A1;
reconsider g1 = Rev f1, g2 = Rev f2 as S-Sequence_in_R2;
take g1, g2;
A8: len g2 = len f2 by FINSEQ_5:def 3;
len g1 = len f1 by FINSEQ_5:def 3;
hence
p2 = g1/.1 & p2 = g2/.1 & p1 = g1/.len g1 & p1 = g2/.len g2 by A2,A3,A4,A5,A8
,FINSEQ_5:65;
L~g1 = L~f1 by Th22;
hence thesis by A6,A7,Th22;
end;
Lm16: for f1,f2 being S-Sequence_in_R2 st p1 = f1/.1 & p1 = f2/.1 & p2 = f1/.
len f1 & p2 = f2/.len f2 & L~f1 /\ L~f2 = {p1,p2} & P = L~f1 \/ L~f2 & q <> p1
& q in rng f1 ex g1,g2 being S-Sequence_in_R2 st p1 = g1/.1 & p1 = g2/.1 & q =
g1/.len g1 & q = g2/.len g2 & L~g1 /\ L~g2 = {p1,q} & P = L~g1 \/ L~g2
proof
let f1,f2 be S-Sequence_in_R2 such that
A1: p1 = f1/.1 and
A2: p1 = f2/.1 and
A3: p2 = f1/.len f1 and
A4: p2 = f2/.len f2 and
A5: L~f1 /\ L~f2 = {p1,p2} and
A6: P = L~f1 \/ L~f2 and
A7: q <> p1 and
A8: q in rng f1;
set f19 = Rev(f1:-q);
A9: 1 <= q..f1 by A8,FINSEQ_4:21;
A10: now
assume
A11: 1 = q..f1;
then
A12: 1 in dom f1 by A8,FINSEQ_4:20;
f1.1 = q by A8,A11,FINSEQ_4:19;
hence contradiction by A1,A7,A12,PARTFUN1:def 6;
end;
then reconsider g1 = f1-:q as S-Sequence_in_R2 by A8,Th46;
A13: 1 in dom g1 by FINSEQ_5:6;
1 in dom f2 by FINSEQ_5:6;
then 1 <= len f2 by FINSEQ_3:25;
then reconsider l = len f2 - 1 as Element of NAT by INT_1:5;
set f29 = f2|l;
A14: l+1 = len f2;
rng f19 = rng(f1:-q) by FINSEQ_5:57;
then
A15: rng f19 c= rng f1 by A8,FINSEQ_5:55;
len f2 >= 2 by TOPREAL1:def 8;
then
A16: rng f2 c= L~f2 by Th18;
len f1 >= 2 by TOPREAL1:def 8;
then rng f1 c= L~f1 by Th18;
then
A17: rng f2 /\ rng f1 c= L~f1 /\ L~f2 by A16,XBOOLE_1:27;
set g2 = f29^f19;
A18: dom f29 = Seg len f29 by FINSEQ_1:def 3;
len(f1:-q) >= 1 by NAT_1:14;
then
A19: len f19 >= 1 by FINSEQ_5:def 3;
then
A20: len f19 in dom f19 & 1 in dom f19 by FINSEQ_3:25;
A21: l < len f2 by XREAL_1:44;
then
A22: len f29 = l by FINSEQ_1:59;
len f2 >= 2 by TOPREAL1:def 8;
then
A23: len f2 - 1 >= 1+1-1 by XREAL_1:9;
then
A24: l in dom f29 by A22,FINSEQ_3:25;
then
A25: f29/.len f29 = f2/.l by A22,FINSEQ_4:70;
A26: f19/.1 = (f1:-q)/.len(f1:-q) by FINSEQ_5:65
.= f2/.len f2 by A3,A4,A8,FINSEQ_5:54;
then
A27: LSeg(f29/.len f29,f19/.1) = LSeg(f2,l) by A23,A14,A25,TOPREAL1:def 3;
A28: now
let i such that
1<=i and
A29: i+2<=len f29;
i+1+1 <= len f29 by A29;
then
A30: i+1 < len f29 by NAT_1:13;
then LSeg(f29,i) = LSeg(f2,i) by Th3;
hence LSeg(f29,i) misses LSeg(f29/.len f29,f19/.1) by A22,A27,A30,
TOPREAL1:def 7;
end;
A31: 1 in dom f1 by FINSEQ_5:6;
A32: now
A33: 1 + 1 <= len f1 by TOPREAL1:def 8;
p1 in LSeg(f1/.1,f1/.(1+1)) by A1,RLTOPSP1:68;
then
A34: p1 in LSeg(f1,1) by A33,TOPREAL1:def 3;
assume p1 in L~f19;
then
A35: p1 in L~(f1:-q) by Th22;
then consider i such that
A36: 1 <= i and
i+1 <= len(f1:-q) and
A37: p1 in LSeg(f1:-q,i) by Th13;
consider j be Nat such that
A38: i = j+1 by A36,NAT_1:6;
A39: 1 < q..f1 by A10,A9,XXREAL_0:1;
reconsider j as Element of NAT by ORDINAL1:def 12;
A40: LSeg(f1:-q,i) = LSeg(f1,j+q..f1) by A8,A38,Th10;
then p1 in LSeg(f1,1) /\ LSeg(f1,j+q..f1) by A37,A34,XBOOLE_0:def 4;
then
A41: LSeg(f1,1) meets LSeg(f1,j+q..f1);
per cases;
suppose
A42: j = 0;
A43: 1+1 <= q..f1 by A39,NAT_1:13;
now
per cases by A43,XXREAL_0:1;
suppose
A44: q..f1 = 2;
A45: q..f1 <= len f1 by A8,FINSEQ_4:21;
now
per cases by A44,A45,XXREAL_0:1;
suppose
len f1 = 2;
then len(f1:-q) = len f1 - len f1 + 1 by A8,A44,FINSEQ_5:50;
hence contradiction by A35,TOPREAL1:22;
end;
suppose
len f1 > 2;
then 1+2 <= len f1 by NAT_1:13;
then LSeg(f1,1) /\ LSeg(f1,1+1) = {f1/.(1+1)} by TOPREAL1:def 6;
then p1 in {f1/.2} by A37,A34,A40,A42,A44,XBOOLE_0:def 4;
then
A46: p1 = f1/.2 by TARSKI:def 1;
2 in dom f1 by A8,A44,FINSEQ_4:20;
hence contradiction by A1,A31,A46,PARTFUN2:10;
end;
end;
hence contradiction;
end;
suppose
q..f1 > 2;
then 1+1 < j+q..f1 by A42;
hence contradiction by A41,TOPREAL1:def 7;
end;
end;
hence contradiction;
end;
suppose
j <> 0;
then 1+1 < j+q..f1 by A39,NAT_1:14,XREAL_1:8;
hence contradiction by A41,TOPREAL1:def 7;
end;
end;
A47: now
let i such that
A48: 2<=i and
A49: i+1 <= len f19;
reconsider m = len f19-(i+1) as Element of NAT by A49,INT_1:5;
m+1+i = len(f1:-q) by FINSEQ_5:def 3;
then
A50: LSeg(f19,i) = LSeg(f1:-q,m+1) by Th2
.= LSeg(f1,m+q..f1) by A8,Th10;
then
A51: LSeg(f19,i) c= L~f1 by TOPREAL3:19;
A52: now
A53: len f1 >= 1+1 by TOPREAL1:def 8;
then reconsider k = len f1 - 1 as Element of NAT by INT_1:5,XXREAL_0:2;
A54: p2 in LSeg(f1/.k,f1/.len f1) by A3,RLTOPSP1:68;
A55: k+1 = len f1;
then 1 <= k by A53,XREAL_1:6;
then
A56: p2 in LSeg(f1,k) by A55,A54,TOPREAL1:def 3;
A57: len f19 = len(f1:-q) by FINSEQ_5:def 3;
A58: len f1 - i = len f1 - q..f1 + 1 - 1 + q..f1 - i
.= len f19 - 1 + q..f1 - i by A8,A57,FINSEQ_5:50
.= m + q..f1;
per cases;
suppose
A59: i = 1+1;
A60: q..f1 <= m+q..f1 by NAT_1:11;
1 <= q..f1 by A8,FINSEQ_4:21;
then
A61: 1 <= m + q..f1 by A60,XXREAL_0:2;
assume
A62: p2 in LSeg(f19,i);
A63: m+q..f1+(1+1) = len f1 by A58,A59;
A64: 1 <= k by A53,XREAL_1:19;
p2 in LSeg(f1/.k,f1/.(k+1)) by A3,RLTOPSP1:68;
then
A65: p2 in LSeg(f1,k) by A64,TOPREAL1:def 3;
m + q..f1 + 1 = k by A58,A59;
then LSeg(f1,m + q..f1) /\ LSeg(f1,k) = {f1/.k} by A61,A63,
TOPREAL1:def 6;
then p2 in {f1/.k} by A50,A65,A62,XBOOLE_0:def 4;
then
A66: f1/.len f1 = f1/.k by A3,TARSKI:def 1;
k <= len f1 by A55,NAT_1:11;
then
A67: k in dom f1 by A64,FINSEQ_3:25;
len f1 in dom f1 by FINSEQ_5:6;
then len f1 - k = len f1 - len f1 by A67,A66,PARTFUN2:10
.= 0;
hence contradiction;
end;
suppose
i <> 2;
then 2 < i by A48,XXREAL_0:1;
then 2+1 <= i by NAT_1:13;
then len f1 - i <= len f1 - (1+2) by XREAL_1:10;
then len f1 - i <= len f1 - 1 - 2;
then
A68: len f1 - i + (1+1) <= k by XREAL_1:19;
len f1 - i + (1+1) = m + q..f1 + 1 + 1 by A58;
then m+q..f1 +1 < k by A68,NAT_1:13;
then LSeg(f1,k) misses LSeg(f1,m+q..f1) by TOPREAL1:def 7;
then LSeg(f1,k) /\ LSeg(f1,m+q..f1) = {};
hence not p2 in LSeg(f19,i) by A50,A56,XBOOLE_0:def 4;
end;
end;
LSeg(f19,i) c= L~f19 by TOPREAL3:19;
then
A69: not p1 in LSeg(f19,i) by A32;
LSeg(f29/.len f29,f19/.1) c=L~f2 by A27,TOPREAL3:19;
then
A70: LSeg(f29/.len f29,f19/.1) /\ LSeg(f19,i) c= {p1,p2} by A5,A51,XBOOLE_1:27;
now
given x being object such that
A71: x in LSeg(f29/.len f29,f19/.1) /\ LSeg(f19,i);
x = p1 or x = p2 by A70,A71,TARSKI:def 2;
hence contradiction by A69,A52,A71,XBOOLE_0:def 4;
end;
then LSeg(f19,i) /\ LSeg(f29/.len f29,f19/.1) = {} by XBOOLE_0:def 1;
hence LSeg(f19,i) misses LSeg(f29/.len f29,f19/.1);
end;
A72: now
assume len f19 <> 1;
then 1 < len f19 by A19,XXREAL_0:1;
then
A73: 1+1 <= len f19 by NAT_1:13;
now
let x be object;
hereby
reconsider m = len f19-2 as Element of NAT by A73,INT_1:5;
LSeg(f19,1) c= L~f19 by TOPREAL3:19;
then not p1 in LSeg(f19,1) by A32;
then
A74: not p1 in LSeg(f29/.len f29,f19/.1) /\ LSeg(f19,1) by XBOOLE_0:def 4;
m+1+1 = len(f1:-q) by FINSEQ_5:def 3;
then LSeg(f19,1) = LSeg(f1:-q,m+1) by Th2
.= LSeg(f1,m+q..f1) by A8,Th10;
then
A75: LSeg(f19,1) c= L~f1 by TOPREAL3:19;
LSeg(f29/.len f29,f19/.1) c=L~f2 by A27,TOPREAL3:19;
then
A76: LSeg(f29/.len f29,f19/.1) /\ LSeg(f19,1) c= {p1,p2} by A5,A75,
XBOOLE_1:27;
assume x in LSeg(f29/.len f29,f19/.1) /\ LSeg(f19,1);
hence x = f19/.1 by A4,A26,A76,A74,TARSKI:def 2;
end;
assume
A77: x = f19/.1;
then x in LSeg(f19/.1,f19/.(1+1)) by RLTOPSP1:68;
then
A78: x in LSeg(f19,1) by A73,TOPREAL1:def 3;
x in LSeg(f29/.len f29,f19/.1) by A77,RLTOPSP1:68;
hence x in LSeg(f29/.len f29,f19/.1) /\ LSeg(f19,1) by A78,XBOOLE_0:def 4
;
end;
hence LSeg(f29/.len f29,f19/.1) /\ LSeg(f19,1) = {f19/.1} by TARSKI:def 1;
end;
A79: len f29 >= 1 by A21,A23,FINSEQ_1:59;
then
A80: f29 is non empty;
f1:-q is unfolded by A8,Th27;
then
A81: f19 is unfolded by Th28;
A82: now
per cases;
suppose
len f29 = 1 & len f19 = 1;
then len g2 = 1+1 by FINSEQ_1:22;
hence g2 is unfolded by Th26;
end;
suppose that
A83: len f29 <> 1 and
A84: len f19 = 1;
consider k be Nat such that
A85: k+1 = len f29 by A79,NAT_1:6;
reconsider k as Element of NAT by ORDINAL1:def 12;
A86: LSeg(f29,k) = LSeg(f2,k) by A85,Th3;
len f29 > 1 by A22,A23,A83,XXREAL_0:1;
then
A87: 1 <= k by A85,NAT_1:13;
A88: f19 = <*f19.1*> by A84,FINSEQ_5:14 .= <*f19/.1*> by PARTFUN1:def 6,A20;
k+(1+1) <= len f2 by A22,A85;
then LSeg(f29,k) /\ LSeg(f29/.len f29,f19/.1) = {f29/.len f29} by A22,A25
,A27,A85,A87,A86,TOPREAL1:def 6;
hence g2 is unfolded by A85,A88,Th30;
end;
suppose that
A89: len f29 = 1 and
A90: len f19 <> 1;
S: len f29 in dom f29 by FINSEQ_3:25,A89;
f29 = <*f29.len f29*> by A89,FINSEQ_5:14 .= <*f29/.len f29*>
by PARTFUN1:def 6,S;
hence g2 is unfolded by A81,A72,A90,Th29;
end;
suppose that
A91: len f29 <> 1 and
A92: len f19 <> 1;
consider k be Nat such that
A93: k+1 = len f29 by A79,NAT_1:6;
reconsider k as Element of NAT by ORDINAL1:def 12;
A94: k+(1+1) <= len f2 by A22,A93;
A95: LSeg(f29,k) = LSeg(f2,k) by A93,Th3;
len f29 > 1 by A22,A23,A91,XXREAL_0:1;
then 1 <= k by A93,NAT_1:13;
then LSeg(f29,k) /\ LSeg(f29/.len f29,f19/.1) = {f29/.len f29} by A22,A25
,A27,A93,A94,A95,TOPREAL1:def 6;
hence g2 is unfolded by A81,A72,A92,A93,Th31;
end;
end;
len g1 >= 2 by TOPREAL1:def 8;
then
A96: rng g1 c= L~g1 by Th18;
set Z = rng f29 /\ rng f19;
A97: 1 in dom f29 by A22,A23,FINSEQ_3:25;
A98: len f2 in dom f2 by FINSEQ_5:6;
then
A99: p2..f2 = len f2 by A4,FINSEQ_5:41;
now
assume
A100: p2 in rng f29;
then p2..f29 = p2..f2 by FINSEQ_5:40;
hence contradiction by A22,A99,A100,FINSEQ_4:21,XREAL_1:44;
end;
then
A101: not p2 in Z by XBOOLE_0:def 4;
then
A102: Z <> {p1,p2} by TARSKI:def 2;
dom f2 = Seg len f2 by FINSEQ_1:def 3;
then
A103: len f29 in dom f2 by A22,A14,A24,A18,FINSEQ_2:8;
now
p2 in LSeg(f2/.len f29,p2) by RLTOPSP1:68;
then
A104: p2 in LSeg(f2,len f29) by A4,A22,A23,A14,TOPREAL1:def 3;
assume p2 in L~f29;
then consider i such that
A105: 1 <= i and
A106: i+1 <= len(f29) and
A107: p2 in LSeg(f29,i) by Th13;
LSeg(f29,i) = LSeg(f2,i) by A106,Th3;
then
A108: p2 in LSeg(f2,i) /\ LSeg(f2,len f29) by A107,A104,XBOOLE_0:def 4;
then
A109: LSeg(f2,i) meets LSeg(f2,len f29);
A110: len f2 <> len f29 by A21,FINSEQ_1:59;
per cases;
suppose
A111: i+1 = len(f29);
then i + (1+1) = len f2 by A22;
then LSeg(f2,i) /\ LSeg(f2,len f29) = {f2/.len f29} by A105,A111,
TOPREAL1:def 6;
then p2 = f2/.len f29 by A108,TARSKI:def 1;
hence contradiction by A4,A98,A103,A110,PARTFUN2:10;
end;
suppose
i+1 <> len(f29);
then i+1 < len(f29) by A106,XXREAL_0:1;
hence contradiction by A109,TOPREAL1:def 7;
end;
end;
then
A112: not p2 in L~f29 /\ L~f19 by XBOOLE_0:def 4;
L~(f1:-q) c= L~f1 by A8,Lm15;
then
A113: L~f19 c= L~f1 by Th22;
L~f29 c= L~f2 by Lm1;
then L~f29 /\ L~f19 c= {p1,p2} by A5,A113,XBOOLE_1:27;
then
A114: L~f29 /\ L~f19 = {} or L~f29 /\ L~f19 = {p1} or L~f29 /\ L~f19 = { p2}
or L~f29 /\ L~f19 = {p1,p2} by ZFMISC_1:36;
f1:-q is special by A8,Th39;
then
A115: f19 is special by Th40;
A116: 1 in dom(f1:-q) by FINSEQ_5:6;
now
set l = p1..(f1:-q);
assume
A117: p1 in rng(f1:-q);
then
A118: (f1:-q).l = p1 by FINSEQ_4:19;
l <> 0 by A117,FINSEQ_4:21;
then consider j be Nat such that
A119: l = j+1 by NAT_1:6;
reconsider j as Element of NAT by ORDINAL1:def 12;
A120: l in dom(f1:-q) by A117,FINSEQ_4:20;
then
A121: j+q..f1 in dom f1 by A8,A119,FINSEQ_5:51;
(f1:-q)/.l = f1/.(j+q..f1) by A8,A120,A119,FINSEQ_5:52;
then j+q..f1 = 1 by A1,A31,A120,A118,A121,PARTFUN1:def 6,PARTFUN2:10;
then
A122: q..f1 <= 1 by NAT_1:11;
1 <= q..f1 by A8,FINSEQ_4:21;
hence contradiction by A10,A122,XXREAL_0:1;
end;
then not p1 in rng f19 by FINSEQ_5:57;
then not p1 in Z by XBOOLE_0:def 4;
then
A123: Z <> {p1} by TARSKI:def 1;
rng f29 c= rng f2 by FINSEQ_5:19;
then Z c= rng f2 /\ rng f1 by A15,XBOOLE_1:27;
then
A124: Z c= {p1,p2} by A5,A17;
reconsider f1q = f1:-q as one-to-one FinSequence of TOP-REAL 2 by A8,
FINSEQ_5:56;
A125: Rev f1q is one-to-one;
f1:-q is s.n.c. by A8,Th34;
then
A126: f19 is s.n.c. by Th35;
(f29/.len f29)`1 = (f19/.1)`1 or (f29/.len f29)`2 = (f19/.1)`2 by A23,A14,A25
,A26,TOPREAL1:def 5;
then
A127: g2 is special by A115,Lm13;
len f29 + len f19 >= 1+1 by A22,A19,A23,XREAL_1:7;
then
A128: len g2 >= 2 by FINSEQ_1:22;
Z <> {p2} by A101,TARSKI:def 1;
then Z = {} by A123,A102,A124,ZFMISC_1:36;
then rng f29 misses rng f19;
then
A129: g2 is one-to-one by A125,FINSEQ_3:91;
not p1 in L~f29 /\ L~f19 by A32,XBOOLE_0:def 4;
then L~f29 misses L~f19 by A114,A112,TARSKI:def 1,def 2;
then f29^f19 is s.n.c. by A126,A28,A47,Th36;
then reconsider g2 as S-Sequence_in_R2 by A129,A128,A82,A127,TOPREAL1:def 8;
A130: L~f2 \/ L~f19 = L~(f29^<*p2*>) \/ L~f19 by A4,A14,FINSEQ_5:21
.= L~f29 \/ LSeg(f29/.len f29,f19/.1) \/ L~f19 by A4,A97,A26,Th19,
RELAT_1:38
.= L~g2 by A20,A80,Th23,RELAT_1:38;
take g1,g2;
thus
A131: p1 = g1/.1 by A1,A8,FINSEQ_5:44;
A132: 1 in dom g2 by FINSEQ_5:6;
hence
A133: g2/.1 = g2.1 by PARTFUN1:def 6
.= f29.1 by A97,FINSEQ_1:def 7
.= f29/.1 by A97,PARTFUN1:def 6
.= p1 by A2,A97,FINSEQ_4:70;
thus
A134: q = g1/.(q..f1) by A8,FINSEQ_5:45
.= g1/.len g1 by A8,FINSEQ_5:42;
A135: len g2 in dom g2 by FINSEQ_5:6;
hence
A136: g2/.len g2 = g2.(len g2) by PARTFUN1:def 6
.= g2.(len f29 + len f19) by FINSEQ_1:22
.= f19.(len f19) by A20,FINSEQ_1:def 7
.= f19.(len (f1:-q)) by FINSEQ_5:def 3
.= (f1:-q).1 by FINSEQ_5:62
.= (f1:-q)/.1 by A116,PARTFUN1:def 6
.= q by FINSEQ_5:53;
len g2 >= 2 by TOPREAL1:def 8;
then
A137: rng g2 c= L~g2 by Th18;
A138: len g1 in dom g1 by FINSEQ_5:6;
thus {p1,q} = L~g1 /\ L~g2
proof
hereby
let x be object;
assume
A139: x in {p1,q};
per cases by A139,TARSKI:def 2;
suppose
A140: x = p1;
A141: p1 in rng g2 by A132,A133,PARTFUN2:2;
p1 in rng g1 by A131,A13,PARTFUN2:2;
hence x in L~g1 /\ L~g2 by A96,A137,A140,A141,XBOOLE_0:def 4;
end;
suppose
A142: x = q;
A143: q in rng g2 by A135,A136,PARTFUN2:2;
q in rng g1 by A134,A138,PARTFUN2:2;
hence x in L~g1 /\ L~g2 by A96,A137,A142,A143,XBOOLE_0:def 4;
end;
end;
A144: len f1 in dom f1 by FINSEQ_5:6;
A145: L~g1 /\ L~g2 = L~g1 /\ L~f2 \/ L~g1 /\ L~f19 by A130,XBOOLE_1:23;
A146: q..f1 in dom f1 by A8,FINSEQ_4:20;
A147: q = f1.(q..f1) by A8,FINSEQ_4:19
.= f1/.(q..f1) by A146,PARTFUN1:def 6;
A148: len g1 = q..f1 by A8,FINSEQ_5:42;
per cases;
suppose
A149: q <> p2;
now
A150: q..f1 <= len f1 by A8,FINSEQ_4:21;
then reconsider j = len f1 - 1 as Element of NAT by A9,INT_1:5
,XXREAL_0:2;
A151: j+1 = len f1;
A152: p2 in LSeg(f1/.j,f1/.(j+1)) by A3,RLTOPSP1:68;
1 < q..f1 by A10,A9,XXREAL_0:1;
then 1 < len f1 by A150,XXREAL_0:2;
then 1 <= j by A151,NAT_1:13;
then
A153: p2 in LSeg(f1,j) by A152,TOPREAL1:def 3;
assume p2 in L~g1;
then consider i such that
A154: 1 <= i and
A155: i+1 <= len g1 and
A156: p2 in LSeg(g1,i) by Th13;
A157: p2 in LSeg(f1,i) by A155,A156,Th9;
q..f1 < len f1 by A3,A147,A149,A150,XXREAL_0:1;
then
A158: q..f1 <= j by A151,NAT_1:13;
then
A159: i+1 <= j by A148,A155,XXREAL_0:2;
per cases;
suppose
A160: i+1 = j;
then i+(1+1) = j+1;
then LSeg(f1,i) /\ LSeg(f1,i+1) = {f1/.(i+1)} by A154,TOPREAL1:def 6;
then p2 in {f1/.(i+1)} by A157,A153,A160,XBOOLE_0:def 4;
then p2 = f1/.(i+1) by TARSKI:def 1;
hence contradiction by A148,A147,A149,A155,A158,A160,XXREAL_0:1;
end;
suppose
i+1 <> j;
then i+1 < j by A159,XXREAL_0:1;
then LSeg(f1,i) misses LSeg(f1,j) by TOPREAL1:def 7;
then LSeg(f1,i) /\ LSeg(f1,j) = {};
hence contradiction by A157,A153,XBOOLE_0:def 4;
end;
end;
then
A161: not p2 in L~g1 /\ L~f2 by XBOOLE_0:def 4;
L~g1 /\ L~f2 c= {p1,p2} by A5,A8,Lm14,XBOOLE_1:26;
then L~g1 /\ L~f2 = {} or L~g1 /\ L~f2 = {p1} or L~g1 /\ L~f2 = {p2} or
L~g1 /\ L~f2 = {p1,p2} by ZFMISC_1:36;
then
A162: L~g1 /\ L~f2 c= {p1} by A161,TARSKI:def 1,def 2;
L~g1 /\ L~f19 = L~g1 /\ L~(f1:-q) by Th22
.= {q} by A3,A8,A10,A147,A149,Th42;
then L~g1 /\ L~g2 c= {p1} \/ {q} by A145,A162,XBOOLE_1:9;
hence thesis by ENUMSET1:1;
end;
suppose
A163: q = p2;
p2..f1 = len f1 by A3,A144,FINSEQ_5:41;
then
A164: len(f1:-q) = len f1 - len f1 + 1 by A8,A163,FINSEQ_5:50
.= 0+1;
L~g1 /\ L~f19 = L~g1 /\ L~(f1:-q) by Th22
.= L~g1 /\ {} by A164,TOPREAL1:22
.= {};
hence thesis by A5,A8,A145,A163,Lm14,XBOOLE_1:26;
end;
end;
thus P = L~(f1-:q) \/ L~(f1:-q) \/ L~f2 by A6,A8,Th24
.= L~g1 \/ (L~f2 \/ L~(f1:-q)) by XBOOLE_1:4
.= L~g1 \/ L~g2 by A130,Th22;
end;
theorem Th51:
p1,p2 split P & q in P & q <> p1 implies p1,q split P
proof
assume p1 <> p2;
given f1,f2 being S-Sequence_in_R2 such that
A1: p1 = f1/.1 and
A2: p1 = f2/.1 and
A3: p2 = f1/.len f1 and
A4: p2 = f2/.len f2 and
A5: L~f1 /\ L~f2 = {p1,p2} and
A6: P = L~f1 \/ L~f2;
assume
A7: q in P;
assume
A8: q <> p1;
hence p1 <> q;
per cases by A6,A7,XBOOLE_0:def 3;
suppose
A9: q in L~f1;
now
per cases;
suppose
q in rng f1;
hence thesis by A1,A2,A3,A4,A5,A6,A8,Lm16;
end;
suppose
A10: not q in rng f1;
consider i such that
A11: 1 <= i and
A12: i+1 <= len f1 and
A13: q in LSeg(f1,i) by A9,Th13;
reconsider f19 = Ins(f1,i,q) as S-Sequence_in_R2 by A10,A13,Th48;
A14: L~f19 = L~f1 by A13,Th25;
1 <= i + 1 by NAT_1:11; then
1 <= len f1 by A12,XXREAL_0:2; then
Z: 1 in dom f1 & len f1 in dom f1 by FINSEQ_3:25; then
a3: p2 = f1.len f1 by A3,PARTFUN1:def 6;
S2: len f19 = len f1 + 1 by FINSEQ_5:69;
1 <= len f1 + 1 by NAT_1:11; then
1 <= len f19 by S2; then
S1: len f19 in dom f19 & 1 in dom f19 by FINSEQ_3:25;
A15: p2 = f19.len f19 by A12,a3,FINSEQ_5:74,S2
.= f19/.len f19 by S1,PARTFUN1:def 6;
A16: q in rng f19 by FINSEQ_5:71;
p1 = f1.1 by Z,A1,PARTFUN1:def 6; then
p1 = f19.1 by A11,FINSEQ_5:75 .= f19/.1 by PARTFUN1:def 6,S1;
hence thesis by A2,A4,A5,A6,A8,A16,A15,A14,Lm16;
end;
end;
hence thesis;
end;
suppose
A17: q in L~f2;
now
per cases;
suppose
q in rng f2;
hence thesis by A1,A2,A3,A4,A5,A6,A8,Lm16;
end;
suppose
A18: not q in rng f2;
consider i such that
A19: 1 <= i and
A20: i+1 <= len f2 and
A21: q in LSeg(f2,i) by A17,Th13;
reconsider f29 = Ins(f2,i,q) as S-Sequence_in_R2 by A18,A21,Th48;
A22: L~f29 = L~f2 by A21,Th25;
1 <= i + 1 by NAT_1:11; then
1 <= len f2 by A20,XXREAL_0:2; then
Z: 1 in dom f2 & len f2 in dom f2 by FINSEQ_3:25; then
Sa: p2 = f2.len f2 by PARTFUN1:def 6,A4;
Sc: len f29 = len f2 + 1 by FINSEQ_5:69;
then
1 <= len f29 by NAT_1:11; then
Sd: 1 in dom f29 & len f29 in dom f29 by FINSEQ_3:25;
A23: p2 = f29.len f29 by Sc,Sa,A20,FINSEQ_5:74
.= f29/.len f29 by PARTFUN1:def 6,Sd;
A24: q in rng f29 by FINSEQ_5:71;
p1 = f2.1 by PARTFUN1:def 6,A2,Z; then
p1 = f29.1 by A19,FINSEQ_5:75 .= f29/.1 by Sd,PARTFUN1:def 6;
hence thesis by A1,A3,A5,A6,A8,A24,A23,A22,Lm16;
end;
end;
hence thesis;
end;
end;
theorem Th52:
p1,p2 split P & q in P & q <> p2 implies q,p2 split P
proof
assume that
A1: p1,p2 split P and
A2: q in P and
A3: q <> p2;
p2,p1 split P by A1,Th50;
then p2,q split P by A2,A3,Th51;
hence thesis by Th50;
end;
theorem Th53:
p1,p2 split P & q1 in P & q2 in P & q1 <> q2 implies q1,q2 split P
proof
assume that
A1: p1,p2 split P and
A2: q1 in P and
A3: q2 in P and
A4: q1 <> q2;
A5: p2,p1 split P by A1,Th50;
per cases;
suppose
p1 = q1;
hence thesis by A1,A3,A4,Th51;
end;
suppose
p1 = q2;
hence thesis by A2,A4,A5,Th52;
end;
suppose
p1 <> q1;
then p1,q1 split P by A1,A2,Th51;
then q2,q1 split P by A3,A4,Th52;
hence thesis by Th50;
end;
suppose
p2 <> q1;
then q1,p2 split P by A1,A2,Th52;
hence thesis by A3,A4,Th51;
end;
end;
notation
let P be Subset of TOP-REAL 2;
synonym P is special_polygonal for P is being_special_polygon;
end;
definition
let P be Subset of TOP-REAL 2;
redefine attr P is special_polygonal means :: redefines special_polygonal (SPPOL_2, synonym) → being_special_polygon (TOPREAL4, definition)
ex p1,p2 st p1,p2 split P;
compatibility
proof
thus P is being_special_polygon implies ex p1,p2 st p1,p2 split P
proof
given p1,p2 being Point of TOP-REAL 2, P1,P2 being Subset of TOP-REAL 2
such that
A1: p1 <> p2 and
p1 in P and
p2 in P and
A2: P1 is_S-P_arc_joining p1,p2 and
A3: P2 is_S-P_arc_joining p1,p2 and
A4: P1 /\ P2 = {p1,p2} and
A5: P = P1 \/ P2;
take p1,p2;
thus p1 <> p2 by A1;
consider f1 such that
A6: f1 is being_S-Seq and
A7: P1 = L~f1 and
A8: p1=f1/.1 and
A9: p2=f1/.len f1 by A2;
consider f2 such that
A10: f2 is being_S-Seq and
A11: P2 = L~f2 and
A12: p1=f2/.1 and
A13: p2=f2/.len f2 by A3;
reconsider f1,f2 as S-Sequence_in_R2 by A6,A10;
take f1,f2;
thus thesis by A4,A5,A7,A8,A9,A11,A12,A13;
end;
given p1,p2 such that
A14: p1,p2 split P;
A15: p2 in {p1,p2} by TARSKI:def 2;
A16: p1 in {p1,p2} by TARSKI:def 2;
consider f1,f2 being S-Sequence_in_R2 such that
A17: p1 = f1/.1 and
A18: p1 = f2/.1 and
A19: p2 = f1/.len f1 and
A20: p2 = f2/.len f2 and
A21: L~f1 /\ L~f2 = {p1,p2} and
A22: P = L~f1 \/ L~f2 by A14;
take p1,p2, P1=L~f1, P2=L~f2;
thus p1 <> p2 by A14;
{p1,p2} c= P by A21,A22,XBOOLE_1:29;
hence p1 in P & p2 in P by A16,A15;
thus ex f st f is being_S-Seq & P1 = L~f & p1=f/.1 & p2=f/.len f by A17,A19
;
thus ex f st f is being_S-Seq & P2 = L~f & p1=f/.1 & p2=f/.len f by A18,A20
;
thus thesis by A21,A22;
end;
end;
definition
let r1,r2,r19,r29 be Real;
func [.r1,r2,r19,r29.] -> Subset of TOP-REAL 2 equals
( LSeg(|[r1,r19]|,|[r1
,r29]|) \/ LSeg(|[r1,r29]|,|[r2,r29]|) ) \/ ( LSeg(|[r2,r29]|,|[r2,r19]|) \/
LSeg(|[r2,r19]|,|[r1,r19]|) );
coherence;
end;
registration
let n be Element of NAT;
let p1, p2 be Point of TOP-REAL n;
cluster LSeg(p1,p2) -> compact;
coherence;
end;
registration
let r1,r2,r19,r29;
cluster [.r1,r2,r19,r29.] -> non empty compact;
coherence
proof
thus [.r1,r2,r19,r29.] is non empty;
A1: LSeg(|[r2,r29]|,|[r2,r19]|) \/ LSeg(|[r2,r19]|,|[r1,r19]|) is compact
by COMPTS_1:10;
LSeg(|[r1,r19]|,|[r1,r29]|) \/ LSeg(|[r1,r29]|,|[r2,r29]|) is compact
by COMPTS_1:10;
hence thesis by A1,COMPTS_1:10;
end;
end;
theorem
r1<=r2 & r19<=r29 implies [.r1,r2,r19,r29.] = { p: p`1 = r1 & p`2 <=
r29 & p`2 >= r19 or p`1 <= r2 & p`1 >= r1 & p`2 = r29 or p`1 <= r2 & p`1 >= r1
& p`2 = r19 or p`1 = r2 & p`2 <= r29 & p`2 >= r19}
proof
assume that
A1: r1<=r2 and
A2: r19<=r29;
set p1 = |[r1,r19]|, p2 = |[r1,r29]| , p3 = |[r2,r29]|, p4 = |[r2,r19]|;
set P4 = { p: p`2 = r19& r1 <= p`1 & p`1 <= r2 };
set P3 = { p: p`1 = r2 & r19<= p`2 & p`2 <= r29};
set P2 = { p: p`2 = r29& r1 <= p`1 & p`1 <= r2 };
set P1 = { p: p`1 = r1 & r19<= p`2 & p`2 <= r29};
set P = { p: p`1 = r1 & p`2 <= r29 & p`2 >= r19 or p`1 <= r2 & p`1 >= r1 & p
`2 = r29 or p`1 <= r2 & p`1 >= r1 & p`2 = r19 or p`1 = r2 & p`2 <= r29 & p`2 >=
r19};
A3: P = P1 \/ P2 \/ (P3 \/ P4)
proof
hereby
let x be object;
assume x in P;
then
ex p st x = p &( p`1 = r1 & p`2 <= r29 & p`2 >= r19 or p `1 <= r2 &
p`1 >= r1 & p`2 = r29 or p`1 <= r2 & p`1 >= r1 & p`2 = r19 or p`1 = r2 & p`2 <=
r29 & p`2 >= r19);
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 x in P1 \/ P2 \/ (P3 \/ P4) by XBOOLE_0:def 3;
end;
let x be object;
assume x in P1 \/ P2 \/ (P3 \/ P4);
then
A4: x in P1 \/ P2 or x in P3 \/ P4 by XBOOLE_0:def 3;
per cases by A4,XBOOLE_0:def 3;
suppose
x in P1;
then ex p st x = p & p`1 = r1 & r19<= p`2 & p`2 <= r29;
hence thesis;
end;
suppose
x in P2;
then ex p st x = p & p`2 = r29& r1 <= p`1 & p`1 <= r2;
hence thesis;
end;
suppose
x in P3;
then ex p st x = p & p`1 = r2 & r19<= p`2 & p`2 <= r29;
hence thesis;
end;
suppose
x in P4;
then ex p st x = p & p`2 = r19& r1 <= p`1 & p`1 <= r2;
hence thesis;
end;
end;
thus [.r1,r2,r19,r29.] = P1 \/ LSeg(p2,p3) \/ (LSeg(p3,p4) \/ LSeg(p4,p1))
by A2,TOPREAL3:9
.= P1 \/ P2 \/ (LSeg(p3,p4) \/ LSeg(p4,p1)) by A1,TOPREAL3:10
.= P1 \/ P2 \/ (P3 \/ LSeg(p4,p1)) by A2,TOPREAL3:9
.= P by A1,A3,TOPREAL3:10;
end;
theorem Th55:
r1<>r2 & r19<>r29 implies [.r1,r2,r19,r29.] is special_polygonal
proof
assume that
A1: r1<>r2 and
A2: r19<>r29;
set p1 = |[r1,r19]|, p2 = |[r1,r29]| , p3 = |[r2,r29]|, p4 = |[r2,r19]|;
A3: p3`1 = r2 by EUCLID:52;
take p1,p3;
thus p1 <> p3 by A1,FINSEQ_1:77;
A4: p4`1 = r2 by EUCLID:52;
A5: p3`2 = r29 by EUCLID:52;
A6: p4`2 = r19 by EUCLID:52;
set f1 = <* p1,p2,p3 *>, f2 = <* p1,p4,p3 *>;
A7: p1`1 = r1 by EUCLID:52;
A8: len f2 = 3 by FINSEQ_1:45;
A9: len f1 = 3 by FINSEQ_1:45;
A10: p1`2 = r19 by EUCLID:52;
then reconsider f1,f2 as S-Sequence_in_R2 by A1,A2,A7,A3,A5,TOPREAL3:34,35;
take f1,f2;
thus p1 = f1/.1 & p1 = f2/.1 & p3 = f1/.len f1 & p3 = f2/.len f2 by A9,A8,
FINSEQ_4:18;
A11: L~f2 = LSeg(p3,p4) \/ LSeg(p4,p1) by TOPREAL3:16;
L~f1 = LSeg(p1,p2) \/ LSeg(p2,p3) by TOPREAL3:16;
hence
L~f1 /\ L~f2 = ((LSeg(p1,p2) \/ LSeg(p2,p3)) /\ LSeg(p3,p4)) \/ ((LSeg(
p1,p2) \/ LSeg(p2,p3)) /\ LSeg(p4,p1)) by A11,XBOOLE_1:23
.= ((LSeg(p2,p1) \/ LSeg(p3,p2)) /\ LSeg(p4,p3)) \/ {p1} by A2,A7,A10,A5,A6
,TOPREAL3:27
.= {p3} \/ {p1} by A1,A7,A3,A5,A4,TOPREAL3:28
.= {p1,p3} by ENUMSET1:1;
thus thesis by A11,TOPREAL3:16;
end;
theorem Th56:
R^2-unit_square = [.0,1,0,1.];
registration
cluster special_polygonal for Subset of TOP-REAL 2;
existence
proof
take [.0,1,0,1.];
thus thesis by Th55;
end;
end;
registration
cluster R^2-unit_square -> special_polygonal;
coherence by Th55,Th56;
end;
registration
cluster special_polygonal for Subset of TOP-REAL 2;
existence by Th56;
cluster special_polygonal -> non empty for Subset of TOP-REAL 2;
coherence;
cluster special_polygonal -> non trivial for Subset of TOP-REAL 2;
coherence
by ZFMISC_1:def 10;
end;
definition
mode Special_polygon_in_R2 is special_polygonal Subset of TOP-REAL 2;
end;
theorem Th57:
P is being_S-P_arc implies P is compact
proof
A1: I[01] is compact by HEINE:4,TOPMETR:20;
assume P is being_S-P_arc;
then reconsider P as being_S-P_arc Subset of TOP-REAL 2;
consider f being Function of I[01], (TOP-REAL 2)|P such that
A2: f is being_homeomorphism by TOPREAL1:29;
A3: rng f = [#]((TOP-REAL 2)|P) by A2,TOPS_2:def 5;
f is continuous by A2,TOPS_2:def 5;
then (TOP-REAL 2)|P is compact by A1,A3,COMPTS_1:14;
hence thesis by COMPTS_1:3;
end;
registration
cluster -> compact for Special_polygon_in_R2;
coherence
proof
let G be Special_polygon_in_R2;
consider p,q being Point of TOP-REAL 2, P1,P2 being Subset of TOP-REAL 2
such that
p<>q and
p in G and
q in G and
A1: P1 is_S-P_arc_joining p,q and
A2: P2 is_S-P_arc_joining p,q and
P1 /\ P2 = {p,q} and
A3: G = P1 \/ P2 by TOPREAL4:def 2;
reconsider P1,P2 as Subset of TOP-REAL 2;
A4: P2 is compact by A2,Th57,TOPREAL4:1;
P1 is compact by A1,Th57,TOPREAL4:1;
hence thesis by A3,A4,COMPTS_1:10;
end;
end;
theorem Th58:
P is special_polygonal implies for p1,p2 st p1 <> p2 & p1 in P &
p2 in P holds p1,p2 split P
by Th53;
theorem
P is special_polygonal implies for p1,p2 st p1 <> p2 & p1 in P & p2 in
P ex P1,P2 being Subset of TOP-REAL 2 st P1 is_S-P_arc_joining p1,p2 & P2
is_S-P_arc_joining p1,p2 & P1 /\ P2 = {p1,p2} & P = P1 \/ P2
proof
assume
A1: P is special_polygonal;
let p1,p2;
assume that
A2: p1 <> p2 and
A3: p1 in P and
A4: p2 in P;
p1,p2 split P by A1,A2,A3,A4,Th58;
then consider f1,f2 being S-Sequence_in_R2 such that
A5: p1 = f1/.1 and
A6: p1 = f2/.1 and
A7: p2 = f1/.len f1 and
A8: p2 = f2/.len f2 and
A9: L~f1 /\ L~f2 = {p1,p2} and
A10: P = L~f1 \/ L~f2;
take P1 = L~f1, P2 = L~f2;
thus P1 is_S-P_arc_joining p1,p2 by A5,A7;
thus P2 is_S-P_arc_joining p1,p2 by A6,A8;
thus thesis by A9,A10;
end;