:: Subsequences of Almost, Weakly and Poorly One-to-one Finite Sequences
:: by Robert Milewski
::
:: Received February 1, 2005
:: Copyright (c) 2005-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies NUMBERS, SUBSET_1, FINSEQ_1, EUCLID, PRE_TOPC, TOPREAL1, JORDAN3,
XXREAL_0, XBOOLE_0, CARD_1, ARYTM_3, GROUP_2, PARTFUN1, FINSEQ_5,
FUNCT_1, RELAT_1, FINSEQ_6, ARYTM_1, FINSEQ_4, RFINSEQ, ORDINAL4,
RCOMP_1, SPPOL_1, JORDAN9, RLTOPSP1, NAT_1, TARSKI, GRAPH_2, MCART_1,
REAL_1, SUPINF_2, JORDAN2C, SPPOL_2, JORDAN18, GOBOARD1, GOBOARD2,
GOBOARD5, MATRIX_1, JORDAN23;
notations TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XXREAL_0, XCMPLX_0,
XREAL_0, REAL_1, NAT_1, FUNCT_1, PARTFUN1, FINSEQ_1, FINSEQ_4, FINSEQ_5,
RFINSEQ, MATRIX_0, FINSEQ_6, GRAPH_2, STRUCT_0, PRE_TOPC, NAT_D,
COMPTS_1, RLVECT_1, RLTOPSP1, EUCLID, GOBOARD1, TOPREAL1, GOBOARD2,
GOBOARD5, SPPOL_1, SPPOL_2, JORDAN3, JORDAN5C, JORDAN9, JORDAN2C,
JORDAN18;
constructors REAL_1, FINSEQ_4, REALSET1, RFINSEQ, NAT_D, FINSEQ_5, GOBOARD2,
GRAPH_2, JORDAN3, JORDAN5C, SPRECT_1, JORDAN2C, JORDAN9, JORDAN18,
GOBOARD1, RELSET_1, FUNCT_7;
registrations RELAT_1, FUNCT_1, XXREAL_0, XREAL_0, FINSEQ_1, FINSEQ_6,
STRUCT_0, GOBOARD2, SPPOL_2, SPRECT_1, REVROT_1, TOPREAL6, JORDAN1J,
ORDINAL1, CARD_1, EUCLID, SPRECT_5, ZFMISC_1, SUBSET_1;
requirements ARITHM, NUMERALS, BOOLE, SUBSET, REAL;
definitions TARSKI, XBOOLE_0, FUNCT_1;
equalities XBOOLE_0, RLTOPSP1;
expansions TARSKI, XBOOLE_0, FUNCT_1;
theorems NAT_1, FINSEQ_1, FINSEQ_4, EUCLID, FINSEQ_3, SPPOL_2, TARSKI,
JORDAN3, FINSEQ_5, FINSEQ_6, GOBOARD7, TOPREAL1, JORDAN5B, SPRECT_2,
SPPOL_1, FINSEQ_2, JORDAN4, GOBOARD2, SPRECT_3, TOPREAL3, JORDAN8,
PARTFUN2, XBOOLE_0, XBOOLE_1, ZFMISC_1, JORDAN1E, REVROT_1, JORDAN1B,
JORDAN1J, GOBOARD3, TOPREAL8, GRAPH_2, JORDAN18, JORDAN5C, MSUALG_8,
XREAL_1, XXREAL_0, ORDINAL1, PARTFUN1, XREAL_0, NAT_D, RLTOPSP1, RFINSEQ,
SEQ_4, RLVECT_1;
begin
reserve n for Nat;
theorem Th1:
for f be FinSequence of TOP-REAL 2 for p be Point of TOP-REAL 2
st p in L~f holds len L_Cut(f,p) >= 1
proof
let f be FinSequence of TOP-REAL 2;
let p be Point of TOP-REAL 2;
assume p in L~f;
then L_Cut(f,p) <> {} by JORDAN1E:3;
then
A1: len L_Cut(f,p) > 0 by NAT_1:3;
1=0+1;
hence thesis by A1,NAT_1:13;
end;
theorem
for f be non empty FinSequence of TOP-REAL 2 for p be Point of
TOP-REAL 2 holds len R_Cut(f,p) >= 1
proof
let f be non empty FinSequence of TOP-REAL 2;
let p be Point of TOP-REAL 2;
R_Cut(f,p) <> {} by JORDAN1J:44;
then
A1: len R_Cut(f,p) > 0 by NAT_1:3;
1 = 0+1;
hence thesis by A1,NAT_1:13;
end;
theorem Th3:
for f be FinSequence of TOP-REAL 2 for p,q be Point of TOP-REAL 2
holds B_Cut (f,p,q) <> {}
proof
let f be FinSequence of TOP-REAL 2;
let p,q be Point of TOP-REAL 2;
A1: R_Cut(L_Cut(f,q),p) <> {} by JORDAN1J:44;
per cases;
suppose
p in L~f & q in L~f & Index(p,f)<Index(q,f) or Index(p,f)=Index(q,
f) & LE p,q,f/.(Index(p,f)),f/.(Index(p,f)+1);
then B_Cut(f,p,q) = R_Cut(L_Cut(f,p),q) by JORDAN3:def 7;
hence thesis by JORDAN1J:44;
end;
suppose
not (p in L~f & q in L~f & Index(p,f)<Index(q,f) or Index(p,f)=
Index(q,f) & LE p,q,f/.(Index(p,f)),f/.(Index(p,f)+1));
then B_Cut(f,p,q) = Rev R_Cut(L_Cut(f,q),p) by JORDAN3:def 7;
hence thesis by A1;
end;
end;
registration
let x be set;
cluster <*x*> -> one-to-one;
coherence by FINSEQ_3:93;
end;
definition
let f be FinSequence;
attr f is almost-one-to-one means
for i,j be Nat st i in
dom f & j in dom f & (i <> 1 or j <> len f) & (i <> len f or j <> 1) & f.i = f.
j holds i = j;
end;
definition
let f be FinSequence;
attr f is weakly-one-to-one means
for i be Nat st 1 <= i & i < len f holds f.i <> f.(i+1);
end;
definition
let f be FinSequence;
attr f is poorly-one-to-one means
:Def3:
for i be Nat st 1 <= i &
i < len f holds f.i <> f.(i+1) if len f <> 2 otherwise not contradiction;
consistency;
end;
theorem
for D be set for f be FinSequence of D holds f is almost-one-to-one
iff for i,j be Nat st i in dom f & j in dom f & (i <> 1 or j <> len
f) & (i <> len f or j <> 1) & f/.i = f/.j holds i = j
proof
let D be set;
let f be FinSequence of D;
thus f is almost-one-to-one implies for i,j be Nat st i in dom f
& j in dom f & (i <> 1 or j <> len f) & (i <> len f or j <> 1) & f/.i = f/.j
holds i = j
proof
assume
A1: f is almost-one-to-one;
let i,j be Nat such that
A2: i in dom f and
A3: j in dom f and
A4: i <> 1 or j <> len f and
A5: i <> len f or j <> 1 and
A6: f/.i = f/.j;
f.i = f/.j by A2,A6,PARTFUN1:def 6
.= f.j by A3,PARTFUN1:def 6;
hence thesis by A1,A2,A3,A4,A5;
end;
assume
A7: for i,j be Nat st i in dom f & j in dom f & (i <> 1 or j
<> len f) & (i <> len f or j <> 1) & f/.i = f/.j holds i = j;
now
let i,j be Nat such that
A8: i in dom f and
A9: j in dom f and
A10: i <> 1 or j <> len f and
A11: i <> len f or j <> 1 and
A12: f.i = f.j;
f/.i = f.j by A8,A12,PARTFUN1:def 6
.= f/.j by A9,PARTFUN1:def 6;
hence i = j by A7,A8,A9,A10,A11;
end;
hence thesis;
end;
theorem Th5:
for D be set for f be FinSequence of D holds f is
weakly-one-to-one iff for i be Nat st 1 <= i & i < len f holds f/.i
<> f/.(i+1)
proof
let D be set;
let f be FinSequence of D;
thus f is weakly-one-to-one implies for i be Nat st 1 <= i & i <
len f holds f/.i <> f/.(i+1)
proof
assume
A1: f is weakly-one-to-one;
let i be Nat such that
A2: 1 <= i and
A3: i < len f;
A4: i+1 <= len f by A3,NAT_1:13;
1 < i+1 by A2,NAT_1:13;
then
A5: f.(i+1) = f/.(i+1) by A4,FINSEQ_4:15;
f.i = f/.i by A2,A3,FINSEQ_4:15;
hence thesis by A1,A2,A3,A5;
end;
assume
A6: for i be Nat st 1 <= i & i < len f holds f/.i <> f/.(i+1 );
now
let i be Nat such that
A7: 1 <= i and
A8: i < len f;
A9: i+1 <= len f by A8,NAT_1:13;
1 < i+1 by A7,NAT_1:13;
then
A10: f.(i+1) = f/.(i+1) by A9,FINSEQ_4:15;
f.i = f/.i by A7,A8,FINSEQ_4:15;
hence f.i <> f.(i+1) by A6,A7,A8,A10;
end;
hence thesis;
end;
theorem
for D be set for f be FinSequence of D holds f is poorly-one-to-one
iff (len f <> 2 implies for i be Nat st 1 <= i & i < len f holds f/.
i <> f/.(i+1))
proof
let D be set;
let f be FinSequence of D;
thus f is poorly-one-to-one & len f <> 2 implies for i be Nat st
1 <= i & i < len f holds f/.i <> f/.(i+1)
proof
assume that
A1: f is poorly-one-to-one and
A2: len f <> 2;
let i be Nat such that
A3: 1 <= i and
A4: i < len f;
A5: i+1 <= len f by A4,NAT_1:13;
1 < i+1 by A3,NAT_1:13;
then
A6: f.(i+1) = f/.(i+1) by A5,FINSEQ_4:15;
f.i = f/.i by A3,A4,FINSEQ_4:15;
hence thesis by A1,A2,A3,A4,A6,Def3;
end;
assume
A7: len f <> 2 implies for i be Nat st 1 <= i & i < len f
holds f/.i <> f/.(i+1);
per cases;
suppose
A8: len f <> 2;
now
let i be Nat such that
A9: 1 <= i and
A10: i < len f;
A11: i+1 <= len f by A10,NAT_1:13;
1 < i+1 by A9,NAT_1:13;
then
A12: f.(i+1) = f/.(i+1) by A11,FINSEQ_4:15;
f.i = f/.i by A9,A10,FINSEQ_4:15;
hence f.i <> f.(i+1) by A7,A8,A9,A10,A12;
end;
hence thesis by A8,Def3;
end;
suppose
len f = 2;
hence thesis by Def3;
end;
end;
registration
cluster one-to-one -> almost-one-to-one for FinSequence;
coherence;
end;
registration
cluster almost-one-to-one -> poorly-one-to-one for FinSequence;
coherence
proof
let f be FinSequence;
assume
A1: f is almost-one-to-one;
per cases;
case
A2: len f <> 2;
now
per cases;
suppose
A3: len f <> 0;
let i be Nat;
A4: not (i = len f & i+1 = 1) by A3;
A5: i+1 >= 1 by NAT_1:11;
assume that
A6: 1 <= i and
A7: i < len f;
i+1 <= len f by A7,NAT_1:13;
then
A8: i+1 in dom f by A5,FINSEQ_3:25;
A9: not (i = 1 & i+1 = len f) by A2;
A10: i <> i+1;
i in dom f by A6,A7,FINSEQ_3:25;
hence f.i <> f.(i+1) by A1,A8,A10,A9,A4;
end;
suppose
A11: len f = 0;
let i be Nat;
assume that
A12: 1 <= i and
A13: i < len f;
thus f.i <> f.(i+1) by A11,A12,A13;
end;
end;
hence thesis;
end;
case len f = 2;
end;
end;
end;
theorem Th7:
for f be FinSequence st len f <> 2 holds f is weakly-one-to-one
iff f is poorly-one-to-one
by Def3;
registration
cluster empty -> weakly-one-to-one for FinSequence;
coherence;
end;
registration
let x be set;
cluster <*x*> -> weakly-one-to-one;
coherence
by FINSEQ_1:39;
end;
registration
let x,y be set;
cluster <*x,y*> -> poorly-one-to-one;
coherence
proof
len <*x,y*> = 2 by FINSEQ_1:44;
hence thesis by Def3;
end;
end;
registration
cluster weakly-one-to-one non empty for FinSequence;
existence
proof
set x = the set;
len <*x*> <> 2 by FINSEQ_1:39;
hence thesis;
end;
end;
registration
let D be non empty set;
cluster weakly-one-to-one circular non empty for FinSequence of D;
existence
proof
set x = the Element of D;
<*x*>/.1 = <*x*>/.len <*x*> by FINSEQ_1:39;
then <*x*> is circular by FINSEQ_6:def 1;
hence thesis;
end;
end;
theorem Th8:
for f be FinSequence st f is almost-one-to-one holds Rev f is
almost-one-to-one
proof
let f be FinSequence;
assume
A1: f is almost-one-to-one;
let i,j be Nat;
assume that
A2: i in dom Rev f and
A3: j in dom Rev f and
A4: i <> 1 or j <> len Rev f and
A5: i <> len Rev f or j <> 1 and
A6: Rev f.i = Rev f.j;
A7: not(len f - i + 1 = len f & len f - j + 1 = 1) by A4,FINSEQ_5:def 3;
A8: dom f = dom Rev f by FINSEQ_5:57;
then i in Seg len f by A2,FINSEQ_1:def 3;
then len f - i + 1 in Seg len f by FINSEQ_5:2;
then
A9: len f - i + 1 in dom f by FINSEQ_1:def 3;
A10: Rev f.j = f.(len f - j + 1) by A3,FINSEQ_5:def 3;
A11: Rev f.i = f.(len f - i + 1) by A2,FINSEQ_5:def 3;
j in Seg len f by A3,A8,FINSEQ_1:def 3;
then len f - j + 1 in Seg len f by FINSEQ_5:2;
then
A12: len f - j + 1 in dom f by FINSEQ_1:def 3;
not(len f - i + 1 = 1 & len f - j + 1 = len f) by A5,FINSEQ_5:def 3;
then len f - i + 1 = len f - j + 1 by A1,A6,A9,A12,A7,A11,A10;
hence thesis;
end;
theorem Th9:
for f be FinSequence st f is weakly-one-to-one holds Rev f is
weakly-one-to-one
proof
let f be FinSequence;
assume
A1: f is weakly-one-to-one;
A2: len f = len Rev f by FINSEQ_5:def 3;
let i be Nat;
assume that
A3: 1 <= i and
A4: i < len Rev f;
A5: i+1 <= len Rev f by A4,NAT_1:13;
i+1 >= 1 by NAT_1:11;
then
A6: i+1 in Seg len Rev f by A5,FINSEQ_1:1;
then i+1 in dom Rev f by FINSEQ_1:def 3;
then
A7: Rev f.(i+1) = f.(len f - (i+1) + 1) by FINSEQ_5:def 3;
A8: i in Seg len Rev f by A3,A4,FINSEQ_1:1;
then i in dom Rev f by FINSEQ_1:def 3;
then
A9: Rev f.i = f.(len f - i + 1) by FINSEQ_5:def 3;
len f - (i+1) + 1 = len f - i;
then reconsider j = len f - i as Nat by A2,A5,FINSEQ_5:1;
len f - i + 1 in Seg len f by A2,A8,FINSEQ_5:2;
then j+1 <= len f by FINSEQ_1:1;
then
A10: j < len f by NAT_1:13;
len f - (i+1) + 1 in Seg len f by A2,A6,FINSEQ_5:2;
then j >= 1 by FINSEQ_1:1;
hence thesis by A1,A9,A7,A10;
end;
theorem Th10:
for f be FinSequence st f is poorly-one-to-one holds Rev f is
poorly-one-to-one
proof
let f be FinSequence;
assume
A1: f is poorly-one-to-one;
A2: len f = len Rev f by FINSEQ_5:def 3;
per cases;
suppose
A3: len f <> 2;
then f is weakly-one-to-one by A1,Th7;
then Rev f is weakly-one-to-one by Th9;
hence thesis by A2,A3,Th7;
end;
suppose
len f = 2;
hence thesis by A2,Def3;
end;
end;
registration
cluster one-to-one non empty for FinSequence;
existence
proof
set x = the set;
<*x*> is non empty one-to-one;
hence thesis;
end;
end;
registration
let f be almost-one-to-one FinSequence;
cluster Rev f -> almost-one-to-one;
coherence by Th8;
end;
registration
let f be weakly-one-to-one FinSequence;
cluster Rev f -> weakly-one-to-one;
coherence by Th9;
end;
registration
let f be poorly-one-to-one FinSequence;
cluster Rev f -> poorly-one-to-one;
coherence by Th10;
end;
theorem Th11:
for D be non empty set for f be FinSequence of D st f is
almost-one-to-one for p be Element of D holds Rotate(f,p) is almost-one-to-one
proof
let D be non empty set;
let f be FinSequence of D;
assume
A1: f is almost-one-to-one;
let p be Element of D;
per cases;
suppose
A2: p in rng f;
then 0+1 <= p..f by FINSEQ_4:21;
then
A3: p..f - 1 >= 0 by XREAL_1:19;
A4: len (f:-p) = len f - p..f + 1 by A2,FINSEQ_5:50;
let i,j be Nat;
assume that
A5: i in dom Rotate(f,p) and
A6: j in dom Rotate(f,p) and
A7: i <> 1 or j <> len Rotate(f,p) and
A8: i <> len Rotate(f,p) or j <> 1 and
A9: Rotate(f,p).i = Rotate(f,p).j;
A10: 0+1 <= i by A5,FINSEQ_3:25;
A11: dom Rotate(f,p) = dom f by FINSEQ_6:180;
then
A12: i <= len f by A5,FINSEQ_3:25;
then
A13: i - len f <= len f-len f by XREAL_1:9;
A14: j <= len f by A6,A11,FINSEQ_3:25;
then
A15: j - len f <= len f-len f by XREAL_1:9;
A16: len Rotate(f,p) = len f by FINSEQ_6:179;
A17: 0+1 <= j by A6,FINSEQ_3:25;
then
A18: j - 1 >= 0 by XREAL_1:19;
A19: now
assume that
A20: i -' 1 + p..f = len f and
A21: j -' 1 + p..f = 1;
j -' 1 + (p..f - 1) = 0 by A21;
then
A22: j -' 1 = 0 by A3;
then j - 1 = 0 by A18,XREAL_0:def 2;
hence contradiction by A8,A16,A10,A20,A21,A22,XREAL_1:235;
end;
A23: p..f <= len f by A2,FINSEQ_4:21;
A24: i - 1 >= 0 by A10,XREAL_1:19;
A25: now
assume that
A26: i -' 1 + p..f = 1 and
A27: j -' 1 + p..f = len f;
i -' 1 + (p..f - 1) = 0 by A26;
then
A28: i -' 1 = 0 by A3;
then i - 1 = 0 by A24,XREAL_0:def 2;
hence contradiction by A7,A16,A17,A26,A27,A28,XREAL_1:235;
end;
now
per cases;
suppose
A29: i <= len(f:-p);
then i in dom(f:-p) by A10,FINSEQ_3:25;
then i -' 1 + 1 in dom(f:-p) by A10,XREAL_1:235;
then
A30: i -' 1 + p..f in dom f by A2,FINSEQ_5:51;
Rotate(f,p)/.i = f/.(i -' 1 + p..f) by A2,A10,A29,FINSEQ_6:174;
then
A31: Rotate(f,p).i = f/.(i -' 1 + p..f) by A5,PARTFUN1:def 6;
now
per cases;
suppose
A32: j <= len(f:-p);
then j in dom(f:-p) by A17,FINSEQ_3:25;
then j -' 1 + 1 in dom(f:-p) by A17,XREAL_1:235;
then
A33: j -' 1 + p..f in dom f by A2,FINSEQ_5:51;
Rotate(f,p)/.j = f/.(j -' 1 + p..f) by A2,A17,A32,FINSEQ_6:174;
then
A34: f/.(i -' 1 + p..f) = f/.(j -' 1 + p..f) by A6,A9,A31,PARTFUN1:def 6
;
f.(i -' 1 + p..f) = f/.(i -' 1 + p..f) by A30,PARTFUN1:def 6
.= f.(j -' 1 + p..f) by A34,A33,PARTFUN1:def 6;
then i -' 1 + p..f = j -' 1 + p..f by A1,A25,A19,A30,A33;
hence thesis by A10,A17,XREAL_1:234;
end;
suppose
A35: j > len(f:-p);
then Rotate(f,p)/.j = f/.(j + p..f -' len f) by A2,A14,
FINSEQ_6:177;
then
A36: f
/.(i -' 1 + p..f) = f/.(j + p..f -' len f) by A6,A9,A31,PARTFUN1:def 6;
A37: j - (len f - p..f) > 1 by A4,A35,XREAL_1:20;
then
A38: j + p..f - len f > 1;
then
A39: j + p..f -' len f >= 1 by XREAL_0:def 2;
j + p..f <= len f + len f by A23,A14,XREAL_1:7;
then j + p..f - len f <= len f by XREAL_1:20;
then j + p..f -' len f <= len f by A37,XREAL_0:def 2;
then
A40: j + p..f -' len f in dom f by A39,FINSEQ_3:25;
A41: now
assume that
A42: i -' 1 + p..f = 1 and
A43: j + p..f -' len f = len f;
j + p..f - len f = len f by A37,A43,XREAL_0:def 2;
then j + p..f = len f + len f;
then
A44: j >= len f by A23,XREAL_1:8;
i -' 1 + (p..f - 1) = 0 by A42;
then i -' 1 = 0 by A3;
then i - 1 = 0 by A24,XREAL_0:def 2;
hence contradiction by A7,A16,A14,A44,XXREAL_0:1;
end;
A45: i -' 1 + p..f <> len f or j + p..f -' len f <> 1 by A38,
XREAL_0:def 2;
f.(i -' 1 + p..f) = f/.(i -' 1 + p..f) by A30,PARTFUN1:def 6
.= f.(j + p..f -' len f) by A36,A40,PARTFUN1:def 6;
then i -' 1 + p..f = j + p..f -' len f by A1,A30,A41,A45,A40;
then
A46: i -' 1 + p..f = j + p..f - len f by A37,XREAL_0:def 2;
then
A47: j - len f = 0 by A15;
i - 1 = 0 by A24,A15,A46,XREAL_0:def 2;
hence thesis by A7,A47,FINSEQ_6:179;
end;
end;
hence thesis;
end;
suppose
A48: i > len(f:-p);
then
A49: i - (len f - p..f) > 1 by A4,XREAL_1:20;
i + p..f <= len f + len f by A23,A12,XREAL_1:7;
then i + p..f - len f <= len f by XREAL_1:20;
then
A50: i + p..f -' len f <= len f by A49,XREAL_0:def 2;
A51: i + p..f - len f > 1 by A49;
then i + p..f -' len f >= 1 by XREAL_0:def 2;
then
A52: i + p..f -' len f in dom f by A50,FINSEQ_3:25;
A53: Rotate(f,p)/.i = f/.(i+p..f -' len f) by A2,A12,A48,FINSEQ_6:177;
now
per cases;
suppose
A54: j <= len(f:-p);
A55: now
assume that
A56: j -' 1 + p..f = 1 and
A57: i + p..f -' len f = len f;
i + p..f - len f = len f by A49,A57,XREAL_0:def 2;
then i + p..f = len f + len f;
then
A58: i >= len f by A23,XREAL_1:8;
j -' 1 + (p..f - 1) = 0 by A56;
then j -' 1 = 0 by A3;
then j - 1 = 0 by A18,XREAL_0:def 2;
hence contradiction by A8,A16,A12,A58,XXREAL_0:1;
end;
Rotate(f,p)/.j = f/.(j -' 1 + p..f) by A2,A17,A54,FINSEQ_6:174;
then Rotate(f,p).j = f/.(j -' 1 + p..f) by A6,PARTFUN1:def 6;
then
A59: f
/.(j -' 1 + p..f) = f/.(i + p..f -' len f) by A5,A9,A53,PARTFUN1:def 6;
A60: j -' 1 + p..f <> len f or i + p..f -' len f <> 1 by A51,
XREAL_0:def 2;
j in dom(f:-p) by A17,A54,FINSEQ_3:25;
then j -' 1 + 1 in dom(f:-p) by A17,XREAL_1:235;
then
A61: j -' 1 + p..f in dom f by A2,FINSEQ_5:51;
then f.(j -' 1 + p..f) = f/.(j -' 1 + p..f) by PARTFUN1:def 6
.= f.(i + p..f -' len f) by A52,A59,PARTFUN1:def 6;
then j -' 1 + p..f = i + p..f -' len f by A1,A52,A61,A55,A60;
then
A62: j -' 1 + p..f = i + p..f - len f by A49,XREAL_0:def 2;
then
A63: i - len f = 0 by A13;
j - 1 = 0 by A18,A13,A62,XREAL_0:def 2;
hence thesis by A8,A63,FINSEQ_6:179;
end;
suppose
A64: j > len(f:-p);
then Rotate(f,p)/.j = f/.(j + p..f -' len f) by A2,A14,
FINSEQ_6:177;
then Rotate(f,p).j = f/.(j + p..f -' len f) by A6,PARTFUN1:def 6;
then
A65: f/.(j + p..f -' len f) = f/.(i + p..f -' len f) by A5,A9,A53,
PARTFUN1:def 6;
A66: i+p..f -' len f <> 1 or j + p..f -' len f <> len f by A51,
XREAL_0:def 2;
A67: j - (len f - p..f) > 1 by A4,A64,XREAL_1:20;
then
A68: j + p..f - len f > 1;
then
A69: j + p..f -' len f >= 1 by XREAL_0:def 2;
j + p..f <= len f + len f by A23,A14,XREAL_1:7;
then j + p..f - len f <= len f by XREAL_1:20;
then j + p..f -' len f <= len f by A67,XREAL_0:def 2;
then
A70: j + p..f -' len f in dom f by A69,FINSEQ_3:25;
A71: i+p..f -' len f <> len f or j + p..f -' len f <> 1 by A68,
XREAL_0:def 2;
f.(i + p..f -' len f) = f/.(i + p..f -' len f) by A52,
PARTFUN1:def 6
.= f.(j + p..f -' len f) by A65,A70,PARTFUN1:def 6;
then i + p..f -' len f = j + p..f -' len f by A1,A52,A70,A66,A71;
then i + p..f - len f = j + p..f -' len f by A49,XREAL_0:def 2;
then i + p..f - len f = j + p..f - len f by A67,XREAL_0:def 2;
hence thesis;
end;
end;
hence thesis;
end;
end;
hence thesis;
end;
suppose
not p in rng f;
hence thesis by A1,FINSEQ_6:def 2;
end;
end;
theorem Th12:
for D be non empty set for f be FinSequence of D st f is
weakly-one-to-one circular for p be Element of D holds Rotate(f,p) is
weakly-one-to-one
proof
let D be non empty set;
let f be FinSequence of D;
assume
A1: f is weakly-one-to-one circular;
let p be Element of D;
per cases;
suppose
A2: p in rng f;
then
A3: p..f <= len f by FINSEQ_4:21;
A4: len (f:-p) = len f - p..f + 1 by A2,FINSEQ_5:50;
let i be Nat;
1 <= p..f by A2,FINSEQ_4:21;
then
A5: i -' 1 + p..f >= 0+1 by XREAL_1:7;
then
A6: i -' 1 + p..f + 1 > 1 by NAT_1:13;
assume that
A7: 1 <= i and
A8: i < len Rotate(f,p);
A9: i+1 > 1 by A7,NAT_1:13;
i-1+1 >= 1 by A7;
then
A10: i-1 >= 1-1 by XREAL_1:20;
A11: i + 1 -' 1 + p..f = i + 1 - 1 + p..f by A7,XREAL_0:def 2
.= i - 1 + p..f + 1
.= i -' 1 + p..f + 1 by A10,XREAL_0:def 2;
A12: i+1 <= len Rotate(f,p) by A8,NAT_1:13;
A13: len Rotate(f,p) = len f by FINSEQ_6:179;
then
A14: len f > 1 by A7,A8,XXREAL_0:2;
then
A15: len f >= 1+1 by NAT_1:13;
now
per cases by XXREAL_0:1;
suppose
A16: i < len(f:-p);
then i - 1 < len f - p..f by A4,XREAL_1:19;
then i - 1 + p..f < len f by XREAL_1:20;
then
A17: i -' 1 + p..f < len f by A10,XREAL_0:def 2;
then
A18: i -' 1 + p..f + 1 <= len f by NAT_1:13;
Rotate(f,p)/.i = f/.(i -' 1 + p..f) by A2,A7,A16,FINSEQ_6:174
.= f.(i -' 1 + p..f) by A5,A17,FINSEQ_4:15;
then
A19: Rotate(f,p).i = f.(i -' 1 + p..f) by A7,A8,FINSEQ_4:15;
i+1 <= len(f:-p) by A16,NAT_1:13;
then Rotate(f,p)/.(i+1) = f/.(i+1 -' 1 + p..f) by A2,A9,FINSEQ_6:174
.= f.(i+1 -' 1 + p..f) by A6,A11,A18,FINSEQ_4:15;
then Rotate(f,p).(i+1) = f.(i+1 -' 1 + p..f) by A9,A12,FINSEQ_4:15;
hence thesis by A1,A5,A11,A17,A19;
end;
suppose
A20: i = len(f:-p);
then Rotate(f,p)/.i = f/.len f by A2,FINSEQ_6:176
.= f/.1 by A1,FINSEQ_6:def 1
.= f.1 by A14,FINSEQ_4:15;
then
A21: Rotate(f,p).i = f.1 by A7,A8,FINSEQ_4:15;
A22: i + 1 + p..f -' len f = len f + (1+1) - len f by A4,A20,XREAL_0:def 2
.= 2;
i + 1 > len(f:-p) by A20,NAT_1:13;
then Rotate(f,p)/.(i+1) = f/.(i + 1 + p..f -' len f) by A2,A13,A12,
FINSEQ_6:177
.= f.(i + 1 + p..f -' len f) by A15,A22,FINSEQ_4:15;
then Rotate(f,p).(i+1) = f.(1+1) by A9,A12,A22,FINSEQ_4:15;
hence thesis by A1,A14,A21;
end;
suppose
A23: i > len(f:-p);
then
A24: i - (len f - p..f) > 1 by A4,XREAL_1:20;
then i + p..f - len f > 1-1 by XXREAL_0:2;
then
A25: i + p..f - len f + 1 > 1 by XREAL_1:19;
then
A26: i + 1 + p..f -' len f = i + 1 + p..f - len f by XREAL_0:def 2
.= i + p..f - len f + 1
.= i + p..f -' len f + 1 by A24,XREAL_0:def 2;
i+1 + p..f <= len f + len f by A3,A13,A12,XREAL_1:7;
then i+1 + p..f - len f <= len f by XREAL_1:20;
then
A27: i+1 + p..f -' len f <= len f by A25,XREAL_0:def 2;
i+1 + p..f - len f > 1 by A25;
then
A28: i+1 + p..f -' len f > 1 by XREAL_0:def 2;
i+1 > len(f:-p) by A23,NAT_1:13;
then Rotate(f,p)/.(i+1) = f/.(i+1 + p..f -' len f) by A2,A13,A12,
FINSEQ_6:177
.= f.(i+1 + p..f -' len f) by A28,A27,FINSEQ_4:15;
then
A29: Rotate(f,p).(i+1) = f.(i+1+p..f -' len f) by A9,A12,FINSEQ_4:15;
i + p..f - len f > 1 by A24;
then
A30: i + p..f -' len f > 1 by XREAL_0:def 2;
i + p..f < len f + len f by A3,A13,A8,XREAL_1:8;
then i + p..f - len f < len f by XREAL_1:19;
then
A31: i + p..f -' len f < len f by A24,XREAL_0:def 2;
Rotate(f,p)/.i = f/.(i + p..f -' len f) by A2,A13,A8,A23,
FINSEQ_6:177
.= f.(i + p..f -' len f) by A30,A31,FINSEQ_4:15;
then Rotate(f,p).i = f.(i + p..f -' len f) by A7,A8,FINSEQ_4:15;
hence thesis by A1,A30,A31,A29,A26;
end;
end;
hence thesis;
end;
suppose
not p in rng f;
hence thesis by A1,FINSEQ_6:def 2;
end;
end;
theorem Th13:
for D be non empty set for f be FinSequence of D st f is
poorly-one-to-one circular for p be Element of D holds Rotate(f,p) is
poorly-one-to-one
proof
let D be non empty set;
let f be FinSequence of D;
assume
A1: f is poorly-one-to-one circular;
let p be Element of D;
A2: len Rotate(f,p) = len f by FINSEQ_6:179;
per cases;
suppose
A3: len f <> 2;
then f is weakly-one-to-one by A1,Th7;
then Rotate(f,p) is weakly-one-to-one by A1,Th12;
hence thesis by A2,A3,Th7;
end;
suppose
len f = 2;
hence thesis by A2,Def3;
end;
end;
registration
let D be non empty set;
cluster one-to-one circular non empty for FinSequence of D;
existence
proof
set x = the Element of D;
<*x*>/.1 = <*x*>/.len <*x*> by FINSEQ_1:39;
then <*x*> is circular by FINSEQ_6:def 1;
hence thesis;
end;
end;
registration
let D be non empty set;
let f be almost-one-to-one FinSequence of D;
let p be Element of D;
cluster Rotate(f,p) -> almost-one-to-one;
coherence by Th11;
end;
registration
let D be non empty set;
let f be circular weakly-one-to-one FinSequence of D;
let p be Element of D;
cluster Rotate(f,p) -> weakly-one-to-one;
coherence by Th12;
end;
registration
let D be non empty set;
let f be circular poorly-one-to-one FinSequence of D;
let p be Element of D;
cluster Rotate(f,p) -> poorly-one-to-one;
coherence by Th13;
end;
theorem Th14:
for D be non empty set for f be FinSequence of D holds f is
almost-one-to-one iff f/^1 is one-to-one & f|(len f-'1) is one-to-one
proof
let D be non empty set;
let f be FinSequence of D;
A1: len (f/^1) = len f-'1 by RFINSEQ:29;
thus f is almost-one-to-one implies f/^1 is one-to-one & f|(len f-'1) is
one-to-one
proof
assume
A2: f is almost-one-to-one;
thus f/^1 is one-to-one
proof
let x,y be object;
assume that
A3: x in dom (f/^1) and
A4: y in dom (f/^1) and
A5: (f/^1).x = (f/^1).y;
reconsider i=x, j=y as Nat by A3,A4;
A6: i in Seg len (f/^1) by A3,FINSEQ_1:def 3;
then
A7: 1 <= i by FINSEQ_1:1;
A8: i <= len (f/^1) by A6,FINSEQ_1:1;
then len f-'1 >= 1 by A1,A7,XXREAL_0:2;
then
A9: len f-'1 = len f-1 by NAT_D:39;
then
A10: i+1 <= len f by A1,A8,XREAL_1:19;
then
A11: (f/^1).i = f.(i+1) by A7,FINSEQ_6:114;
A12: j in Seg len (f/^1) by A4,FINSEQ_1:def 3;
then
A13: 1 <= j by FINSEQ_1:1;
j <= len (f/^1) by A12,FINSEQ_1:1;
then
A14: j+1 <= len f by A1,A9,XREAL_1:19;
then
A15: (f/^1).j = f.(j+1) by A13,FINSEQ_6:114;
A16: j+1 > 1 by A13,NAT_1:13;
then
A17: j+1 in dom f by A14,FINSEQ_3:25;
A18: i+1 > 1 by A7,NAT_1:13;
then i+1 in dom f by A10,FINSEQ_3:25;
then i+1 = j+1 by A2,A5,A11,A15,A18,A16,A17;
hence thesis;
end;
A19: len (f|(len f-'1)) = len f-'1 by FINSEQ_1:59,NAT_D:35;
thus f|(len f-'1) is one-to-one
proof
let x,y be object;
assume that
A20: x in dom (f|(len f-'1)) and
A21: y in dom (f|(len f-'1)) and
A22: (f|(len f-'1)).x = (f|(len f-'1)).y;
reconsider i=x, j=y as Nat by A20,A21;
A23: i in Seg len (f|(len f-'1)) by A20,FINSEQ_1:def 3;
then
A24: 1 <= i by FINSEQ_1:1;
A25: j in Seg len (f|(len f-'1)) by A21,FINSEQ_1:def 3;
then
A26: j <= len (f|(len f-'1)) by FINSEQ_1:1;
then
A27: (f|(len f-'1)).j = f.j by A19,FINSEQ_3:112;
A28: i <= len (f|(len f-'1)) by A23,FINSEQ_1:1;
then
A29: (f|(len f-'1)).i = f.i by A19,FINSEQ_3:112;
len f-'1 >= 1 by A19,A24,A28,XXREAL_0:2;
then
A30: len f-'1 = len f-1 by NAT_D:39;
then j+1 <= len f by A19,A26,XREAL_1:19;
then
A31: j < len f by NAT_1:13;
1 <= j by A25,FINSEQ_1:1;
then
A32: j in dom f by A31,FINSEQ_3:25;
i+1 <= len f by A19,A28,A30,XREAL_1:19;
then
A33: i < len f by NAT_1:13;
then i in dom f by A24,FINSEQ_3:25;
hence thesis by A2,A22,A29,A27,A33,A31,A32;
end;
end;
assume that
A34: f/^1 is one-to-one and
A35: f|(len f-'1) is one-to-one;
let i,j be Nat;
assume that
A36: i in dom f and
A37: j in dom f and
A38: i <> 1 or j <> len f and
A39: i <> len f or j <> 1 and
A40: f.i = f.j;
A41: 0+1 <= i by A36,FINSEQ_3:25;
then
A42: i-1 >= 0 by XREAL_1:19;
A43: i <= len f by A36,FINSEQ_3:25;
then
A44: i-1 <= len f-1 by XREAL_1:9;
then i-'1 <= len f-1 by A42,XREAL_0:def 2;
then
A45: i-'1 <= len f-'1 by XREAL_0:def 2;
len f = len f-'1+1 by A41,A43,XREAL_1:235,XXREAL_0:2;
then len f-'1 <= len f by NAT_1:13;
then
A46: len (f|(len f-'1)) = len f-'1 by FINSEQ_1:59;
A47: j <= len f by A37,FINSEQ_3:25;
then j-1 <= len f-1 by XREAL_1:9;
then j-'1 <= len f-1 by A42,A44,XREAL_0:def 2;
then
A48: j-'1 <= len f-'1 by XREAL_0:def 2;
f is non empty by A36;
then
A49: f = <* f/.1 *> ^ (f/^1) by FINSEQ_5:29;
A50: i = i-'1+1 by A41,XREAL_1:235;
A51: 0+1 <= j by A37,FINSEQ_3:25;
then
A52: j-1 >= 0 by XREAL_1:19;
A53: j = j-'1+1 by A51,XREAL_1:235;
per cases;
suppose
A54: i <> 1 & j <> 1;
then j > 0+1 by A51,XXREAL_0:1;
then j-1 > 0 by XREAL_1:20;
then j-'1 > 0 by XREAL_0:def 2;
then j-'1 >= 0+1 by NAT_1:13;
then
A55: j-'1 in dom (f/^1) by A1,A48,FINSEQ_3:25;
then
A56: f.j = (f/^1).(j-'1) by A53,A49,FINSEQ_3:103;
i > 0+1 by A41,A54,XXREAL_0:1;
then i-1 > 0 by XREAL_1:20;
then i-'1 > 0 by XREAL_0:def 2;
then i-'1 >= 0+1 by NAT_1:13;
then
A57: i-'1 in dom (f/^1) by A1,A45,FINSEQ_3:25;
then f.i = (f/^1).(i-'1) by A50,A49,FINSEQ_3:103;
then i-'1 = j-'1 by A34,A40,A57,A55,A56;
then i-1 = j-'1 by A42,XREAL_0:def 2;
then i-1 = j-1 by A52,XREAL_0:def 2;
hence thesis;
end;
suppose
A58: i = 1;
then j < len f by A38,A47,XXREAL_0:1;
then j+1 <= len f by NAT_1:13;
then j <= len f-1 by XREAL_1:19;
then
A59: j <= len f-'1 by XREAL_0:def 2;
then
A60: (f|(len f-'1)).j = f.j by FINSEQ_3:112;
i <= len f-'1 by A51,A58,A59,XXREAL_0:2;
then
A61: i in dom(f|(len f-'1)) by A41,A46,FINSEQ_3:25;
A62: j in dom(f|(len f-'1)) by A51,A46,A59,FINSEQ_3:25;
(f|(len f-'1)).i = f.i by A51,A58,A59,FINSEQ_3:112,XXREAL_0:2;
hence thesis by A35,A40,A60,A61,A62;
end;
suppose
A63: j = 1;
then i < len f by A39,A43,XXREAL_0:1;
then i+1 <= len f by NAT_1:13;
then i <= len f-1 by XREAL_1:19;
then
A64: i <= len f-'1 by XREAL_0:def 2;
then
A65: (f|(len f-'1)).i = f.i by FINSEQ_3:112;
j <= len f-'1 by A41,A63,A64,XXREAL_0:2;
then
A66: j in dom(f|(len f-'1)) by A51,A46,FINSEQ_3:25;
A67: i in dom(f|(len f-'1)) by A41,A46,A64,FINSEQ_3:25;
(f|(len f-'1)).j = f.j by A41,A63,A64,FINSEQ_3:112,XXREAL_0:2;
hence thesis by A35,A40,A65,A67,A66;
end;
end;
registration
let C be compact non vertical non horizontal Subset of TOP-REAL 2;
let n be Nat;
cluster Cage(C,n) -> almost-one-to-one;
coherence
proof
len Cage(C,n) > 0+1 by GOBOARD7:34,XXREAL_0:2;
then len Cage(C,n)-1 > 0 by XREAL_1:20;
then
A1: len Cage(C,n)-'1 = len Cage(C,n)-1 by XREAL_0:def 2;
A2: len Cage(C,n) > 4 by GOBOARD7:34;
len Cage(C,n) < len Cage(C,n)+1 by NAT_1:13;
then len Cage(C,n)-'1 < len Cage(C,n) by A1,XREAL_1:19;
then
A3: Cage(C,n)|(len Cage(C,n)-'1) is one-to-one by A2,TOPREAL8:22;
Cage(C,n) /^ 1 is one-to-one;
hence thesis by A3,Th14;
end;
end;
registration
let C be compact non vertical non horizontal Subset of TOP-REAL 2;
let n be Nat;
cluster Cage(C,n) -> weakly-one-to-one;
coherence
proof
len Cage(C,n) > 2 by GOBOARD7:34,XXREAL_0:2;
hence thesis by Th7;
end;
end;
theorem Th15: :: JORDAN5B:24
for f be FinSequence of TOP-REAL 2 for p be Point of TOP-REAL 2
st p in L~f & f is weakly-one-to-one holds B_Cut(f,p,p) = <*p*>
proof
let f be FinSequence of TOP-REAL 2;
let p be Point of TOP-REAL 2;
assume that
A1: p in L~f and
A2: f is weakly-one-to-one;
A3: 1 <= Index(p,f) by A1,JORDAN3:8;
L_Cut(f,p).1 = p by A1,JORDAN3:23;
then
A4: R_Cut(L_Cut(f,p),p) = <*p*> by JORDAN3:def 4;
A5: Index(p,f) < len f by A1,JORDAN3:8;
then
A6: Index(p,f)+1 <= len f by NAT_1:13;
then
A7: Index(p,f) + 1 in dom f by A3,SEQ_4:134;
f.Index(p,f) <> f.(Index(p,f)+1) by A2,A5,A3;
then
A8: f.Index(p,f) <> f/.(Index(p,f)+1) by A7,PARTFUN1:def 6;
Index(p,f) in dom f by A3,A6,SEQ_4:134;
then
A9: f/.Index(p,f) <> f/.(Index(p,f)+1) by A8,PARTFUN1:def 6;
p in LSeg(f,Index(p,f)) by A1,JORDAN3:9;
then p in LSeg(f/.Index(p,f), f/.(Index(p,f)+1)) by A3,A6,TOPREAL1:def 3;
then LE p,p,f/.Index(p,f),f/.(Index(p,f)+1) by A9,JORDAN5B:9;
hence thesis by A4,JORDAN3:def 7;
end;
theorem Th16:
for f being FinSequence st f is one-to-one holds f is weakly-one-to-one
proof
let f be FinSequence;
assume
A1: f is one-to-one;
for i be Nat st 1 <= i & i < len f holds f.i <> f.(i+1)
proof
let i be Nat;
assume that
A2: 1 <= i and
A3: i < len f;
A4: i+1 in dom f by A2,A3,MSUALG_8:1;
A5: i <> i+1;
i in dom f by A2,A3,MSUALG_8:1;
hence thesis by A1,A4,A5;
end;
hence thesis;
end;
registration
cluster one-to-one -> weakly-one-to-one for FinSequence;
coherence by Th16;
end;
theorem Th17:
for f be FinSequence of TOP-REAL 2 st f is weakly-one-to-one for
p,q be Point of TOP-REAL 2 st p in L~f & q in L~f holds B_Cut(f,p,q) = Rev
B_Cut(f,q,p)
proof
let f be FinSequence of TOP-REAL 2;
assume
A1: f is weakly-one-to-one;
let p,q be Point of TOP-REAL 2 such that
A2: p in L~f and
A3: q in L~f;
per cases;
suppose
A4: p = q;
then B_Cut(f,p,q) = <*p*> by A1,A2,Th15;
hence thesis by A4,FINSEQ_5:60;
end;
suppose that
A5: p <> q and
A6: Index(p,f)<Index(q,f) or Index(p,f)=Index(q,f) & LE p,q,f/.Index(p
,f),f/.(Index(p,f)+1);
not (Index(q,f)=Index(p,f) & LE q,p,f/.(Index(q,f)),f/.(Index(q,f)+1)
) by A5,A6,JORDAN3:27;
then
A7: Rev B_Cut(f,q,p) = Rev Rev (R_Cut(L_Cut(f,p),q)) by A6,JORDAN3:def 7;
B_Cut(f,p,q) = R_Cut(L_Cut(f,p),q) by A2,A3,A6,JORDAN3:def 7;
hence thesis by A7;
end;
suppose that
p <> q and
A8: not(Index(p,f)<Index(q,f) or Index(p,f)=Index(q,f) & LE p,q,f/.
Index(p,f),f/.(Index(p,f)+1));
A9: Index(q,f) < Index(p,f) or Index(p,f)=Index(q,f) & not LE p,q,f/.
Index(p,f),f/.(Index(p,f)+1) by A8,XXREAL_0:1;
A10: now
assume that
A11: Index(p,f)=Index(q,f) and
A12: not LE p,q,f/.Index(p,f),f/.(Index(p,f)+1);
A13: 1 <= Index(p,f) by A2,JORDAN3:8;
A14: Index(p,f) < len f by A2,JORDAN3:8;
then
A15: Index(p,f)+1 <= len f by NAT_1:13;
then
A16: LSeg(f,Index(p,f)) = LSeg(f/.Index(p,f),f/.(Index(p,f)+1)) by A13,
TOPREAL1:def 3;
then
A17: p in LSeg(f/.Index(p,f),f/.(Index(p,f)+1)) by A2,JORDAN3:9;
1 <= Index(p,f)+1 by NAT_1:11;
then
A18: Index(p,f)+1 in dom f by A15,FINSEQ_3:25;
f.Index(p,f) <> f.(Index(p,f)+1) by A1,A13,A14;
then
A19: f.Index(p,f) <> f/.(Index(p,f)+1) by A18,PARTFUN1:def 6;
Index(p,f) in dom f by A13,A14,FINSEQ_3:25;
then
A20: f/.Index(p,f) <> f/.(Index(p,f)+1) by A19,PARTFUN1:def 6;
q in LSeg(f/.Index(p,f),f/.(Index(p,f)+1)) by A3,A11,A16,JORDAN3:9;
then LT q,p,f/.Index(p,f),f/.(Index(p,f)+1) by A12,A17,A20,JORDAN3:28;
hence LE q,p,f/.Index(q,f),f/.(Index(q,f)+1) by A11,JORDAN3:def 6;
end;
B_Cut(f,p,q) = Rev R_Cut(L_Cut(f,q),p) by A8,JORDAN3:def 7;
hence thesis by A2,A3,A9,A10,JORDAN3:def 7;
end;
end;
theorem Th18:
for f be FinSequence of TOP-REAL 2 for p be Point of TOP-REAL 2
for i1 be Nat st f is poorly-one-to-one unfolded s.n.c. & 1<i1 & i1
<=len f & p=f.i1 holds Index(p,f) + 1 = i1
proof
let f be FinSequence of TOP-REAL 2;
let p be Point of TOP-REAL 2,i1 be Nat;
assume
A1: f is poorly-one-to-one unfolded s.n.c.;
assume that
A2: 1<i1 and
A3: i1<=len f;
consider j being Nat such that
A4: i1 = j+1 by A2,NAT_1:6;
reconsider j as Nat;
A5: 1 + 0 <= j by A2,A4,NAT_1:13;
assume
A6: p=f.i1;
assume
A7: Index(p,f) + 1 <> i1;
A8: j in NAT by ORDINAL1:def 12;
i1 in dom f by A2,A3,FINSEQ_3:25;
then p = f/.i1 by A6,PARTFUN1:def 6;
then
A9: p in LSeg(f,j) by A3,A4,A5,TOPREAL1:21;
then Index(p,f) <= j by A8,JORDAN3:7;
then Index(p,f) < j by A4,A7,XXREAL_0:1;
then
A10: Index(p,f) + 1 <= j by NAT_1:13;
A11: LSeg(f,j) c= L~f by TOPREAL3:19;
then
A12: p in LSeg(f,Index(p,f)) by A9,JORDAN3:9;
per cases by A10,XXREAL_0:1;
suppose
A13: Index(p,f) + 1 = j;
A14: 1 <= Index(p,f) by A9,A11,JORDAN3:8;
then Index(p,f) + 2 >= 1+2 by XREAL_1:7;
then len f >= 2+1 by A3,A4,A13,XXREAL_0:2;
then
A15: len f > 2 by NAT_1:13;
Index(p,f) + (1+1) <= len f by A3,A4,A13;
then LSeg(f,Index(p,f)) /\ LSeg(f,j) = {f/.j} by A1,A13,A14,TOPREAL1:def 6;
then
A16: p in {f/.j} by A9,A12,XBOOLE_0:def 4;
A17: j < len f by A3,A4,NAT_1:13;
then j in dom f by A5,FINSEQ_3:25;
then f.j = f/.j by PARTFUN1:def 6
.= f.i1 by A6,A16,TARSKI:def 1;
hence contradiction by A1,A4,A5,A17,A15,Def3;
end;
suppose
A18: Index(p,f) + 1 < j;
p in LSeg(f,Index(p,f)) /\ LSeg(f,j) by A9,A12,XBOOLE_0:def 4;
then LSeg(f,Index(p,f)) meets LSeg(f,j);
hence contradiction by A1,A18,TOPREAL1:def 7;
end;
end;
theorem Th19:
for f be FinSequence of TOP-REAL 2 st f is weakly-one-to-one for
p,q be Point of TOP-REAL 2 st p in L~f & q in L~f holds B_Cut(f,p,q)/.1 = p
proof
let f be FinSequence of TOP-REAL 2;
assume
A1: f is weakly-one-to-one;
let p,q be Point of TOP-REAL 2;
assume that
A2: p in L~f and
A3: q in L~f;
A4: Index(p,f) < len f by A2,JORDAN3:8;
A5: 1 <= Index(p,f) by A2,JORDAN3:8;
then
A6: Index(p,f) in dom f by A4,FINSEQ_3:25;
A7: 1 <= len L_Cut(f,p) by A2,Th1;
per cases;
suppose
A8: p <> q;
now
per cases;
suppose
A9: p in L~f & q in L~f & Index(p,f)<Index(q,f);
then q in L~L_Cut(f,p) by JORDAN3:29;
then (R_Cut(L_Cut(f,p),q))/.1 = L_Cut(f,p)/.1 by SPRECT_3:22
.= L_Cut(f,p).1 by A7,FINSEQ_4:15
.= p by A9,JORDAN3:23;
hence thesis by A9,JORDAN3:def 7;
end;
suppose
A10: Index(p,f)=Index(q,f) & LE p,q,f/.(Index(p,f)),f/.(Index(p,f) +1);
then q in L~L_Cut(f,p) by A2,A3,A8,JORDAN3:31;
then (R_Cut(L_Cut(f,p),q))/.1 = L_Cut(f,p)/.1 by SPRECT_3:22
.= L_Cut(f,p).1 by A7,FINSEQ_4:15
.= p by A2,JORDAN3:23;
hence thesis by A10,JORDAN3:def 7;
end;
suppose
A11: not (p in L~f & q in L~f & Index(p,f)<Index(q,f)) & not(Index
(p,f)=Index(q,f) & LE p,q,f/.(Index(p,f)),f/.(Index(p,f)+1));
then
A12: B_Cut(f,p,q) = Rev (R_Cut(L_Cut(f,q),p)) by JORDAN3:def 7;
now
per cases by A2,A3,A11,XXREAL_0:1;
suppose
Index(p,f) > Index(q,f);
then
A13: p in L~L_Cut(f,q) by A2,A3,JORDAN3:29;
R_Cut(L_Cut(f,q),p) <> {} by JORDAN1J:44;
hence
B_Cut(f,p,q)/.1 = R_Cut(L_Cut(f,q),p)/.len R_Cut(L_Cut(f,q),p
) by A12,FINSEQ_5:65
.= p by A13,JORDAN1J:45;
end;
suppose
A14: Index(p,f) = Index(q,f);
A15: Index(p,f)+1 >= 1 by NAT_1:11;
Index(p,f)+1 <= len f by A4,NAT_1:13;
then
A16: Index(p,f)+1 in dom f by A15,FINSEQ_3:25;
set Ls = LSeg(f/.(Index(p,f)),f/.(Index(p,f)+1));
A17: q in Ls by A3,A14,JORDAN5B:29;
A18: p in Ls by A2,JORDAN5B:29;
f.Index(p,f) <> f.(Index(p,f)+1) by A1,A5,A4;
then f.Index(p,f) <> f/.(Index(p,f)+1) by A16,PARTFUN1:def 6;
then
A19: f/.Index(p,f) <> f/.(Index(p,f)+1) by A6,PARTFUN1:def 6;
then
A20: Ls is_an_arc_of f/.(Index(p,f)),f/.(Index(p,f)+1) by TOPREAL1:9;
not LE p,q,Ls,f/.(Index(p,f)),f/.(Index(p,f)+1) by A11,A14,A19,
JORDAN5C:17;
then LE q,p,Ls,f/.(Index(p,f)),f/.(Index(p,f)+1) by A8,A20,A18,A17,
JORDAN5C:14;
then
A21: p in L~(L_Cut(f,q)) by A2,A3,A8,A14,A19,JORDAN3:31,JORDAN5C:17;
R_Cut(L_Cut(f,q),p) <> {} by JORDAN1J:44;
hence
B_Cut(f,p,q)/.1 = R_Cut(L_Cut(f,q),p)/.len R_Cut(L_Cut(f,q),p
) by A12,FINSEQ_5:65
.= p by A21,JORDAN1J:45;
end;
end;
hence thesis;
end;
end;
hence thesis;
end;
suppose
p = q;
then B_Cut(f,p,q) = <*p*> by A1,A2,Th15;
hence thesis by FINSEQ_4:16;
end;
end;
theorem Th20:
for f be FinSequence of TOP-REAL 2 st f is weakly-one-to-one for
p,q be Point of TOP-REAL 2 st p in L~f & q in L~f holds B_Cut(f,p,q)/.len B_Cut
(f,p,q) = q
proof
let f be FinSequence of TOP-REAL 2;
assume
A1: f is weakly-one-to-one;
let p,q be Point of TOP-REAL 2 such that
A2: p in L~f and
A3: q in L~f;
A4: B_Cut(f,q,p) <> {} by Th3;
B_Cut(f,p,q) = Rev B_Cut(f,q,p) by A1,A2,A3,Th17;
hence B_Cut(f,p,q)/.len B_Cut(f,p,q) = Rev B_Cut(f,q,p)/.len B_Cut(f,q,p) by
FINSEQ_5:def 3
.= B_Cut(f,q,p)/.1 by A4,FINSEQ_5:65
.= q by A1,A2,A3,Th19;
end;
theorem
for f be FinSequence of TOP-REAL 2 for p be Point of TOP-REAL 2 st p
in L~f holds L~L_Cut(f,p) c= L~f
proof
let f be FinSequence of TOP-REAL 2;
let p be Point of TOP-REAL 2 such that
A1: p in L~f;
Index(p,f)<len f by A1,JORDAN3:8;
then
A2: Index(p,f)+1<=len f by NAT_1:13;
len f <> 0 by A1,TOPREAL1:22;
then len f > 0 by NAT_1:3;
then
A3: len f >= 0+1 by NAT_1:13;
then
A4: len f in dom f by FINSEQ_3:25;
A5: 1<=Index(p,f) by A1,JORDAN3:8;
then
A6: 1<Index(p,f)+1 by NAT_1:13;
then
A7: Index(p,f)+1 in dom f by A2,FINSEQ_3:25;
per cases;
suppose
p = f.(Index(p,f)+1);
then L_Cut(f,p) = mid(f,Index(p,f)+1,len f) by JORDAN3:def 3;
hence thesis by A3,A6,A2,JORDAN4:35;
end;
suppose
p <> f.(Index(p,f)+1);
then
A8: L_Cut(f,p) = <*p*>^mid(f,Index(p,f)+1,len f) by JORDAN3:def 3;
A9: f/.(Index(p,f)+1) in LSeg(f/.(Index(p,f)),f/.(Index(p,f)+1)) by RLTOPSP1:68
;
p in LSeg(f,Index(p,f)) by A1,JORDAN3:9;
then
A10: p in LSeg(f/.(Index(p,f)),f/.(Index(p,f)+1)) by A5,A2,TOPREAL1:def 3;
A11: LSeg(f/.(Index(p,f)),f/.(Index(p,f)+1)) c= L~f by A1,A2,JORDAN3:8
,SPPOL_2:16;
mid(f,Index(p,f)+1,len f)/.1 = f/.(Index(p,f)+1) by A4,A7,SPRECT_2:8;
then LSeg(p,mid(f,Index(p,f)+1,len f)/.1) c= LSeg(f/.(Index(p,f)),f/.(
Index(p,f)+1)) by A10,A9,TOPREAL1:6;
then
A12: LSeg(p,mid(f,Index(p,f)+1,len f)/.1) c= L~f by A11;
len mid(f,Index(p,f)+1,len f) >= 0+1 by A4,A7,SPRECT_2:5;
then mid(f,Index(p,f)+1,len f) <> {};
then
A13: L~(<*p*>^mid(f,Index(p,f)+1,len f)) = LSeg(p,mid(f,Index(p,f)+1,len f
)/.1) \/ L~mid(f,Index(p,f)+1,len f) by SPPOL_2:20;
L~mid(f,Index(p,f)+1,len f) c= L~f by A3,A6,A2,JORDAN4:35;
hence thesis by A8,A13,A12,XBOOLE_1:8;
end;
end;
theorem
for f be FinSequence of TOP-REAL 2 for p,q be Point of TOP-REAL 2 st p
in L~f & q in L~f & f is weakly-one-to-one holds L~B_Cut(f,p,q) c= L~f
proof
let f be FinSequence of TOP-REAL 2;
let p,q be Point of TOP-REAL 2 such that
A1: p in L~f and
A2: q in L~f and
A3: f is weakly-one-to-one;
per cases;
suppose
p = q;
then B_Cut(f,p,q) = <*p*> by A1,A3,Th15;
then len B_Cut(f,p,q) = 1 by FINSEQ_1:39;
then L~B_Cut(f,p,q) = {} by TOPREAL1:22;
hence thesis;
end;
suppose
p <> q & (Index(p,f)<Index(q,f) or Index(p,f)=Index(q,f) & LE p,q,
f/.Index(p,f),f/.(Index(p,f)+1));
hence thesis by A1,A2,JORDAN5B:33;
end;
suppose that
A4: p <> q and
A5: not(Index(p,f)<Index(q,f) or Index(p,f)=Index(q,f) & LE p,q,f/.
Index(p,f),f/.(Index(p,f)+1));
A6: now
assume that
A7: Index(p,f)=Index(q,f) and
A8: not LE p,q,f/.Index(p,f),f/.(Index(p,f)+1);
A9: Index(p,f) < len f by A1,JORDAN3:8;
A10: 1 <= Index(p,f) by A1,JORDAN3:8;
then
A11: Index(p,f) in dom f by A9,FINSEQ_3:25;
A12: Index(p,f)+1 <= len f by A9,NAT_1:13;
then
A13: LSeg(f,Index(p,f)) = LSeg(f/.Index(p,f),f/.(Index(p,f)+1)) by A10,
TOPREAL1:def 3;
then
A14: p in LSeg(f/.Index(p,f),f/.(Index(p,f)+1)) by A1,JORDAN3:9;
f.Index(p,f) <> f.(Index(p,f)+1) by A3,A10,A9;
then
A15: f/.Index(p,f) <> f.(Index(p,f)+1) by A11,PARTFUN1:def 6;
1 <= Index(p,f)+1 by NAT_1:11;
then Index(p,f)+1 in dom f by A12,FINSEQ_3:25;
then
A16: f/.Index(p,f) <> f/.(Index(p,f)+1) by A15,PARTFUN1:def 6;
q in LSeg(f/.Index(p,f),f/.(Index(p,f)+1)) by A2,A7,A13,JORDAN3:9;
then LT q,p,f/.Index(p,f),f/.(Index(p,f)+1) by A8,A14,A16,JORDAN3:28;
hence LE q,p,f/.Index(q,f),f/.(Index(q,f)+1) by A7,JORDAN3:def 6;
end;
A17: Index(q,f) < Index(p,f) or Index(p,f)=Index(q,f) & not LE p,q,f/.
Index(p,f),f/.(Index(p,f)+1) by A5,XXREAL_0:1;
then
A18: L~B_Cut(f,q,p) c= L~f by A1,A2,A4,A6,JORDAN5B:33;
B_Cut(f,p,q)=Rev R_Cut(L_Cut(f,q),p) by A5,JORDAN3:def 7;
then Rev B_Cut(f,q,p) = B_Cut(f,p,q) by A1,A2,A17,A6,JORDAN3:def 7;
hence thesis by A18,SPPOL_2:22;
end;
end;
theorem Th23:
for f,g be FinSequence holds dom f c= dom (f^'g)
proof
let f,g be FinSequence;
len f <= len(f^'g) by TOPREAL8:7;
hence thesis by FINSEQ_3:30;
end;
theorem
for f be non empty FinSequence for g be FinSequence holds dom g c= dom (f^'g)
proof
let f be non empty FinSequence;
let g be FinSequence;
len g <= len(f^'g) by TOPREAL8:9;
hence thesis by FINSEQ_3:30;
end;
theorem Th25:
for f,g be FinSequence st f^'g is constant holds f is constant
proof
let f,g be FinSequence;
assume f^'g is constant;
then reconsider h = f^'g as constant FinSequence;
rng f c= rng h by TOPREAL8:10;
hence thesis;
end;
theorem
for f,g be FinSequence st f^'g is constant & f.len f = g.1 & f <> {}
holds g is constant
proof
let f,g be FinSequence;
assume that
A1: f^'g is constant and
A2: f.len f = g.1 and
A3: f <> {};
reconsider h = f^'g as constant FinSequence by A1;
per cases;
suppose
g <> {};
then rng h = rng f \/ rng g by A2,A3,FINSEQ_6:144;
then rng g c= rng h by XBOOLE_1:7;
hence thesis;
end;
suppose
g = {};
hence thesis;
end;
end;
theorem Th27:
for f be special FinSequence of TOP-REAL 2 for i,j be Nat
holds mid(f,i,j) is special
proof
let f be special FinSequence of TOP-REAL 2;
let i,j be Nat;
per cases;
suppose
i <= j;
then mid(f,i,j) = (f/^(i-'1))|(j-'i+1) by FINSEQ_6:def 3;
hence thesis;
end;
suppose
j < i;
then mid(f,j,i) = (f/^(j-'1))|(i-'j+1) by FINSEQ_6:def 3;
then Rev mid(f,i,j) is special by FINSEQ_6:196;
then Rev Rev mid(f,i,j) is special by SPPOL_2:40;
hence thesis;
end;
end;
theorem Th28:
for f be unfolded FinSequence of TOP-REAL 2 for i,j be Nat
holds mid(f,i,j) is unfolded
proof
let f be unfolded FinSequence of TOP-REAL 2;
let i,j be Nat;
per cases;
suppose
i <= j;
then mid(f,i,j) = (f/^(i-'1))|(j-'i+1) by FINSEQ_6:def 3;
hence thesis;
end;
suppose
j < i;
then mid(f,j,i) = (f/^(j-'1))|(i-'j+1) by FINSEQ_6:def 3;
then Rev mid(f,i,j) is unfolded by FINSEQ_6:196;
then Rev Rev mid(f,i,j) is unfolded by SPPOL_2:28;
hence thesis;
end;
end;
theorem Th29:
for f be FinSequence of TOP-REAL 2 st f is special for p be
Point of TOP-REAL 2 st p in L~f holds L_Cut(f,p) is special
proof
let f be FinSequence of TOP-REAL 2;
assume
A1: f is special;
let p be Point of TOP-REAL 2;
A2: mid(f,Index(p,f)+1,len f) is special by A1,Th27;
A3: <*p*>/.1 = p by FINSEQ_4:16;
assume
A4: p in L~f;
then Index(p,f) < len f by JORDAN3:8;
then
A5: Index(p,f)+1 <= len f by NAT_1:13;
1 <= Index(p,f) by A4,JORDAN3:8;
then
A6: LSeg(f,Index(p,f)) = LSeg(f/.Index(p,f), f/.(Index(p,f)+1)) by A5,
TOPREAL1:def 3;
A7: now
per cases by A1,SPPOL_1:19;
case
LSeg(f,Index(p,f)) is vertical;
hence p`1=(f/.(Index(p,f)+1))`1 by A4,A6,JORDAN5B:29,SPPOL_1:41;
end;
case
LSeg(f,Index(p,f)) is horizontal;
hence p`2=(f/.(Index(p,f)+1))`2 by A4,A6,JORDAN5B:29,SPPOL_1:40;
end;
end;
A8: len <*p*> = 1 by FINSEQ_1:39;
len f <> 0 by A4,TOPREAL1:22;
then len f > 0 by NAT_1:3;
then len f >= 0+1 by NAT_1:13;
then
A9: len f in dom f by FINSEQ_3:25;
Index(p,f)+1 >= 1 by NAT_1:11;
then Index(p,f)+1 in dom f by A5,FINSEQ_3:25;
then
A10: mid(f,Index(p,f)+1,len f)/.1 = f/.(Index(p,f)+1) by A9,SPRECT_2:8;
per cases;
suppose
p <> f.(Index(p,f)+1);
then L_Cut(f,p) = <*p*>^mid(f,Index(p,f)+1,len f) by JORDAN3:def 3;
hence thesis by A2,A8,A3,A10,A7,GOBOARD2:8;
end;
suppose
p = f.(Index(p,f)+1);
hence thesis by A2,JORDAN3:def 3;
end;
end;
theorem Th30:
for f be FinSequence of TOP-REAL 2 st f is special for p be
Point of TOP-REAL 2 st p in L~f holds R_Cut(f,p) is special
proof
let f be FinSequence of TOP-REAL 2;
assume
A1: f is special;
let p be Point of TOP-REAL 2;
A2: mid(f,1,Index(p,f)) is special by A1,Th27;
assume
A3: p in L~f;
then
A4: Index(p,f) < len f by JORDAN3:8;
len f <> 0 by A3,TOPREAL1:22;
then len f > 0 by NAT_1:3;
then len f >= 0+1 by NAT_1:13;
then
A5: 1 in dom f by FINSEQ_3:25;
A6: 1 <= Index(p,f) by A3,JORDAN3:8;
then Index(p,f) in dom f by A4,FINSEQ_3:25;
then
A7: mid(f,1,Index(p,f))/.len mid(f,1,Index(p,f)) = f/.Index(p,f) by A5,
SPRECT_2:9;
Index(p,f)+1 <= len f by A4,NAT_1:13;
then
A8: LSeg(f,Index(p,f)) = LSeg(f/.Index(p,f), f/.(Index(p,f)+1)) by A6,
TOPREAL1:def 3;
A9: now
per cases by A1,SPPOL_1:19;
case
LSeg(f,Index(p,f)) is vertical;
hence p`1=(f/.Index(p,f))`1 by A3,A8,JORDAN5B:29,SPPOL_1:41;
end;
case
LSeg(f,Index(p,f)) is horizontal;
hence p`2=(f/.Index(p,f))`2 by A3,A8,JORDAN5B:29,SPPOL_1:40;
end;
end;
A10: <*p*>/.1 = p by FINSEQ_4:16;
A11: <*p*> is special;
per cases;
suppose
p <> f.1;
then R_Cut(f,p) = mid(f,1,Index(p,f))^<*p*> by JORDAN3:def 4;
hence thesis by A2,A10,A7,A9,GOBOARD2:8;
end;
suppose
p = f.1;
hence thesis by A11,JORDAN3:def 4;
end;
end;
theorem
for f be FinSequence of TOP-REAL 2 st f is special weakly-one-to-one
for p,q be Point of TOP-REAL 2 st p in L~f & q in L~f holds B_Cut(f,p,q) is
special
proof
let f be FinSequence of TOP-REAL 2;
assume
A1: f is special weakly-one-to-one;
let p,q be Point of TOP-REAL 2;
assume that
A2: p in L~f and
A3: q in L~f;
A4: Index(p,f) < len f by A2,JORDAN3:8;
A5: 1 <= Index(p,f) by A2,JORDAN3:8;
then
A6: Index(p,f) in dom f by A4,FINSEQ_3:25;
per cases;
suppose
A7: p <> q;
now
per cases;
suppose
A8: p in L~f & q in L~f & Index(p,f) < Index(q,f);
then
A9: q in L~L_Cut(f,p) by JORDAN3:29;
L_Cut(f,p) is special by A1,A2,Th29;
then R_Cut(L_Cut(f,p),q) is special by A9,Th30;
hence thesis by A8,JORDAN3:def 7;
end;
suppose
A10: Index(p,f)=Index(q,f) & LE p,q,f/.(Index(p,f)),f/.(Index(p,f) +1);
A11: L_Cut(f,p) is special by A1,A2,Th29;
q in L~L_Cut(f,p) by A2,A3,A7,A10,JORDAN3:31;
then R_Cut(L_Cut(f,p),q) is special by A11,Th30;
hence thesis by A10,JORDAN3:def 7;
end;
suppose
A12: not (p in L~f & q in L~f & Index(p,f) < Index(q,f) or Index(p
,f)=Index(q,f) & LE p,q,f/.(Index(p,f)),f/.(Index(p,f)+1));
A13: now
per cases by A2,A3,A12,XXREAL_0:1;
suppose
Index(q,f) < Index(p,f);
hence p in L~L_Cut(f,q) by A2,A3,JORDAN3:29;
end;
suppose
A14: Index(q,f) = Index(p,f);
A15: Index(p,f)+1 >= 1 by NAT_1:11;
Index(p,f)+1 <= len f by A4,NAT_1:13;
then
A16: Index(p,f)+1 in dom f by A15,FINSEQ_3:25;
set Ls = LSeg(f/.(Index(p,f)),f/.(Index(p,f)+1));
A17: q in Ls by A3,A14,JORDAN5B:29;
A18: p in Ls by A2,JORDAN5B:29;
f.Index(p,f) <> f.(Index(p,f)+1) by A1,A5,A4;
then f.Index(p,f) <> f/.(Index(p,f)+1) by A16,PARTFUN1:def 6;
then
A19: f/.Index(p,f) <> f/.(Index(p,f)+1) by A6,PARTFUN1:def 6;
then
A20: Ls is_an_arc_of f/.(Index(p,f)),f/.(Index(p,f)+1) by TOPREAL1:9;
not LE p,q,Ls,f/.(Index(p,f)),f/.(Index(p,f)+1) by A12,A14,A19,
JORDAN5C:17;
then LE q,p,Ls,f/.(Index(p,f)),f/.(Index(p,f)+1) by A7,A20,A18,A17,
JORDAN5C:14;
hence p in L~L_Cut(f,q) by A2,A3,A7,A14,A19,JORDAN3:31,JORDAN5C:17;
end;
end;
A21: B_Cut(f,p,q) = Rev (R_Cut(L_Cut(f,q),p)) by A12,JORDAN3:def 7;
L_Cut(f,q) is special by A1,A3,Th29;
then R_Cut(L_Cut(f,q),p) is special by A13,Th30;
hence thesis by A21,SPPOL_2:40;
end;
end;
hence thesis;
end;
suppose
p = q;
then B_Cut(f,p,q) = <*p*> by A1,A2,Th15;
hence thesis;
end;
end;
theorem Th32:
for f be FinSequence of TOP-REAL 2 st f is unfolded for p be
Point of TOP-REAL 2 st p in L~f holds L_Cut(f,p) is unfolded
proof
let f be FinSequence of TOP-REAL 2;
assume
A1: f is unfolded;
let p be Point of TOP-REAL 2;
A2: mid(f,Index(p,f)+1,len f) is unfolded by A1,Th28;
assume
A3: p in L~f;
then
A4: p in LSeg ( f/.Index(p,f), f/.(Index(p,f)+1) ) by JORDAN5B:29;
Index(p,f) < len f by A3,JORDAN3:8;
then
A5: Index(p,f)+1+0 <= len f by NAT_1:13;
len f <> 0 by A3,TOPREAL1:22;
then len f > 0 by NAT_1:3;
then
A6: len f >= 0+1 by NAT_1:13;
then
A7: len f in dom f by FINSEQ_3:25;
A8: 1 <= Index(p,f) by A3,JORDAN3:8;
then
A9: LSeg(f,Index(p,f)) = LSeg(f/.Index(p,f), f/.(Index(p,f)+1)) by A5,
TOPREAL1:def 3;
A10: 1<Index(p,f)+1 by A8,NAT_1:13;
then
A11: Index(p,f)+1 in dom f by A5,FINSEQ_3:25;
then
A12: mid(f,Index(p,f)+1,len f)/.1 = f/.(Index(p,f)+1) by A7,SPRECT_2:8;
per cases;
suppose
A13: Index(p,f)+1+1 <= len f;
then LSeg(f,Index(p,f)+1) = LSeg(f/.(Index(p,f)+1),f/.(Index(p,f)+(1+1)))
by A10,TOPREAL1:def 3;
then
A14: LSeg(f/.Index(p,f), f/.(Index(p,f)+1)) /\ LSeg(f/.(Index(p,f)+1),f/.(
Index(p,f)+(1+1))) = {f/.(Index(p,f)+1)} by A1,A8,A9,A13,TOPREAL1:def 6;
A15: len f -(Index(p,f)+1) >= 0 by A5,XREAL_1:19;
Index(p,f)+(1+1) <= len f by A13;
then
A16: 2 <= len f - Index(p,f) by XREAL_1:19;
A17: f/.(Index(p,f)+1) in LSeg(f/.(Index(p,f)+1),f/.(Index(p,f)+(1+1))) by
RLTOPSP1:68;
f/.(Index(p,f)+1) in LSeg(p,f/.(Index(p,f)+1)) by RLTOPSP1:68;
then
f/.(Index(p,f)+1) in LSeg(p,f/.(Index(p,f)+1)) /\ LSeg(f/.(Index(p,f)
+1),f/.(Index(p,f)+(1+1))) by A17,XBOOLE_0:def 4;
then
A18: {f/.(Index(p,f)+1)} c= LSeg(p,f/.(Index(p,f)+1)) /\ LSeg(f/.(Index(p,
f)+1),f/.(Index(p,f)+(1+1))) by ZFMISC_1:31;
2+(Index(p,f)+1)-1 = Index(p,f)+1+1;
then
A19: 2+(Index(p,f)+1)-1 >= 0 by NAT_1:2;
A20: len mid(f,Index(p,f)+1,len f) = len f-'(Index(p,f)+1)+1 by A6,A10,A5,
FINSEQ_6:118
.= len f -(Index(p,f)+1)+1 by A15,XREAL_0:def 2
.= len f - Index(p,f);
then 2 in dom mid(f,Index(p,f)+1,len f) by A16,FINSEQ_3:25;
then
(mid(f,Index(p,f)+1,len f))/.2 = f/.(2+(Index(p,f)+1)-'1) by A5,A11,A7,
SPRECT_2:3
.= f/.(Index(p,f)+(1+1)) by A19,XREAL_0:def 2;
then
A21: LSeg(mid(f,Index(p,f)+1,len f),1) = LSeg(f/.(Index(p,f)+1),f/.(Index(
p,f)+(1+1))) by A12,A20,A16,TOPREAL1:def 3;
f/.(Index(p,f)+1) in LSeg(f/.Index(p,f),f/.(Index(p,f)+1)) by RLTOPSP1:68;
then
LSeg(p,f/.(Index(p,f)+1)) /\ LSeg(f/.(Index(p,f)+1),f/.(Index(p,f)+(1
+1))) c= {f/.(Index(p,f)+1)} by A4,A14,TOPREAL1:6,XBOOLE_1:26;
then
A22: LSeg(p,f/.(Index(p,f)+1)) /\ LSeg(f/.(Index(p,f)+1),f/.(Index(p,f)+(1
+1))) = {f/.(Index(p,f)+1)} by A18;
now
per cases;
suppose
p <> f.(Index(p,f)+1);
then L_Cut(f,p) = <*p*>^mid(f,Index(p,f)+1,len f) by JORDAN3:def 3;
hence thesis by A1,A12,A21,A22,Th28,SPPOL_2:29;
end;
suppose
p = f.(Index(p,f)+1);
hence thesis by A2,JORDAN3:def 3;
end;
end;
hence thesis;
end;
suppose
A23: Index(p,f)+1+1 > len f;
A24: Index(p,f)+1 < len f or Index(p,f)+1 = len f by A5,XXREAL_0:1;
now
per cases;
suppose
p <> f.(Index(p,f)+1);
then L_Cut(f,p) = <*p*>^mid(f,len f,len f) by A23,A24,JORDAN3:def 3
,NAT_1:13
.= <*p*>^<*f.len f*> by A7,FINSEQ_6:193
.= <*p*>^<*f/.len f*> by A7,PARTFUN1:def 6
.= <*p,f/.len f*> by FINSEQ_1:def 9;
then len L_Cut(f,p) = 2 by FINSEQ_1:44;
hence thesis by SPPOL_2:26;
end;
suppose
p = f.(Index(p,f)+1);
then L_Cut(f,p) = mid(f,len f,len f) by A23,A24,JORDAN3:def 3,NAT_1:13
.= <*f.len f*> by A7,FINSEQ_6:193;
then len L_Cut(f,p) = 1 by FINSEQ_1:39;
hence thesis by SPPOL_2:26;
end;
end;
hence thesis;
end;
end;
theorem Th33:
for f be FinSequence of TOP-REAL 2 st f is unfolded for p be
Point of TOP-REAL 2 st p in L~f holds R_Cut(f,p) is unfolded
proof
let f be FinSequence of TOP-REAL 2;
assume
A1: f is unfolded;
let p be Point of TOP-REAL 2;
assume
A2: p in L~f;
then
A3: 1 <= Index(p,f) by JORDAN3:8;
len f <> 0 by A2,TOPREAL1:22;
then len f > 0 by NAT_1:3;
then
A4: len f >= 0+1 by NAT_1:13;
then 1 in Seg len f by FINSEQ_1:1;
then
A5: 1 in dom f by FINSEQ_1:def 3;
A6: Index(p,f) < len f by A2,JORDAN3:8;
then
A7: Index(p,f)+1+0 <= len f by NAT_1:13;
then
A8: LSeg(f,Index(p,f)) = LSeg(f/.Index(p,f), f/.(Index(p,f)+1)) by A3,
TOPREAL1:def 3;
Index(p,f) in Seg len f by A3,A6,FINSEQ_1:1;
then
A9: Index(p,f) in dom f by FINSEQ_1:def 3;
then
A10: mid(f,1,Index(p,f))/.len mid(f,1,Index(p,f)) = f/.Index(p,f) by A5,
SPRECT_2:9;
A11: p in LSeg ( f/.Index(p,f), f/.(Index(p,f)+1) ) by A2,JORDAN5B:29;
A12: Index(p,f)-'1+1 = Index(p,f) by A2,JORDAN3:8,XREAL_1:235;
per cases by A3,XXREAL_0:1;
suppose
A13: Index(p,f) > 0+1;
A14: f/.Index(p,f) in LSeg(f/.Index(p,f),f/.(Index(p,f)+1)) by RLTOPSP1:68;
A15: f/.Index(p,f) in LSeg(f/.Index(p,f),p) by RLTOPSP1:68;
f/.Index(p,f) in LSeg(f/.(Index(p,f)-'1),f/.Index(p,f)) by RLTOPSP1:68;
then f/.Index(p,f) in LSeg(f/.(Index(p,f)-'1),f/.Index(p,f)) /\ LSeg(f/.
Index(p,f),p) by A15,XBOOLE_0:def 4;
then
A16: {f/.Index(p,f)} c= LSeg(f/.(Index(p,f)-'1),f/.Index(p,f)) /\ LSeg(f/.
Index(p,f),p) by ZFMISC_1:31;
A17: Index(p,f)-'1+(1+1) <= len f by A7,A12;
Index(p,f)-1 > 0 by A13,XREAL_1:20;
then Index(p,f)-'1 > 0 by XREAL_0:def 2;
then
A18: Index(p,f)-'1 >= 0+1 by NAT_1:13;
then LSeg(f,Index(p,f)-'1) = LSeg(f/.(Index(p,f)-'1),f/.(Index(p,f)) ) by
A6,A12,TOPREAL1:def 3;
then LSeg(f/.(Index(p,f)-'1),f/.Index(p,f)) /\ LSeg(f/.Index(p,f),f/.(
Index(p,f)+1)) = {f/.Index(p,f)} by A1,A12,A8,A18,A17,TOPREAL1:def 6;
then
LSeg(f/.(Index(p,f)-'1),f/.Index(p,f)) /\ LSeg(f/.Index(p,f),p) c= {f
/.Index(p,f)} by A11,A14,TOPREAL1:6,XBOOLE_1:26;
then
A19: LSeg(f/.(Index(p,f)-'1),f/.Index(p,f)) /\ LSeg(f/.Index(p,f),p) = {f
/.Index(p,f)} by A16;
A20: len mid(f,1,Index(p,f)) = Index(p,f)-'1+1 by A4,A3,A6,FINSEQ_6:118
.= Index(p,f) by A2,JORDAN3:8,XREAL_1:235;
then
A21: len mid(f,1,Index(p,f))-'1+1 = len mid(f,1,Index(p,f)) by A2,JORDAN3:8
,XREAL_1:235;
len mid(f,1,Index(p,f))-'1 <= len mid(f,1,Index(p,f)) by NAT_D:35;
then
len mid(f,1,Index(p,f))-'1 in Seg len mid(f,1,Index(p,f)) by A18,A20,
FINSEQ_1:1;
then len mid(f,1,Index(p,f))-'1 in dom mid(f,1,Index(p,f)) by
FINSEQ_1:def 3;
then
A22: mid(f,1,Index(p,f))/.(len mid(f,1,Index(p,f))-'1) = f/.(len mid(f,1,
Index(p,f))-'1+1-'1) by A2,A9,A5,JORDAN3:8,SPRECT_2:3
.= f/.(len mid(f,1,Index(p,f))-'1) by NAT_D:34
.= f/.(Index(p,f)-'1+1-'1) by A3,A6,FINSEQ_6:186
.= f/.(Index(p,f)-'1) by A2,JORDAN3:8,XREAL_1:235;
len mid(f,1,Index(p,f))-'1+1=len mid(f,1,Index(p,f)) by A2,A20,JORDAN3:8
,XREAL_1:235;
then
A23: LSeg(mid(f,1,Index(p,f)),len mid(f,1,Index(p,f))-'1) = LSeg(f/.(Index
(p,f)-'1),f/.Index(p,f)) by A10,A18,A20,A22,TOPREAL1:def 3;
now
per cases;
suppose
p <> f.1;
then R_Cut(f,p) = mid(f,1,Index(p,f))^<*p*> by JORDAN3:def 4;
hence thesis by A1,A10,A23,A21,A19,Th28,SPPOL_2:30;
end;
suppose
p = f.1;
then R_Cut(f,p) = <*p*> by JORDAN3:def 4;
then len R_Cut(f,p) = 1 by FINSEQ_1:39;
hence thesis by SPPOL_2:26;
end;
end;
hence thesis;
end;
suppose
A24: Index(p,f) = 0+1;
now
per cases;
suppose
p <> f.1;
then R_Cut(f,p) = mid(f,1,1)^<*p*> by A24,JORDAN3:def 4
.= <*f.1 *>^<*p*> by A5,FINSEQ_6:193
.= <*f/.1 *>^<*p*> by A5,PARTFUN1:def 6
.= <*f/.1,p*> by FINSEQ_1:def 9;
then len R_Cut(f,p) = 2 by FINSEQ_1:44;
hence thesis by SPPOL_2:26;
end;
suppose
p = f.1;
then R_Cut(f,p) = <*p*> by JORDAN3:def 4;
then len R_Cut(f,p) = 1 by FINSEQ_1:39;
hence thesis by SPPOL_2:26;
end;
end;
hence thesis;
end;
end;
theorem
for f be FinSequence of TOP-REAL 2 st f is unfolded weakly-one-to-one
for p,q be Point of TOP-REAL 2 st p in L~f & q in L~f holds B_Cut(f,p,q) is
unfolded
proof
let f be FinSequence of TOP-REAL 2;
assume
A1: f is unfolded weakly-one-to-one;
let p,q be Point of TOP-REAL 2;
assume that
A2: p in L~f and
A3: q in L~f;
A4: Index(p,f) < len f by A2,JORDAN3:8;
A5: 1 <= Index(p,f) by A2,JORDAN3:8;
then Index(p,f) in Seg len f by A4,FINSEQ_1:1;
then
A6: Index(p,f) in dom f by FINSEQ_1:def 3;
per cases;
suppose
A7: p <> q;
now
per cases;
suppose
A8: p in L~f & q in L~f & Index(p,f) < Index(q,f);
then
A9: q in L~L_Cut(f,p) by JORDAN3:29;
L_Cut(f,p) is unfolded by A1,A2,Th32;
then R_Cut(L_Cut(f,p),q) is unfolded by A9,Th33;
hence thesis by A8,JORDAN3:def 7;
end;
suppose
A10: Index(p,f)=Index(q,f) & LE p,q,f/.(Index(p,f)),f/.(Index(p,f) +1);
A11: L_Cut(f,p) is unfolded by A1,A2,Th32;
q in L~L_Cut(f,p) by A2,A3,A7,A10,JORDAN3:31;
then R_Cut(L_Cut(f,p),q) is unfolded by A11,Th33;
hence thesis by A10,JORDAN3:def 7;
end;
suppose
A12: not (p in L~f & q in L~f & Index(p,f) < Index(q,f) or Index(p
,f)=Index(q,f) & LE p,q,f/.(Index(p,f)),f/.(Index(p,f)+1));
A13: now
per cases by A2,A3,A12,XXREAL_0:1;
suppose
Index(q,f) < Index(p,f);
hence p in L~L_Cut(f,q) by A2,A3,JORDAN3:29;
end;
suppose
A14: Index(q,f) = Index(p,f);
A15: Index(p,f)+1 >= 1 by NAT_1:11;
Index(p,f)+1 <= len f by A4,NAT_1:13;
then Index(p,f)+1 in Seg len f by A15,FINSEQ_1:1;
then
A16: Index(p,f)+1 in dom f by FINSEQ_1:def 3;
set Ls = LSeg(f/.(Index(p,f)),f/.(Index(p,f)+1));
A17: q in Ls by A3,A14,JORDAN5B:29;
A18: p in Ls by A2,JORDAN5B:29;
f.Index(p,f) <> f.(Index(p,f)+1) by A1,A5,A4;
then f.Index(p,f) <> f/.(Index(p,f)+1) by A16,PARTFUN1:def 6;
then
A19: f/.Index(p,f) <> f/.(Index(p,f)+1) by A6,PARTFUN1:def 6;
then
A20: Ls is_an_arc_of f/.(Index(p,f)),f/.(Index(p,f)+1) by TOPREAL1:9;
not LE p,q,Ls,f/.(Index(p,f)),f/.(Index(p,f)+1) by A12,A14,A19,
JORDAN5C:17;
then LE q,p,Ls,f/.(Index(p,f)),f/.(Index(p,f)+1) by A7,A20,A18,A17,
JORDAN5C:14;
hence p in L~L_Cut(f,q) by A2,A3,A7,A14,A19,JORDAN3:31,JORDAN5C:17;
end;
end;
A21: B_Cut(f,p,q) = Rev (R_Cut(L_Cut(f,q),p)) by A12,JORDAN3:def 7;
L_Cut(f,q) is unfolded by A1,A3,Th32;
then R_Cut(L_Cut(f,q),p) is unfolded by A13,Th33;
hence thesis by A21,SPPOL_2:28;
end;
end;
hence thesis;
end;
suppose
p = q;
then B_Cut(f,p,q) = <*p*> by A1,A2,Th15;
then len B_Cut(f,p,q) = 1 by FINSEQ_1:39;
hence thesis by SPPOL_2:26;
end;
end;
theorem Th35:
for f,g be FinSequence of TOP-REAL 2 for p be Point of TOP-REAL
2 st f is almost-one-to-one special unfolded s.n.c. & p in L~f & p<>f.1 & g=mid
(f,1,Index(p,f))^<*p*> holds g is_S-Seq_joining f/.1,p
proof
let f,g be FinSequence of TOP-REAL 2;
let p be Point of TOP-REAL 2;
assume that
A1: f is almost-one-to-one special unfolded s.n.c. and
A2: p in L~f and
A3: p<>f.1 and
A4: g=mid(f,1,Index(p,f))^<*p*>;
A5: Index(p,f)<len f by A2,JORDAN3:8;
A6: for j1,j2 be Nat st j1+1 < j2 holds LSeg(g,j1) misses LSeg(g,j2)
proof
let j1,j2 be Nat;
assume
A7: j1+1 < j2;
j1>=0 by NAT_1:2;
then
A8: j1=0 or j1>=0+1 by NAT_1:13;
now
per cases by A8,XXREAL_0:1;
case
j1=0;
then LSeg(g,j1)={} by TOPREAL1:def 3;
then LSeg(g,j1) /\ LSeg(g,j2) = {};
hence thesis;
end;
case that
A9: j1=1 or j1>1 and
A10: j2+1<=len g;
j2<len g by A10,NAT_1:13;
then j1+1<len g by A7,XXREAL_0:2;
then
A11: LSeg(g,j1) c= LSeg(f,j1) by A2,A4,A9,JORDAN3:18;
1+1<=j1+1 by A9,XREAL_1:6;
then 2<=j2 by A7,XXREAL_0:2;
then 1<=j2 by XXREAL_0:2;
then
A12: LSeg(g,j2) c= LSeg(f,j2) by A2,A4,A10,JORDAN3:18;
LSeg(f,j1) misses LSeg(f,j2) by A1,A7,TOPREAL1:def 7;
then LSeg(f,j1) /\ LSeg(f,j2) = {};
then LSeg(g,j1) /\ LSeg(g,j2) = {} by A11,A12,XBOOLE_1:3,27;
hence thesis;
end;
case
j2+1>len g;
then LSeg(g,j2)={} by TOPREAL1:def 3;
then LSeg(g,j1)/\ LSeg(g,j2)={};
hence thesis;
end;
end;
hence thesis;
end;
A13: len g = len mid(f,1,Index(p,f))+ len<*p*> by A4,FINSEQ_1:22
.= len mid(f,1,Index(p,f))+ 1 by FINSEQ_1:39;
consider i be Nat such that
1<=i and
A14: i+1<=len f and
p in LSeg(f,i) by A2,SPPOL_2:13;
A15: 1<=Index(p,f) by A2,JORDAN3:8;
1<=1+i by NAT_1:12;
then
A16: 1<=len f by A14,XXREAL_0:2;
then
A17: len mid(f,1,Index(p,f))=Index(p,f)-'1+1 by A15,A5,FINSEQ_6:118;
then
A18: len mid(f,1,Index(p,f))=Index(p,f) by A2,JORDAN3:8,XREAL_1:235;
then g.1 = mid(f,1,Index(p,f)).1 by A4,A15,FINSEQ_6:109;
then g.1=f.1 by A15,A5,A16,FINSEQ_6:118;
then
A19: g.1=f/.1 by A16,FINSEQ_4:15;
A20: for j be Nat st 1 <= j & j + 2 <= len g holds LSeg(g,j) /\ LSeg(g,j+1)
= {g/.(j+1)}
proof
let j be Nat;
assume that
A21: 1 <= j and
A22: j + 2 <= len g;
A23: j+1<=len g by A22,NAT_D:47;
then LSeg(g,j)=LSeg(g/.j,g/.(j+1)) by A21,TOPREAL1:def 3;
then
A24: g/.(j+1) in LSeg(g,j) by RLTOPSP1:68;
A25: 1<=j+1 by A21,NAT_D:48;
then LSeg(g,j+1)=LSeg(g/.(j+1),g/.(j+1+1)) by A22,TOPREAL1:def 3;
then g/.(j+1) in LSeg(g,j+1) by RLTOPSP1:68;
then g/.(j+1) in LSeg(g,j) /\ LSeg(g,j+1) by A24,XBOOLE_0:def 4;
then
A26: {g/.(j+1)} c= LSeg(g,j) /\ LSeg(g,j+1) by ZFMISC_1:31;
j+1<=len g by A22,NAT_D:47;
then
A27: LSeg(g,j) c= LSeg(f,j) by A2,A4,A21,JORDAN3:18;
A28: Index(p,f)<=len f by A2,JORDAN3:8;
A29: j+1+1<=len g by A22;
then LSeg(g,j+1) c= LSeg(f,j+1) by A2,A4,A25,JORDAN3:18;
then
A30: LSeg(g,j)/\ LSeg(g,j+1) c= LSeg(f,j)/\ LSeg(f,j+1) by A27,XBOOLE_1:27;
A31: g/.(j+1)=g.(j+1) by A25,A23,FINSEQ_4:15;
now
A32: len g=len mid(f,1,Index(p,f))+1 by A4,FINSEQ_2:16;
Index(p,f)<=len f by A2,JORDAN3:8;
then
A33: len g<=len f +1 by A18,A32,XREAL_1:6;
now
per cases by A33,XXREAL_0:1;
case
len g = len f +1;
hence contradiction by A2,A18,A32,JORDAN3:8;
end;
case
len g<len f+1;
then len g<=len f by NAT_1:13;
then j+2<=len f by A22,XXREAL_0:2;
then
A34: LSeg(g,j)/\ LSeg(g,j+1) c= {f/.(j+1)} by A1,A21,A30,TOPREAL1:def 6;
A35: j+1<=Index(p,f) by A18,A29,A32,XREAL_1:6;
then j+1<=len f by A28,XXREAL_0:2;
then
A36: f.(j+1)=f/.(j+1) by A25,FINSEQ_4:15;
g.(j+1) = mid(f,1,Index(p,f)).(j+1) by A4,A18,A25,A35,FINSEQ_1:64
.= f.(j+1) by A5,A25,A35,FINSEQ_6:123;
hence thesis by A31,A26,A34,A36;
end;
end;
hence thesis;
end;
hence thesis;
end;
for j be Nat st 1 <= j & j+1 <= len g holds (g/.j)`1 = (g/.(j+1))`1 or
(g/.j)`2 = (g/.(j+1))`2
proof
A37: Index(p,f)<len f by A2,JORDAN3:8;
let j be Nat;
assume that
A38: 1 <= j and
A39: j+1 <= len g;
A40: LSeg(g,j) = LSeg(g/.j,g/.(j+1)) by A38,A39,TOPREAL1:def 3;
j+1 <= Index(p,f)+1 by A4,A18,A39,FINSEQ_2:16;
then j<=Index(p,f) by XREAL_1:6;
then j<len f by A37,XXREAL_0:2;
then
A41: j+1<=len f by NAT_1:13;
then
A42: LSeg(f,j) = LSeg(f/.j,f/.(j+1)) by A38,TOPREAL1:def 3;
A43: (f/.j)`1 = (f/.(j+1))`1 or (f/.j)`2 = (f/.(j+1))`2 by A1,A38,A41,
TOPREAL1:def 5;
LSeg(g,j) c= LSeg(f,j) by A2,A4,A38,A39,JORDAN3:18;
hence thesis by A40,A42,A43,JORDAN3:3;
end;
then
A44: g is unfolded s.n.c. special by A20,A6,TOPREAL1:def 5,def 6,def 7;
1<=len <*p*> by FINSEQ_1:39;
then
A45: 1 in dom <*p*> by FINSEQ_3:25;
for x1,x2 being object st x1 in dom g & x2 in dom g & g.x1=g.x2 holds x1= x2
proof
let x1,x2 be object;
assume that
A46: x1 in dom g and
A47: x2 in dom g and
A48: g.x1=g.x2;
reconsider n1=x1,n2=x2 as Nat by A46,A47;
A49: 1<=n1 by A46,FINSEQ_3:25;
A50: n2<=len g by A47,FINSEQ_3:25;
A51: 1<=n2 by A47,FINSEQ_3:25;
A52: n1<=len g by A46,FINSEQ_3:25;
now
A53: g.len g = <*p*>.1 by A4,A45,A13,FINSEQ_1:def 7
.= p;
now
per cases;
case
A54: n1=len g;
now
assume
A55: n2<>len g;
then n2<len g by A50,XXREAL_0:1;
then
A56: n2<=len mid(f,1,Index(p,f)) by A13,NAT_1:13;
then
A57: n2 < len f by A5,A18,XXREAL_0:2;
g.n2=mid(f,1,Index(p,f)).n2 by A4,A51,A56,FINSEQ_1:64;
then g.n2=f.(n2+1-'1) by A15,A5,A16,A51,A56,FINSEQ_6:118;
then
A58: p=f.n2 by A48,A53,A54,NAT_D:34;
then 1 < n2 by A3,A51,XXREAL_0:1;
then Index(p,f)+1 = n2 by A1,A58,A57,Th18;
hence contradiction by A2,A17,A13,A55,JORDAN3:8,XREAL_1:235;
end;
hence thesis by A54;
end;
case
A59: n2=len g;
now
assume
A60: n1<>len g;
then n1<len g by A52,XXREAL_0:1;
then
A61: n1<=len mid(f,1,Index(p,f)) by A13,NAT_1:13;
then
A62: n1 < len f by A5,A18,XXREAL_0:2;
g.n1=mid(f,1,Index(p,f)).n1 by A4,A49,A61,FINSEQ_1:64;
then g.n1=f.(n1+1-'1) by A15,A5,A16,A49,A61,FINSEQ_6:118;
then
A63: p=f.n1 by A48,A53,A59,NAT_D:34;
then 1 < n1 by A3,A49,XXREAL_0:1;
then Index(p,f)+1 = n1 by A1,A63,A62,Th18;
hence contradiction by A2,A17,A13,A60,JORDAN3:8,XREAL_1:235;
end;
hence thesis by A59;
end;
case that
A64: n1 <> len g and
A65: n2 <> len g;
n2 < len g by A50,A65,XXREAL_0:1;
then
A66: n2<=len mid(f,1,Index(p,f)) by A13,NAT_1:13;
then
A67: g.n2 = mid(f,1,Index(p,f)).n2 by A4,A51,FINSEQ_1:64
.= f.n2 by A5,A18,A51,A66,FINSEQ_6:123;
n2<len f by A5,A18,A66,XXREAL_0:2;
then n2 in Seg len f by A51,FINSEQ_1:1;
then
A68: n2 in dom f by FINSEQ_1:def 3;
n1 < len g by A52,A64,XXREAL_0:1;
then
A69: n1<=len mid(f,1,Index(p,f)) by A13,NAT_1:13;
then n1<len f by A5,A18,XXREAL_0:2;
then n1 in Seg len f by A49,FINSEQ_1:1;
then
A70: n1 in dom f by FINSEQ_1:def 3;
g.n1=mid(f,1,Index(p,f)).n1 by A4,A49,A69,FINSEQ_1:64
.=f.n1 by A5,A18,A49,A69,FINSEQ_6:123;
hence thesis by A1,A5,A18,A48,A69,A66,A67,A70,A68;
end;
end;
hence thesis;
end;
hence thesis;
end;
then
A71: g is one-to-one;
1+1<=len g by A15,A18,A13,XREAL_1:6;
then
A72: g is being_S-Seq by A71,A44,TOPREAL1:def 8;
g.len g = p by A4,A13,FINSEQ_1:42;
hence thesis by A19,A72,JORDAN3:def 2;
end;
theorem Th36:
for f be FinSequence of TOP-REAL 2 for p be Point of TOP-REAL 2
st f is poorly-one-to-one unfolded s.n.c. & p in L~f & p = f.(Index(p,f)+1) & p
<> f.len f holds Index(p,Rev f) + Index(p,f) + 1 = len f
proof
let f be FinSequence of TOP-REAL 2;
let p be Point of TOP-REAL 2 such that
A1: f is poorly-one-to-one unfolded s.n.c. and
A2: p in L~f and
A3: p = f.(Index(p,f)+1) and
A4: p <> f.len f;
A5: Rev f is s.n.c. by A1,SPPOL_2:35;
A6: len f = len Rev f by FINSEQ_5:def 3;
len f <= len f + Index(p,f) by NAT_1:11;
then
A7: len f - Index(p,f) <= len Rev f by A6,XREAL_1:20;
Index(p,f) <= len f by A2,JORDAN3:8;
then
A8: len f - Index(p,f) = len f -' Index(p,f) by XREAL_1:233;
Index(p,f) < len f by A2,JORDAN3:8;
then
A9: Index(p,f)+1 <= len f by NAT_1:13;
then Index(p,f)+1 < len f by A3,A4,XXREAL_0:1;
then
A10: 1 < len f - Index(p,f) by XREAL_1:20;
1 <= Index(p,f)+1 by NAT_1:11;
then Index(p,f)+1 in dom f by A9,FINSEQ_3:25;
then
A11: Index(p,f)+1 in dom Rev f by FINSEQ_5:57;
p = (Rev Rev f).(Index(p,f)+1) by A3
.= (Rev f).(len Rev f - (Index(p,f)+1) + 1) by A11,FINSEQ_5:58
.= (Rev f).(len Rev f - Index(p,f))
.= (Rev f).(len f - Index(p,f)) by FINSEQ_5:def 3;
then Index(p,Rev f) + 1 = len f -' Index(p,f) by A1,A5,A7,A10,A8,Th18,
SPPOL_2:28;
hence thesis by A8;
end;
theorem
for f be non empty FinSequence of TOP-REAL 2 for p be Point of
TOP-REAL 2 st f is weakly-one-to-one & len f >= 2 holds L_Cut (f,f/.1) = f
proof
let f be non empty FinSequence of TOP-REAL 2;
let p be Point of TOP-REAL 2;
assume that
A1: f is weakly-one-to-one and
A2: len f >= 2;
A3: Index(f/.1,f) = 1 by A2,JORDAN3:11;
1 <= len f by A2,XXREAL_0:2;
then
A4: 1 in dom f by FINSEQ_3:25;
then
A5: f/.1 = f.1 by PARTFUN1:def 6;
2 = 1+1;
then
A6: 1 < len f by A2,NAT_1:13;
then f.1 <> f.(1+1) by A1;
then f/.1 <> f.(1+1) by A4,PARTFUN1:def 6;
hence L_Cut (f,f/.1) = <*f/.1 *>^mid(f,Index(f/.1,f)+1,len f) by A3,
JORDAN3:def 3
.= mid(f,1,len f) by A4,A6,A5,A3,FINSEQ_6:126
.= f by A2,FINSEQ_6:120,XXREAL_0:2;
end;
theorem Th38:
for f be non empty FinSequence of TOP-REAL 2 for p be Point of
TOP-REAL 2 st f is poorly-one-to-one unfolded s.n.c. & p in L~f & p <> f.len f
holds L_Cut(Rev f,p) = Rev R_Cut(f,p)
proof
let f be non empty FinSequence of TOP-REAL 2;
let p be Point of TOP-REAL 2 such that
A1: f is poorly-one-to-one unfolded s.n.c. and
A2: p in L~f and
A3: p <> f.len f;
A4: Index(p,f) < len f by A2,JORDAN3:8;
A5: p in L~Rev f by A2,SPPOL_2:22;
A6: Rev f is s.n.c. by A1,SPPOL_2:35;
A7: dom Rev f = dom f by FINSEQ_5:57;
A8: len f = len Rev f by FINSEQ_5:def 3;
A9: 1 <= Index(p,f) by A2,JORDAN3:8;
then
A10: 1 < len f by A4,XXREAL_0:2;
L~f = L~Rev f by SPPOL_2:22;
then Index(p, Rev f) < len Rev f by A2,JORDAN3:8;
then
A11: Index(p, Rev f) + 1 <= len f by A8,NAT_1:13;
1 <= Index(p, Rev f)+1 by NAT_1:11;
then
A12: Index(p, Rev f)+1 in dom f by A11,FINSEQ_3:25;
per cases by A3;
suppose
A13: p = f.1;
A14: len Rev f-'1+1=len Rev f by A8,A9,A4,XREAL_1:235,XXREAL_0:2;
then
A15: (Rev f/^(len Rev f-'1)).1=Rev f.len Rev f by FINSEQ_6:114;
A16: len (Rev f/^(len Rev f-'1))=len Rev f-'(len Rev f-'1) by RFINSEQ:29;
A17: 1<=len Rev f-(len Rev f-'1) by A14;
A19: Rev f/^(len Rev f-'1) is non empty by A16,A17,NAT_D:39;
len Rev f-'len Rev f+1=len Rev f-len Rev f+1 by XREAL_1:233
.=1;
then
A20: mid(Rev f,len Rev f,len Rev f)=(Rev f/^(len Rev f-'1))|1 by FINSEQ_6:def 3
.=<*(Rev f/^(len Rev f-'1)).1 *> by A19,FINSEQ_5:20
.=<*Rev f.len Rev f*> by A15;
A21: p = (Rev f).len f by A13,FINSEQ_5:62;
then Index(p,Rev f) + 1 = len f by A1,A6,A8,A10,Th18,SPPOL_2:28;
hence L_Cut(Rev f,p) = <*p*> by A8,A21,A20,JORDAN3:def 3
.= Rev <*p*> by FINSEQ_5:60
.= Rev R_Cut(f,p) by A13,JORDAN3:def 4;
end;
suppose that
A22: p <> f.1 and
A23: p <> f.len f and
A24: p = f.(Index(p,f)+1);
A25: len f = Index(p,Rev f) + Index(p,f) + 1 by A1,A2,A23,A24,Th36
.= Index(p,f) + (Index(p,Rev f) + 1);
len f = Index(p,Rev f) + Index(p,f) + 1 by A1,A2,A23,A24,Th36
.= Index(p,Rev f) + (Index(p,f) + 1);
then
A26: p = f.(len f - (Index(p, Rev f)+1) + 1) by A24
.= (Rev f).(Index(p, Rev f)+1) by A12,FINSEQ_5:58;
A27: len f -' Index(p,f) = len f - Index(p,f) by A4,XREAL_1:233
.= Index(p,Rev f)+1 by A25;
p <> (Rev f).len f by A22,FINSEQ_5:62;
then
A28: Index(p, Rev f)+1 < len f by A11,A26,XXREAL_0:1;
thus L_Cut(Rev f,p) = mid(Rev f,Index(p,Rev f)+1,len f) by A8,A26,
JORDAN3:def 3
.= <*p*>^mid(Rev f,len f -' Index(p,f)+1, len f) by A7,A12,A26,A27,A28,
FINSEQ_6:126
.= <*p*>^mid(Rev f,len f -' Index(p,f)+1, len f-'1+1) by A9,A4,
XREAL_1:235,XXREAL_0:2
.= <*p*>^Rev mid(f,1,Index(p,f)) by A9,A4,A10,FINSEQ_6:113
.= Rev (mid(f,1,Index(p,f))^<*p*>) by FINSEQ_5:63
.= Rev R_Cut(f,p) by A22,JORDAN3:def 4;
end;
suppose that
A29: p <> f.1 and
A30: p <> f.(Index(p,f)+1);
A31: p <> (Rev f).len f by A29,FINSEQ_5:62;
A32: now
assume
A33: p = (Rev f).(Index(p, Rev f)+1);
then
A34: len Rev f = Index(p,Rev Rev f) + Index(p,Rev f) + 1 by A1,A6,A5,A8,A31
,Th36,SPPOL_2:28
.= Index(p,f) + 1 + Index(p,Rev f);
p = f.(len f - (Index(p, Rev f)+1) + 1) by A12,A33,FINSEQ_5:58
.= f.(Index(p,f)+1) by A8,A34;
hence contradiction by A30;
end;
A35: Index(p, f) < len f by A2,JORDAN3:8;
len f = Index(p,Rev f) + Index(p,f) by A1,A2,A30,JORDAN3:21;
then Index(p,Rev f) = len f - Index(p,f)
.= len f -' Index(p,f) by A35,XREAL_1:233;
hence
L_Cut(Rev f,p) = <*p*>^mid(Rev f,len f -' Index(p,f)+1, len f) by A8,A32,
JORDAN3:def 3
.= <*p*>^mid(Rev f,len f -' Index(p,f)+1, len f-'1+1) by A9,A4,
XREAL_1:235,XXREAL_0:2
.= <*p*>^Rev mid(f,1,Index(p,f)) by A9,A4,A10,FINSEQ_6:113
.= Rev (mid(f,1,Index(p,f))^<*p*>) by FINSEQ_5:63
.= Rev R_Cut(f,p) by A29,JORDAN3:def 4;
end;
end;
theorem Th39:
for f be FinSequence of TOP-REAL 2 for p be Point of TOP-REAL 2
st f is almost-one-to-one special unfolded s.n.c. & p in L~f & p<>f.1 holds
R_Cut(f,p) is_S-Seq_joining f/.1,p
proof
let f be FinSequence of TOP-REAL 2;
let p be Point of TOP-REAL 2;
assume that
A1: f is almost-one-to-one special unfolded s.n.c. and
A2: p in L~f and
A3: p<>f.1;
R_Cut(f,p)=mid(f,1,Index(p,f))^<*p*> by A3,JORDAN3:def 4;
hence thesis by A1,A2,A3,Th35;
end;
theorem Th40:
for f be non empty FinSequence of TOP-REAL 2 for p be Point of
TOP-REAL 2 st f is almost-one-to-one special unfolded s.n.c. & p in L~f & p<>f.
len f & p <> f.1 holds L_Cut(f,p) is_S-Seq_joining p,f/.len f
proof
let f be non empty FinSequence of TOP-REAL 2;
let p be Point of TOP-REAL 2;
assume that
A1: f is almost-one-to-one special unfolded s.n.c. and
A2: p in L~f and
A3: p<>f.len f and
A4: p <> f.1;
A5: Rev f is special by A1,SPPOL_2:40;
A6: p in L~Rev f by A2,SPPOL_2:22;
p <> Rev f.len f by A4,FINSEQ_5:62;
then
A7: p <> Rev f.len Rev f by FINSEQ_5:def 3;
A8: Rev f is s.n.c. by A1,SPPOL_2:35;
A9: p <> (Rev f).1 by A3,FINSEQ_5:62;
A10: Rev f is unfolded by A1,SPPOL_2:28;
L_Cut(f,p) = L_Cut(Rev Rev f,p)
.= Rev R_Cut(Rev f,p) by A1,A7,A10,A8,A6,Th38;
then L_Cut(f,p) is_S-Seq_joining p,(Rev f)/.1 by A1,A5,A10,A8,A6,A9,Th39,
JORDAN3:15;
hence thesis by FINSEQ_5:65;
end;
theorem
for f be FinSequence of TOP-REAL 2 for p be Point of TOP-REAL 2 st f
is almost-one-to-one special unfolded s.n.c. & p in L~f & p<>f.1 holds R_Cut(f,
p) is being_S-Seq
proof
let f be FinSequence of TOP-REAL 2;
let p be Point of TOP-REAL 2;
assume that
A1: f is almost-one-to-one special unfolded s.n.c. and
A2: p in L~f and
A3: p<>f.1;
R_Cut(f,p) is_S-Seq_joining f/.1,p by A1,A2,A3,Th39;
hence thesis by JORDAN3:def 2;
end;
theorem Th42:
for f be non empty FinSequence of TOP-REAL 2 for p be Point of
TOP-REAL 2 st f is almost-one-to-one special unfolded s.n.c. & p in L~f & p <>
f.len f & p <> f.1 holds L_Cut(f,p) is being_S-Seq
proof
let f be non empty FinSequence of TOP-REAL 2;
let p be Point of TOP-REAL 2;
assume that
A1: f is almost-one-to-one special unfolded s.n.c. and
A2: p in L~f and
A3: p <> f.len f and
A4: p <> f.1;
L_Cut(f,p) is_S-Seq_joining p,f/.len f by A1,A2,A3,A4,Th40;
hence thesis by JORDAN3:def 2;
end;
Lm1: for f be non empty FinSequence of TOP-REAL 2 for p,q be Point of TOP-REAL
2 st f is almost-one-to-one special unfolded s.n.c. & p in L~f & q in L~f & p<>
q & p <> f.1 & (Index(p,f)<Index(q,f) or Index(p,f)=Index(q,f) & LE p,q,f/.(
Index(p,f)),f/.(Index(p,f)+1)) holds B_Cut(f,p,q) is_S-Seq_joining p,q
proof
let f be non empty FinSequence of TOP-REAL 2;
let p,q be Point of TOP-REAL 2;
assume that
A1: f is almost-one-to-one special unfolded s.n.c. and
A2: p in L~f and
A3: q in L~f and
A4: p <> q;
assume
A5: p <> f.1;
A6: Index(q,f)<len f by A3,JORDAN3:8;
Index(p,f) < len f by A2,JORDAN3:8;
then
A7: Index(p,f)+1 <= len f by NAT_1:13;
assume
A8: Index(p,f)<Index(q,f) or Index(p,f)=Index(q,f) & LE p,q,f/.(Index(p,
f)),f/.(Index(p,f)+1);
then
A9: B_Cut(f,p,q)=R_Cut(L_Cut(f,p),q) by A2,A3,JORDAN3:def 7;
1<=Index(q,f) by A3,JORDAN3:8;
then
A10: 1<len f by A6,XXREAL_0:2;
A11: now
per cases by A8;
case
A12: Index(p,f)<Index(q,f);
assume
A13: p=f.len f;
Index(p,f)+1<=Index(q,f) by A12,NAT_1:13;
then len f <= Index(q,f) by A1,A10,A13,Th18;
hence contradiction by A3,JORDAN3:8;
end;
case
A14: Index(p,f)=Index(q,f) & LE p,q,f/.(Index(p,f)),f/.(Index(p,f)+1 );
A15: now
q in LSeg(f/.(Index(p,f)),f/.(Index(p,f)+1)) by A14,JORDAN3:def 5;
then consider r being Real such that
A16: q = (1-r)*f/.(Index(p,f))+r*f/.(Index(p,f)+1) and
A17: 0 <= r and
A18: r <= 1;
A19: p = 1 * p by RLVECT_1:def 8
.= 0.TOP-REAL 2 + 1 * p by RLVECT_1:4
.= (1-1)*f/.(Index(p,f))+1 * p by RLVECT_1:10;
assume
A20: p = f.(Index(p,f)+1);
then p = f/.(Index(p,f)+1) by A7,FINSEQ_4:15,NAT_1:11;
then 1<=r by A14,A16,A17,A19,JORDAN3:def 5;
then r = 1 by A18,XXREAL_0:1;
hence contradiction by A4,A7,A20,A16,A19,FINSEQ_4:15,NAT_1:11;
end;
assume p=f.len f;
hence contradiction by A1,A10,A15,Th18;
end;
end;
then L_Cut(f,p) is_S-Seq_joining p,f/.len f by A1,A2,A5,Th40;
then
A21: (L_Cut(f,p)).1=p by JORDAN3:def 2;
now
per cases by A8;
case
Index(p,f)<Index(q,f);
then q in L~(L_Cut(f,p)) by A2,A3,JORDAN3:29;
hence ex i1 being Nat st 1<=i1 & i1+1<=len L_Cut(f,p) & q in
LSeg(L_Cut(f,p),i1) by SPPOL_2:13;
end;
case
Index(p,f)=Index(q,f) & LE p,q,f/.(Index(p,f)),f/.(Index(p,f)+1 );
then q in L~(L_Cut(f,p)) by A2,A3,A4,JORDAN3:31;
hence ex i1 being Nat st 1<=i1 & i1+1<=len L_Cut(f,p) & q in
LSeg(L_Cut(f,p),i1) by SPPOL_2:13;
end;
end;
then
A22: q in L~L_Cut(f,p) by SPPOL_2:17;
then
A23: Index(q,L_Cut(f,p))<len L_Cut(f,p) by JORDAN3:8;
1<=Index(q,L_Cut(f,p)) by A22,JORDAN3:8;
then 1<=len L_Cut(f,p) by A23,XXREAL_0:2;
then p=(L_Cut(f,p))/. 1 by A21,FINSEQ_4:15;
hence thesis by A1,A2,A4,A5,A9,A11,A22,A21,Th42,JORDAN3:32;
end;
theorem Th43:
for f be non empty FinSequence of TOP-REAL 2 for p,q be Point of
TOP-REAL 2 st f is almost-one-to-one special unfolded s.n.c. & len f <> 2 & p
in L~f & q in L~f & p<>q & p <> f.1 & q <> f.1 holds B_Cut(f,p,q)
is_S-Seq_joining p,q
proof
let f be non empty FinSequence of TOP-REAL 2;
let p,q be Point of TOP-REAL 2;
assume that
A1: f is almost-one-to-one special unfolded s.n.c. and
A2: len f <> 2 and
A3: p in L~f and
A4: q in L~f and
A5: p<>q and
A6: p <> f.1 and
A7: q <> f.1;
per cases;
suppose
Index(p,f)<Index(q,f) or Index(p,f)=Index(q,f) & LE p,q,f/.(Index(
p,f)),f/.(Index(p,f)+1);
hence thesis by A1,A3,A4,A5,A6,Lm1;
end;
suppose
A8: not(Index(p,f)<Index(q,f) or Index(p,f)=Index(q,f) & LE p,q,f/.(
Index(p,f)),f/.(Index(p,f)+1));
A9: now
assume that
A10: Index(p,f)=Index(q,f) and
A11: not LE p,q,f/.(Index(p,f)),f/.(Index(p,f)+1);
A12: Index(p,f) < len f by A3,JORDAN3:8;
A13: 1 <= Index(p,f) by A3,JORDAN3:8;
then
A14: Index(p,f) in dom f by A12,FINSEQ_3:25;
f is weakly-one-to-one by A1,A2,Th7;
then f.Index(p,f) <> f.(Index(p,f)+1) by A13,A12;
then
A15: f/.(Index(p,f))<>f.(Index(p,f)+1) by A14,PARTFUN1:def 6;
A16: Index(p,f)+1 <= len f by A12,NAT_1:13;
then
A17: LSeg(f,Index(p,f)) = LSeg(f/.(Index(p,f)),f/.(Index(p,f)+1)) by A13,
TOPREAL1:def 3;
then
A18: p in LSeg(f/.(Index(p,f)),f/.(Index(p,f)+1)) by A3,JORDAN3:9;
1 <= Index(p,f)+1 by NAT_1:11;
then Index(p,f)+1 in dom f by A16,FINSEQ_3:25;
then
A19: f/.(Index(p,f))<>f/.(Index(p,f)+1) by A15,PARTFUN1:def 6;
q in LSeg(f/.(Index(p,f)),f/.(Index(p,f)+1)) by A4,A10,A17,JORDAN3:9;
then LT q,p,f/.(Index(p,f)),f/.(Index(p,f)+1) by A11,A18,A19,JORDAN3:28;
hence LE q,p,f/.Index(q,f),f/.(Index(q,f)+1) by A10,JORDAN3:def 6;
end;
A20: Index(q,f) < Index(p,f) or Index(p,f)=Index(q,f) & not LE p,q,f/.(
Index(p,f)),f/.(Index(p,f)+1) by A8,XXREAL_0:1;
B_Cut(f,p,q)=Rev R_Cut(L_Cut(f,q),p) by A8,JORDAN3:def 7;
then
A21: Rev B_Cut(f,q,p) = B_Cut(f,p,q) by A3,A4,A20,A9,JORDAN3:def 7;
B_Cut(f,q,p) is_S-Seq_joining q,p by A1,A3,A4,A5,A7,A20,A9,Lm1;
hence thesis by A21,JORDAN3:15;
end;
end;
theorem
for f be non empty FinSequence of TOP-REAL 2 for p,q be Point of
TOP-REAL 2 st f is almost-one-to-one special unfolded s.n.c. & len f <> 2 & p
in L~f & q in L~f & p<>q & p <> f.1 & q <> f.1 holds B_Cut(f,p,q) is
being_S-Seq
proof
let f be non empty FinSequence of TOP-REAL 2;
let p,q be Point of TOP-REAL 2;
assume that
A1: f is almost-one-to-one special unfolded s.n.c. and
A2: len f <> 2 and
A3: p in L~f and
A4: q in L~f and
A5: p<>q and
A6: p <> f.1 and
A7: q <> f.1;
B_Cut(f,p,q) is_S-Seq_joining p,q by A1,A2,A3,A4,A5,A6,A7,Th43;
hence thesis by JORDAN3:def 2;
end;
theorem
for C be compact non vertical non horizontal Subset of TOP-REAL 2 for
p,q be Point of TOP-REAL 2 st p in BDD L~Cage(C,n) ex B be S-Sequence_in_R2 st
B = B_Cut(Rotate(Cage(C,n),Cage(C,n)/.Index(South-Bound(p,L~Cage(C,n)), Cage(C,
n)))|(len Rotate(Cage(C,n),Cage(C,n)/. Index(South-Bound(p,L~Cage(C,n)), Cage(C
,n)))-'1),South-Bound(p,L~Cage(C,n)),North-Bound(p,L~Cage(C,n))) & ex P be
S-Sequence_in_R2 st P is_sequence_on GoB(B^'<*North-Bound(p,L~Cage(C,n)),
South-Bound(p,L~Cage(C,n))*>) & L~<*North-Bound(p,L~Cage(C,n)),South-Bound(p,L~
Cage(C,n))*> = L~P & P/.1 = North-Bound(p,L~Cage(C,n)) & P/.len P = South-Bound
(p,L~Cage(C,n)) & len P >= 2 & ex B1 be S-Sequence_in_R2 st B1 is_sequence_on
GoB(B^'<*North-Bound(p,L~Cage(C,n)),South-Bound(p,L~Cage(C,n))*>) & L~B = L~B1
& B/.1 = B1/.1 & B/.len B = B1/.len B1 & len B <= len B1 & ex g be non constant
standard special_circular_sequence st g = B1^'P
proof
let C be compact non vertical non horizontal Subset of TOP-REAL 2;
let p,q be Point of TOP-REAL 2;
set f = Cage(C,n);
set Lf = L~f;
set a = North-Bound(p,Lf);
set b = South-Bound(p,Lf);
set Rotf = Rotate(f,f/.Index(b,f));
set rf = Rotf|(len Rotf-'1);
A1: L~Rotf = L~f by REVROT_1:33;
A2: LSeg(Rotf,len Rotf -' 1) /\ LSeg(Rotf,1) = {Rotf/.1} by GOBOARD7:34
,REVROT_1:30;
then
A3: LSeg(Rotf,len Rotf -' 1) meets LSeg(Rotf,1);
A4: Rotf/.2 in LSeg(Rotf/.2,Rotf/.1) by RLTOPSP1:68;
len Rotf >=1+1 by GOBOARD7:34,XXREAL_0:2;
then
A5: LSeg(Rotf,1) = LSeg(Rotf/.1,Rotf/.(1+1)) by TOPREAL1:def 3;
A6: b`1 = p`1 by JORDAN18:16;
len f > 4 by GOBOARD7:34;
then
A7: len f-'1+1 = len f by XREAL_1:235,XXREAL_0:2;
then
A8: len f-'1 < len f by NAT_1:13;
set pion = <*a,b*>;
A9: len f > 1 by GOBOARD7:34,XXREAL_0:2;
A10: Rotf/.(len Rotf-'1) in LSeg(Rotf/.(len Rotf-'1),Rotf/.(len Rotf)) by
RLTOPSP1:68;
assume that
A11: p in BDD Lf;
A12: a <> b by A11,JORDAN18:20;
A13: b in Lf by A11,JORDAN18:17;
then
A14: Index(b,f) < len f by JORDAN3:8;
A15: for i be Nat st 1 <= i & i < Index(b,f) holds f/.i <> f/.Index(b,f)
by A14,GOBOARD7:36;
1<=Index(b,f) by A13,JORDAN3:8;
then
A16: Index(b,f) in dom f by A14,FINSEQ_3:25;
then f/.Index(b,f)..f <= Index(b,f) by FINSEQ_5:39;
then 0+(f/.Index(b,f))..f < len f by A14,XXREAL_0:2;
then
A17: len f - (f/.Index(b,f))..f > 1-1 by XREAL_1:20;
A18: f/.Index(b,f) in rng f by A16,PARTFUN2:2;
then len(f:-(f/.Index(b,f)))=len f-(f/.Index(b,f))..f+1 by FINSEQ_5:50;
then 1 < len(f:-(f/.Index(b,f))) by A17,XREAL_1:19;
then
A19: LSeg(Rotate(f,f/.Index(b,f)),1) = LSeg(f,1 -' 1 + (f/.Index(b,f)) ..f)
by A18,REVROT_1:24
.= LSeg(f,0+(f/.Index(b,f))..f) by XREAL_1:232
.= LSeg(f,Index(b,f)) by A16,A15,FINSEQ_6:48;
then
A20: b in LSeg(Rotate(f,f/.Index(b,f)),1) by A13,JORDAN3:9;
A21: len f > 1+1 by GOBOARD7:34,XXREAL_0:2;
then
A22: len f-1 > 1 by XREAL_1:20;
then
A23: 1 < len f-'1 by XREAL_0:def 2;
A24: len Rotf = len f by FINSEQ_6:179;
then
A25: LSeg(Rotf,1) = LSeg(Rotf/.1,Rotf/.(1+1)) by A21,TOPREAL1:def 3;
A26: a`1 = p`1 by JORDAN18:16;
then LSeg(a,b) is vertical by A6,SPPOL_1:16;
then
A27: pion is being_S-Seq by A12,JORDAN1B:7;
A28: p`2 < a`2 by A11,JORDAN18:18;
A29: b`2 < p`2 by A11,JORDAN18:18;
then
A30: p in LSeg(a,b) by A26,A6,A28,GOBOARD7:7;
A31: LSeg(Rotf,len Rotf-'1) = LSeg(Rotf/.(len Rotf-'1),Rotf/.(len Rotf)) by A24
,A22,A7,TOPREAL1:def 3;
reconsider rf as S-Sequence_in_R2 by A24,A22,A7,JORDAN4:37;
A32: L~Rotf = L~rf \/ LSeg(Rotf,len Rotf-'1) by A24,A22,A7,GOBOARD2:3;
A33: Rotf/.1 = Rotf/.len Rotf by FINSEQ_6:def 1;
A34: b`2 < a`2 by A29,A28,XXREAL_0:2;
A35: now
assume
A36: a in LSeg(Rotf,len Rotf-'1);
per cases by SPPOL_1:19;
suppose
A37: LSeg(Rotf,1) is vertical & LSeg(Rotf,len Rotf-'1) is vertical;
then
A38: b`1 = (Rotf/.1)`1 by A13,A19,A25,JORDAN3:9,SPPOL_1:41;
A39: (Rotf/.1)`1 = (Rotf/.(1+1))`1 by A25,A37,SPPOL_1:16;
A40: (Rotf/.(len Rotf-'1))`1 = (Rotf/.(len Rotf))`1 by A31,A37,SPPOL_1:16;
per cases by A34,XXREAL_0:2;
suppose
A41: b`2 < (Rotf/.1)`2;
then
A42: (b`2+(Rotf/.1)`2)/2 < (Rotf/.1)`2 by XREAL_1:226;
A43: b`2 < (b`2+(Rotf/.1)`2)/2 by A41,XREAL_1:226;
set p1 = |[(Rotf/.1)`1,(b`2+(Rotf/.1)`2)/2]|;
A44: p1`1 = (Rotf/.1)`1 by EUCLID:52;
A45: p1`2 = (b`2+(Rotf/.1)`2)/2 by EUCLID:52;
A46: (Rotf/.1)`2 > (Rotf/.(1+1))`2 by A20,A25,A41,TOPREAL1:4;
then (Rotf/.(1+1))`2 <= b`2 by A20,A25,TOPREAL1:4;
then (Rotf/.(1+1))`2 < p1`2 by A45,A43,XXREAL_0:2;
then
A47: p1 in Lf by A1,A5,A39,A44,A45,A42,GOBOARD7:7,SPPOL_2:17;
(Rotf/.len Rotf)`2 <= (Rotf/.(len Rotf-'1))`2
proof
A48: (Rotf/.(len Rotf-'1))`2 < (Rotf/.(1+1))`2 or (Rotf/.(len Rotf-'
1))`2 >= (Rotf/.(1+1))`2;
assume (Rotf/.len Rotf)`2 > (Rotf/.(len Rotf-'1))`2;
then
Rotf/.2 in LSeg(Rotf/.(len Rotf-'1),Rotf/.(len Rotf)) or Rotf/.
(len Rotf-'1) in LSeg(Rotf/.2,Rotf/.1) by A33,A39,A40,A46,A48,GOBOARD7:7;
then
Rotf/.2 in {Rotf/.1} or Rotf/.(len Rotf-'1) in {Rotf/.1} by A4,A10,A2
,A25,A31,XBOOLE_0:def 4;
then
Rotf/.(1+1) = Rotf/.1 or Rotf/.(len Rotf-'1) = Rotf/.(len Rotf)
by A33,TARSKI:def 1;
hence contradiction by A24,A22,A9,A7,A8,Th5;
end;
then
A49: (Rotf/.len Rotf)`2 <= a`2 by A31,A36,TOPREAL1:4;
then p1`2 < a`2 by A33,A45,A42,XXREAL_0:2;
then p1 in LSeg(b,a) by A26,A6,A38,A44,A45,A43,GOBOARD7:7;
then p1 in LSeg(a,b) /\ Lf by A47,XBOOLE_0:def 4;
then p1 in {a,b} by A11,JORDAN18:22;
hence contradiction by A33,A45,A43,A42,A49,TARSKI:def 2;
end;
suppose
A50: (Rotf/.1)`2 < a`2;
then
A51: (a`2+(Rotf/.1)`2)/2 < a`2 by XREAL_1:226;
A52: (Rotf/.1)`2 < (a`2+(Rotf/.1)`2)/2 by A50,XREAL_1:226;
set p1 = |[(Rotf/.1)`1,(a`2+(Rotf/.1)`2)/2]|;
A53: p1`1 = (Rotf/.1)`1 by EUCLID:52;
A54: p1`2 = (a`2+(Rotf/.1)`2)/2 by EUCLID:52;
A55: (Rotf/.(len Rotf-'1))`2 > (Rotf/.len Rotf)`2 by A33,A31,A36,A50,
TOPREAL1:4;
then a`2 <= (Rotf/.(len Rotf-'1))`2 by A31,A36,TOPREAL1:4;
then p1`2 < (Rotf/.(len Rotf-'1))`2 by A54,A51,XXREAL_0:2;
then
A56: p1 in Lf by A1,A33,A31,A40,A53,A54,A52,GOBOARD7:7,SPPOL_2:17;
(Rotf/.(1+1))`2 <= (Rotf/.1)`2
proof
A57: (Rotf/.(len Rotf-'1))`2 < (Rotf/.(1+1))`2 or (Rotf/.(len Rotf-'
1))`2 >= (Rotf/.(1+1))`2;
assume (Rotf/.(1+1))`2 > (Rotf/.1)`2;
then
Rotf/.2 in LSeg(Rotf/.(len Rotf-'1),Rotf/.(len Rotf)) or Rotf/.
(len Rotf-'1) in LSeg(Rotf/.2,Rotf/.1) by A33,A39,A40,A55,A57,GOBOARD7:7;
then
Rotf/.2 in {Rotf/.1} or Rotf/.(len Rotf-'1) in {Rotf/.1} by A4,A10,A2
,A25,A31,XBOOLE_0:def 4;
then
Rotf/.(1+1) = Rotf/.1 or Rotf/.(len Rotf-'1) = Rotf/.(len Rotf)
by A33,TARSKI:def 1;
hence contradiction by A24,A22,A9,A7,A8,Th5;
end;
then
A58: b`2 <= (Rotf/.1)`2 by A20,A25,TOPREAL1:4;
then b`2 < p1`2 by A54,A52,XXREAL_0:2;
then p1 in LSeg(b,a) by A26,A6,A38,A53,A54,A51,GOBOARD7:7;
then p1 in LSeg(a,b) /\ Lf by A56,XBOOLE_0:def 4;
then p1 in {a,b} by A11,JORDAN18:22;
hence contradiction by A54,A52,A51,A58,TARSKI:def 2;
end;
end;
suppose
A59: LSeg(Rotf,1) is vertical & LSeg(Rotf,len Rotf-'1) is horizontal;
then
A60: a`2 = (Rotf/.len Rotf)`2 by A31,A36,SPPOL_1:40;
a`1 = (Rotf/.len Rotf)`1 by A26,A6,A13,A19,A33,A25,A59,JORDAN3:9
,SPPOL_1:41;
then a = Rotf/.len Rotf by A60,TOPREAL3:6;
then a in LSeg(Rotf/.1,Rotf/.2) by A33,RLTOPSP1:68;
then LSeg(a,b) c= LSeg(Rotf/.1,Rotf/.2) by A20,A25,TOPREAL1:6;
then p in Lf by A1,A30,A25,SPPOL_2:17;
then p in LSeg(a,b) /\ Lf by A30,XBOOLE_0:def 4;
then p in {a,b} by A11,JORDAN18:22;
hence contradiction by A29,A28,TARSKI:def 2;
end;
suppose
A61: LSeg(Rotf,1) is horizontal & LSeg(Rotf,len Rotf-'1) is vertical;
then
A62: b`2 = (Rotf/.1)`2 by A13,A19,A25,JORDAN3:9,SPPOL_1:40;
b`1 = (Rotf/.1)`1 by A26,A6,A33,A31,A36,A61,SPPOL_1:41;
then b = Rotf/.1 by A62,TOPREAL3:6;
then b in LSeg(Rotf/.(len Rotf-'1),Rotf/.len Rotf) by A33,RLTOPSP1:68;
then LSeg(a,b) c= LSeg(Rotf/.(len Rotf-'1),Rotf/.len Rotf) by A31,A36,
TOPREAL1:6;
then p in Lf by A1,A30,A31,SPPOL_2:17;
then p in LSeg(a,b) /\ Lf by A30,XBOOLE_0:def 4;
then p in {a,b} by A11,JORDAN18:22;
hence contradiction by A29,A28,TARSKI:def 2;
end;
suppose
A63: LSeg(Rotf,1) is horizontal & LSeg(Rotf,len Rotf-'1)is horizontal;
then
A64: a`2 = (Rotf/.(len Rotf-'1))`2 by A31,A36,SPPOL_1:40;
b`2 = (Rotf/.1)`2 by A13,A19,A25,A63,JORDAN3:9,SPPOL_1:40;
hence contradiction by A29,A28,A3,A25,A31,A63,A64,SPRECT_3:9;
end;
end;
a in Lf by A11,JORDAN18:17;
then
A65: a in L~rf by A1,A35,A32,XBOOLE_0:def 3;
len rf = len Rotf-'1 by FINSEQ_1:59,NAT_D:35;
then 1+1 <= len rf by A24,A23,NAT_1:13;
then
A66: b in LSeg(rf,1) by A20,SPPOL_2:3;
A67: LSeg(rf,1) c= L~rf by TOPREAL3:19;
then reconsider BCut = B_Cut(rf,b,a) as S-Sequence_in_R2 by A11,A66,A65,
JORDAN18:20,JORDAN3:37;
A68: len BCut + 1 >= 1 by NAT_1:11;
set Ga = GoB(BCut^'pion);
now
let n be Nat;
assume
A69: n in dom BCut;
then
A70: n <= len BCut by FINSEQ_3:25;
dom BCut c= dom (BCut^'pion) by Th23;
then consider i,j be Nat such that
A71: [i,j] in Indices GoB(BCut^'pion) and
A72: (BCut^'pion)/.n = GoB(BCut^'pion)*(i,j) by A69,GOBOARD2:14;
take i,j;
thus [i,j] in Indices Ga by A71;
1 <= n by A69,FINSEQ_3:25;
hence BCut/.n = Ga*(i,j) by A72,A70,FINSEQ_6:159;
end;
then consider BCut1 be FinSequence of TOP-REAL 2 such that
A73: BCut1 is_sequence_on Ga and
A74: BCut1 is being_S-Seq and
A75: L~BCut = L~BCut1 and
A76: BCut/.1 = BCut1/.1 and
A77: BCut/.len BCut = BCut1/.len BCut1 and
A78: len BCut <= len BCut1 by GOBOARD3:2;
reconsider BCut1 as S-Sequence_in_R2 by A74;
A79: L~BCut1 c= L~rf by A67,A66,A65,A75,JORDAN5B:24;
A80: len BCut1 in dom BCut1 by FINSEQ_5:6;
A81: 1 in dom BCut1 by FINSEQ_5:6;
A82: now
assume BCut1 is constant;
then BCut1/.1 = BCut1/.len BCut1 by A81,A80,FINSEQ_6:def 11;
then BCut1/.len BCut1 = b by A67,A66,A65,A76,Th19;
hence contradiction by A11,A67,A66,A65,A77,Th20,JORDAN18:20;
end;
BCut/.len BCut = a by A67,A66,A65,Th20;
then
A83: a in LSeg(BCut1/.(len BCut1-'1),BCut1/.len BCut1) by A77,RLTOPSP1:68;
A84: len BCut1 >= 1+1 by TOPREAL1:def 8;
then
A85: len BCut1-1 >= 1 by XREAL_1:19;
take BCut;
thus BCut = B_Cut(Rotate(Cage(C,n),Cage(C,n)/. Index(South-Bound(p,L~Cage(C,
n)), Cage(C,n)))|(len Rotate(Cage(C,n),Cage(C,n)/. Index(South-Bound(p,L~Cage(C
,n)), Cage(C,n)))-'1),South-Bound(p,L~Cage(C,n)),North-Bound(p,L~Cage(C,n)));
A86: LSeg(a,b) /\ Lf = {a,b} by A11,JORDAN18:22;
len BCut > 0 by NAT_1:3;
then
A87: len BCut >= 0+1 by NAT_1:13;
then
A88: (BCut^'pion)/.len BCut = BCut/.len BCut by FINSEQ_6:159
.= a by A67,A66,A65,Th20
.= pion/.1 by FINSEQ_4:17;
A89: len pion = 1+1 by FINSEQ_1:44;
then
A90: len (BCut^'pion) + 1 = len BCut + (1+1) by FINSEQ_6:139
.= len BCut + 1 + 1;
then
A91: len BCut < len (BCut^'pion) by NAT_1:13;
now
let n be Nat;
assume n in dom pion;
then
A92: n in Seg 2 by FINSEQ_1:89;
per cases by A92,FINSEQ_1:2,TARSKI:def 2;
suppose
A93: n = 1;
len BCut in Seg len (BCut^'pion) by A91,A87,FINSEQ_1:1;
then len BCut in dom (BCut^'pion) by FINSEQ_1:def 3;
then consider i,j be Nat such that
A94: [i,j] in Indices Ga and
A95: (BCut^'pion)/.len BCut = Ga*(i,j) by GOBOARD2:14;
take i,j;
thus [i,j] in Indices Ga by A94;
thus pion/.n = Ga*(i,j) by A88,A93,A95;
end;
suppose
A96: n = 1+1;
len BCut + 1 in dom (BCut^'pion) by A90,A68,FINSEQ_3:25;
then consider i,j be Nat such that
A97: [i,j] in Indices Ga and
A98: (BCut^'pion)/.(len BCut + 1) = Ga*(i,j) by GOBOARD2:14;
take i,j;
thus [i,j] in Indices Ga by A97;
thus pion/.n = Ga*(i,j) by A89,A96,A98,FINSEQ_6:160;
end;
end;
then consider pion1 be FinSequence of TOP-REAL 2 such that
A99: pion1 is_sequence_on Ga and
A100: pion1 is being_S-Seq and
A101: L~pion = L~pion1 and
A102: pion/.1 = pion1/.1 and
A103: pion/.len pion = pion1/.len pion1 and
A104: len pion <= len pion1 by A27,GOBOARD3:2;
reconsider pion1 as S-Sequence_in_R2 by A100;
A105: pion1/.len pion1 = b by A89,A103,FINSEQ_4:17
.= BCut1/.1 by A67,A66,A65,A76,Th19;
A106: L~rf c= L~f by A1,TOPREAL3:20;
then L~BCut1 c= Lf by A79;
then L~BCut1 /\ LSeg(a,b) c= {a,b} by A86,XBOOLE_1:26;
then L~BCut1 /\ L~pion1 c= {a,b} by A101,SPPOL_2:21;
then L~BCut1 /\ L~pion1 c= {a,BCut1/.1} by A67,A66,A65,A76,Th19;
then
A107: L~BCut1 /\ L~pion1 c= {BCut1/.1,pion1/.1} by A102,FINSEQ_4:17;
len BCut1 > 1 by A84,NAT_1:13;
then
A108: len BCut1-'1+1 = len BCut1 by XREAL_1:235;
A109: BCut1/.len BCut1 = a by A67,A66,A65,A77,Th20
.= pion1/.1 by A102,FINSEQ_4:17;
then
A110: BCut1^'pion1 is_sequence_on Ga by A99,A73,TOPREAL8:12;
A111: L~BCut1 c= Lf by A106,A79;
A112: now
assume b in LSeg(BCut1,len BCut1 -' 1);
then b in LSeg(BCut1/.(len BCut1-'1),BCut1/.len BCut1) by A85,A108,
TOPREAL1:def 3;
then LSeg(a,b) c= LSeg(BCut1/.(len BCut1-'1),BCut1/.len BCut1) by A83,
TOPREAL1:6;
then p in LSeg(BCut1/.(len BCut1-'1),BCut1/.len BCut1) by A30;
then p in LSeg(BCut1,len BCut1-'1) by A85,A108,TOPREAL1:def 3;
then p in L~BCut1 by SPPOL_2:17;
then p in LSeg(a,b) /\ Lf by A30,A111,XBOOLE_0:def 4;
then p in {a,b} by A11,JORDAN18:22;
hence contradiction by A29,A28,TARSKI:def 2;
end;
LSeg(BCut1,len BCut1 -' 1) c= L~BCut1 by TOPREAL3:19;
then LSeg(BCut1,len BCut1 -' 1) c= L~rf by A79;
then
A113: LSeg(BCut1,len BCut1 -' 1) c= Lf by A106;
LSeg(pion1,1) c= L~pion by A101,TOPREAL3:19;
then LSeg(pion1,1) c= LSeg(a,b) by SPPOL_2:21;
then LSeg(BCut1,len BCut1 -' 1) /\ LSeg(pion1,1) c= LSeg(a,b) /\ Lf by A113,
XBOOLE_1:27;
then
A114: LSeg(BCut1,len BCut1 -' 1) /\ LSeg(pion1,1) c= {a,b} by A11,JORDAN18:22;
A115: LSeg(BCut1,len BCut1 -' 1) /\ LSeg(pion1,1) = { BCut1/.len BCut1 }
proof
thus LSeg(BCut1,len BCut1 -' 1) /\ LSeg(pion1,1) c= { BCut1/.len BCut1 }
proof
let x be object;
assume
A116: x in LSeg(BCut1,len BCut1 -' 1) /\ LSeg(pion1,1);
then x <> b by A112,XBOOLE_0:def 4;
then x = a by A114,A116,TARSKI:def 2;
then x = BCut1/.len BCut1 by A67,A66,A65,A77,Th20;
hence thesis by TARSKI:def 1;
end;
let x be object;
assume x in { BCut1/.len BCut1 };
then
A117: x = BCut1/.len BCut1 by TARSKI:def 1;
then x in LSeg(BCut1/.(len BCut1-'1),BCut1/.len BCut1) by RLTOPSP1:68;
then
A118: x in LSeg(BCut1,len BCut1-'1) by A85,A108,TOPREAL1:def 3;
x in LSeg(pion1/.1,pion1/.(1+1)) by A109,A117,RLTOPSP1:68;
then x in LSeg(pion1,1) by A89,A104,TOPREAL1:def 3;
hence thesis by A118,XBOOLE_0:def 4;
end;
take pion1;
len <*a,b*> = 2 by FINSEQ_1:44;
hence
pion1 is_sequence_on GoB(BCut^'<*North-Bound(p,L~Cage(C,n)),South-Bound
(p,L~Cage(C,n))*>) & L~<*North-Bound(p,L~Cage(C,n)),South-Bound(p,L~Cage(C,n))
*> = L~pion1 & pion1/.1 = North-Bound(p,L~Cage(C,n)) & pion1/.len pion1 =
South-Bound(p,L~Cage(C,n)) & len pion1 >= 2 by A99,A101,A102,A103,A104,
FINSEQ_4:17;
set g = BCut1^'pion1;
now
assume len BCut = 1;
then BCut/.1 = a by A67,A66,A65,Th20;
hence contradiction by A12,A67,A66,A65,Th19;
end;
then len BCut > 1 by A87,XXREAL_0:1;
then len BCut1 > 1 by A78,XXREAL_0:2;
then
A119: len BCut1 >= 1+1 by NAT_1:13;
{BCut1/.1,pion1/.1} c= L~BCut1 /\ L~pion1
proof
let x be object;
assume x in {BCut1/.1,pion1/.1};
then
A120: x = BCut1/.1 or x = pion1/.1 by TARSKI:def 2;
then
A121: x in L~BCut1 by A109,A119,JORDAN3:1;
x in L~pion1 by A89,A104,A105,A120,JORDAN3:1;
hence thesis by A121,XBOOLE_0:def 4;
end;
then L~BCut1 /\ L~pion1 = {BCut1/.1,pion1/.1} by A107;
then reconsider
g as non constant standard special_circular_sequence by A109,A82,A110,A115
,A105,Th25,JORDAN8:4,TOPREAL8:11,33,34;
take BCut1;
thus BCut1 is_sequence_on GoB(BCut^'<*North-Bound(p,L~Cage(C,n)),South-Bound
(p,L~Cage(C,n))*>) & L~BCut = L~BCut1 & BCut/.1 = BCut1/.1 & BCut/.len BCut =
BCut1/.len BCut1 & len BCut <= len BCut1 by A73,A75,A76,A77,A78;
take g;
thus thesis;
end;