:: Upper and Lower Sequence of a Cage
:: by Robert Milewski
::
:: Received August 8, 2001
:: Copyright (c) 2001-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, SPRECT_2, RELAT_1, FINSEQ_5,
FINSEQ_4, XXREAL_0, PARTFUN1, CARD_1, ARYTM_3, ARYTM_1, PRE_TOPC,
TOPREAL1, JORDAN3, XBOOLE_0, FUNCT_1, GROUP_2, ORDINAL4, NAT_1, RLTOPSP1,
TARSKI, RCOMP_1, SPPOL_1, FINSEQ_6, JORDAN9, PSCOMP_1, GRAPH_2, TOPREAL2,
RELAT_2, MCART_1, GOBOARD1, JORDAN8, TREES_1, MATRIX_1, JORDAN1E;
notations TARSKI, XBOOLE_0, ENUMSET1, SUBSET_1, CARD_1, ORDINAL1, NUMBERS,
XCMPLX_0, XXREAL_0, NAT_1, NAT_D, FUNCT_1, PARTFUN1, FINSEQ_1, FINSEQ_4,
FINSEQ_5, MATRIX_0, MATRIX_1, FINSEQ_6, STRUCT_0, GRAPH_2, PRE_TOPC,
TOPREAL2, CONNSP_1, COMPTS_1, RLTOPSP1, EUCLID, PSCOMP_1, SPRECT_2,
GOBOARD1, TOPREAL1, SPPOL_1, JORDAN3, JORDAN8, JORDAN9;
constructors FINSEQ_4, NEWTON, FINSEQ_5, CONNSP_1, REALSET2, TOPREAL2,
PSCOMP_1, GRAPH_2, JORDAN3, JORDAN8, GOBRD13, JORDAN9, NAT_D, RELSET_1,
REAL_1, MATRIX_1;
registrations RELSET_1, XXREAL_0, XREAL_0, FINSEQ_1, FINSEQ_6, STRUCT_0,
TOPREAL2, SPPOL_2, SPRECT_2, REVROT_1, TOPREAL6, JORDAN8, JORDAN1A,
CARD_1, FUNCT_1, EUCLID, NAT_1, ORDINAL1;
requirements NUMERALS, BOOLE, SUBSET, REAL, ARITHM;
definitions TARSKI, TOPREAL1, SPRECT_2, XBOOLE_0;
equalities XBOOLE_0, PSCOMP_1, ORDINAL1;
expansions TARSKI, TOPREAL1, SPRECT_2, XBOOLE_0;
theorems JORDAN8, PSCOMP_1, JORDAN1A, NAT_1, GOBOARD5, FINSEQ_1, FINSEQ_2,
SPRECT_2, FINSEQ_4, FINSEQ_5, FINSEQ_6, GOBOARD7, SPPOL_2, REVROT_1,
TOPREAL1, SPRECT_3, JORDAN5B, JORDAN3, JORDAN9, GOBOARD1, TARSKI,
FINSEQ_3, FUNCT_1, TOPREAL5, JORDAN10, GRAPH_2, CARD_1, CARD_2, ENUMSET1,
JORDAN1B, SPRECT_5, XBOOLE_0, XREAL_1, XXREAL_0, EUCLID, PARTFUN1,
XREAL_0, MATRIX_0;
begin :: Preliminaries
reserve n for Nat;
theorem Th1:
for f,g be FinSequence of TOP-REAL 2 st f is_in_the_area_of g for
p be Element of TOP-REAL 2 st p in rng f holds f-:p is_in_the_area_of g
proof
let f,g be FinSequence of TOP-REAL 2;
assume
A1: f is_in_the_area_of g;
let p be Element of TOP-REAL 2;
assume
A2: p in rng f;
then
A3: p..f <= len f by FINSEQ_4:21;
let n be Nat;
assume
A4: n in dom(f-:p);
A5: len(f-:p) = p..f by A2,FINSEQ_5:42;
then n in Seg(p..f) by A4,FINSEQ_1:def 3;
then
A6: (f-:p)/.n = f/.n by A2,FINSEQ_5:43;
A7: n in Seg len(f-:p) by A4,FINSEQ_1:def 3;
then n <= p..f by A5,FINSEQ_1:1;
then
A8: n <= len f by A3,XXREAL_0:2;
1 <= n by A7,FINSEQ_1:1;
then n in dom f by A8,FINSEQ_3:25;
hence thesis by A1,A6;
end;
theorem Th2:
for f,g be FinSequence of TOP-REAL 2 st f is_in_the_area_of g for
p be Element of TOP-REAL 2 st p in rng f holds f:-p is_in_the_area_of g
proof
let f,g be FinSequence of TOP-REAL 2;
assume
A1: f is_in_the_area_of g;
let p be Element of TOP-REAL 2;
assume
A2: p in rng f;
let n be Nat;
1 <= p..f by A2,FINSEQ_4:21;
then
A3: 0+1 <= n-'1+p..f by XREAL_1:7;
assume
A4: n in dom(f:-p);
then
A5: n in Seg len(f:-p) by FINSEQ_1:def 3;
then
A6: 0+1 <= n by FINSEQ_1:1;
then n-'1+1 = n by XREAL_1:235;
then
A7: (f:-p)/.n = f/.(n-'1+p..f) by A2,A4,FINSEQ_5:52;
len(f:-p) = len f - p..f + 1 by A2,FINSEQ_5:50;
then n <= len f - p..f + 1 by A5,FINSEQ_1:1;
then n - 1 <= len f - p..f by XREAL_1:20;
then
A8: n - 1 + p..f <= len f by XREAL_1:19;
n-1 >= 0 by A6,XREAL_1:19;
then n-'1+p..f <= len f by A8,XREAL_0:def 2;
then n-'1+p..f in dom f by A3,FINSEQ_3:25;
hence thesis by A1,A7;
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_Cut (f,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: L_Cut (f,p) = {};
len f <> 0 by A1,TOPREAL1:22;
then f <> {};
then
A3: len f in dom f by FINSEQ_5:6;
A4: p<>f.(Index(p,f)+1) or p=f.(Index(p,f)+1);
<*p*>^mid(f,Index(p,f)+1,len f) is non empty;
then L_Cut(f,p) = mid(f,Index(p,f)+1,len f) by A2,A4,JORDAN3:def 3;
then not Index(p,f)+1 in dom f by A2,A3,SPRECT_2:7;
then Index(p,f)+1 < 1 or Index(p,f)+1 > len f by FINSEQ_3:25;
then Index(p,f) >= len f by NAT_1:11,13;
hence contradiction by A1,JORDAN3:8;
end;
theorem
for f be FinSequence of TOP-REAL 2 for p be Point of TOP-REAL 2 st p
in L~f & len R_Cut(f,p) >= 2 holds f.1 in L~R_Cut(f,p)
proof
let f be FinSequence of TOP-REAL 2;
let p be Point of TOP-REAL 2;
assume
A1: p in L~f;
then len f <> 0 by TOPREAL1:22;
then len f > 0;
then 0+1 <= len f by NAT_1:13;
then
A2: R_Cut(f,p).1 = f.1 by A1,JORDAN1B:3;
assume 2 <= len R_Cut(f,p);
hence thesis by A2,JORDAN3:1;
end;
theorem Th5:
for f be FinSequence of TOP-REAL 2 st f is being_S-Seq for p be
Point of TOP-REAL 2 st p in L~f holds not f.1 in L~mid(f,Index(p,f)+1,len f)
proof
let f be FinSequence of TOP-REAL 2 such that
A1: f is being_S-Seq;
let p be Point of TOP-REAL 2 such that
A2: p in L~f and
A3: f.1 in L~mid(f,Index(p,f)+1,len f);
len f <> 0 by A2,TOPREAL1:22;
then f <> {};
then 1 in dom f by FINSEQ_5:6;
then
A4: f/.1 in L~mid(f,Index(p,f)+1,len f) by A3,PARTFUN1:def 6;
Index(p,f) < len f by A2,JORDAN3:8;
then Index(p,f)+1 <= len f by NAT_1:13;
then Index(p,f)+1 = 0+1 by A1,A4,JORDAN5B:16,NAT_1:11;
hence contradiction by A2,JORDAN3:8;
end;
theorem Th6:
for i,j,m,n be Nat holds i+j = m+n & i <= m & j <= n implies i = m
proof
let i,j,m,n be Nat;
assume that
A1: i+j = m+n and
A2: i <= m and
A3: j <= n;
consider k be Nat such that
A4: m = i + k by A2,NAT_1:10;
consider l be Nat such that
A5: n = j + l by A3,NAT_1:10;
j + (l+k) = j+0 by A1,A4,A5;
then k = 0;
hence thesis by A4;
end;
theorem
for f be FinSequence of TOP-REAL 2 st f is being_S-Seq for p be Point
of TOP-REAL 2 st p in L~f & f.1 in L~L_Cut(f,p) holds f.1 = p
proof
let f be FinSequence of TOP-REAL 2;
assume
A1: f is being_S-Seq;
A2: len f in dom f by A1,FINSEQ_5:6;
1 in dom f by A1,FINSEQ_5:6;
then
A3: f/.1 = f.1 by PARTFUN1:def 6;
let p be Point of TOP-REAL 2 such that
A4: p in L~f and
A5: f.1 in L~L_Cut(f,p) and
A6: f.1 <> p;
set g = mid(f,Index(p,f)+1,len f);
A7: not f.1 in L~g by A1,A4,Th5;
then p<>f.(Index(p,f)+1) by A5,JORDAN3:def 3;
then
A8: L_Cut(f,p) = <*p*>^g by JORDAN3:def 3;
per cases;
suppose
g is empty;
then L_Cut(f,p) = <*p*> by A8,FINSEQ_1:34;
then len L_Cut(f,p) = 1 by FINSEQ_1:39;
hence contradiction by A5,TOPREAL1:22;
end;
suppose
g is non empty;
then L~L_Cut(f,p) = LSeg(p,g/.1) \/ L~g by A8,SPPOL_2:20;
then
A9: f.1 in LSeg(p,g/.1) by A5,A7,XBOOLE_0:def 3;
A10: 1+1 <= len f by A1;
then
A11: 2 in dom f by FINSEQ_3:25;
consider i being Nat such that
A12: 1 <= i and
A13: i+1 <= len(<*p*>^g) and
A14: f/.1 in LSeg(<*p*>^g,i) by A5,A3,A8,SPPOL_2:13;
LSeg(<*p*>^g,i) c= LSeg(f,Index(p,f)+i-'1) by A4,A12,A13,JORDAN3:16;
then
A15: Index(p,f)+i-'1 = 1 by A1,A14,JORDAN5B:30;
A16: 1 <= Index(p,f) by A4,JORDAN3:8;
then 1+1 <= Index(p,f)+i by A12,XREAL_1:7;
then
A17: Index(p,f)+i = 1+1 by A15,XREAL_1:235,XXREAL_0:2;
then Index(p,f) = 1 by A12,A16,Th6;
then p in LSeg(f,1) by A4,JORDAN3:9;
then
A18: p in LSeg(f/.1,f/.(1+1)) by A10,TOPREAL1:def 3;
i = 1 by A12,A16,A17,Th6;
then g/.1 = f/.(1+1) by A2,A17,A11,SPRECT_2:8;
hence contradiction by A6,A3,A9,A18,SPRECT_3:6;
end;
end;
begin :: About Upper and Lower Sequence of a Cage
definition
let C be compact non vertical non horizontal Subset of TOP-REAL 2;
let n be Nat;
func Upper_Seq(C,n) -> FinSequence of TOP-REAL 2 equals
Rotate(Cage(C,n),
W-min L~Cage(C,n))-:E-max L~Cage(C,n);
coherence;
end;
theorem Th8:
for C be compact non vertical non horizontal Subset of TOP-REAL
2 for n be Nat holds len Upper_Seq(C,n) = (E-max L~Cage(C,n))..Rotate(Cage(C,n)
,W-min L~Cage(C,n))
proof
let C be compact non vertical non horizontal non empty Subset of TOP-REAL 2;
let n be Nat;
E-max L~Cage(C,n) in rng Cage(C,n) by SPRECT_2:46;
then E-max L~Cage(C,n) in rng Rotate(Cage(C,n),W-min L~Cage(C,n)) by
FINSEQ_6:90,SPRECT_2:43;
hence thesis by FINSEQ_5:42;
end;
definition
let C be compact non vertical non horizontal Subset of TOP-REAL 2;
let n be Nat;
func Lower_Seq(C,n) -> FinSequence of TOP-REAL 2 equals
Rotate(Cage(C,n),
W-min L~Cage(C,n)):-E-max L~Cage(C,n);
coherence;
end;
theorem Th9:
for C be compact non vertical non horizontal Subset of TOP-REAL
2 for n be Nat holds len Lower_Seq(C,n) = len Rotate(Cage(C,n),W-min L~Cage(C,n
))- (E-max L~Cage(C,n))..Rotate(Cage(C,n),W-min L~Cage(C,n))+1
proof
let C be compact non vertical non horizontal Subset of TOP-REAL 2;
let n be Nat;
E-max L~Cage(C,n) in rng Cage(C,n) by SPRECT_2:46;
then E-max L~Cage(C,n) in rng Rotate(Cage(C,n),W-min L~Cage(C,n)) by
FINSEQ_6:90,SPRECT_2:43;
hence thesis by FINSEQ_5:50;
end;
registration
let C be compact non vertical non horizontal Subset of TOP-REAL 2;
let n be Nat;
cluster Upper_Seq(C,n) -> non empty;
coherence
proof
E-max L~Cage(C,n) in rng Cage(C,n) by SPRECT_2:46;
then
A1: E-max L~Cage(C,n) in rng Rotate(Cage(C,n),W-min L~Cage(C,n)) by FINSEQ_6:90
,SPRECT_2:43;
len Upper_Seq(C,n) = (E-max L~Cage(C,n))..Rotate(Cage(C,n), W-min L~
Cage(C,n)) by Th8;
hence thesis by A1,FINSEQ_4:21;
end;
cluster Lower_Seq(C,n) -> non empty;
coherence
proof
E-max L~Cage(C,n) in rng Cage(C,n) by SPRECT_2:46;
then
A2: E-max L~Cage(C,n) in rng Rotate(Cage(C,n),W-min L~Cage(C,n)) by FINSEQ_6:90
,SPRECT_2:43;
len Lower_Seq(C,n) = len Rotate(Cage(C,n),W-min L~Cage(C,n))- (E-max
L~Cage(C,n))..Rotate(Cage(C,n),W-min L~Cage(C,n))+1 by Th9;
then len Rotate(Cage(C,n),W-min L~Cage(C,n))-len Lower_Seq(C,n)+1 <= len
Rotate(Cage(C,n),W-min L~Cage(C,n)) by A2,FINSEQ_4:21;
then len Rotate(Cage(C,n),W-min L~Cage(C,n))-len Lower_Seq(C,n) <= len
Rotate(Cage(C,n),W-min L~Cage(C,n))-1 by XREAL_1:19;
hence thesis by XREAL_1:10;
end;
end;
registration
let C be compact non vertical non horizontal Subset of TOP-REAL 2;
let n be Nat;
cluster Upper_Seq(C,n) -> one-to-one special unfolded s.n.c.;
coherence
proof
set f = Rotate(Cage(C,n),W-min L~Cage(C,n));
A1: W-min L~Cage(C,n) in rng Cage(C,n) by SPRECT_2:43;
E-max L~Cage(C,n) in rng Cage(C,n) by SPRECT_2:46;
then
A2: E-max L~Cage(C,n) in rng f by FINSEQ_6:90,SPRECT_2:43;
A3: len Upper_Seq(C,n) = (E-max L~Cage(C,n))..f by Th8;
now
let i1,j1 be object;
assume that
A4: i1 in dom Upper_Seq(C,n) and
A5: j1 in dom Upper_Seq(C,n) and
A6: Upper_Seq(C,n).i1 = Upper_Seq(C,n).j1 and
A7: i1 <> j1;
reconsider i2 = i1, j2 = j1 as Nat by A4,A5;
A8: i2 in Seg((E-max L~Cage(C,n))..f) by A3,A4,FINSEQ_1:def 3;
then
A9: 1 <= i2 by FINSEQ_1:1;
A10: L~Cage(C,n) = L~f by REVROT_1:33;
A11: j2 in Seg((E-max L~Cage(C,n))..f) by A3,A5,FINSEQ_1:def 3;
then
A12: 1 <= j2 by FINSEQ_1:1;
j2 <= (E-max L~Cage(C,n))..f by A11,FINSEQ_1:1;
then
A13: j2 < len f by A10,SPRECT_5:16,XXREAL_0:2;
A14: Upper_Seq(C,n).j1 = Upper_Seq(C,n)/.j2 by A5,PARTFUN1:def 6
.= f/.j2 by A2,A11,FINSEQ_5:43;
i2 <= (E-max L~Cage(C,n))..f by A8,FINSEQ_1:1;
then
A15: i2 < len f by A10,SPRECT_5:16,XXREAL_0:2;
A16: Upper_Seq(C,n).i1 = Upper_Seq(C,n)/.i2 by A4,PARTFUN1:def 6
.= f/.i2 by A2,A8,FINSEQ_5:43;
per cases by A7,XXREAL_0:1;
suppose
i2 < j2;
hence contradiction by A6,A16,A14,A9,A13,GOBOARD7:36;
end;
suppose
j2 < i2;
hence contradiction by A6,A16,A14,A12,A15,GOBOARD7:36;
end;
end;
hence Upper_Seq(C,n) is one-to-one by FUNCT_1:def 4;
thus Upper_Seq(C,n) is special;
thus Upper_Seq(C,n) is unfolded;
let i,j be Nat;
assume
A17: i+1 < j;
0+1 <= len f by NAT_1:13;
then
A18: len f in dom f by FINSEQ_3:25;
now
per cases;
suppose
A19: j+1 <= len Upper_Seq(C,n);
A20: (E-max L~Cage(C,n))..f <= len f by A2,FINSEQ_4:21;
A21: j+1 <= (E-max L~Cage(C,n))..f by A2,A19,FINSEQ_5:42;
A22: now
per cases by A21,XXREAL_0:1;
suppose
j+1 < (E-max L~Cage(C,n))..f;
hence j+1 < len f by A20,XXREAL_0:2;
end;
suppose
A23: j+1 = (E-max L~Cage(C,n))..f;
assume j+1 >= len f;
then (E-max L~Cage(C,n))..f = len f by A20,A23,XXREAL_0:1;
then E-max L~Cage(C,n) = f.(len f) by A2,FINSEQ_4:19
.= f/.(len f) by A18,PARTFUN1:def 6
.= f/.1 by FINSEQ_6:def 1
.= W-min L~Cage(C,n) by A1,FINSEQ_6:92;
hence contradiction by TOPREAL5:19;
end;
end;
j < len Upper_Seq(C,n) by A19,NAT_1:13;
then
A24: LSeg(Upper_Seq(C,n),i) = LSeg(f,i) by A17,SPPOL_2:9,XXREAL_0:2;
LSeg(Upper_Seq(C,n),j) = LSeg(f,j) by A19,SPPOL_2:9;
hence thesis by A17,A24,A22,GOBOARD5:def 4;
end;
suppose
j+1 > len Upper_Seq(C,n);
then LSeg(Upper_Seq(C,n),j) = {} by TOPREAL1:def 3;
then LSeg(Upper_Seq(C,n),i) /\ LSeg(Upper_Seq(C,n),j) = {};
hence thesis;
end;
end;
hence thesis;
end;
cluster Lower_Seq(C,n) -> one-to-one special unfolded s.n.c.;
coherence
proof
set f = Rotate(Cage(C,n),W-min L~Cage(C,n));
A25: L~Cage(C,n) = L~f by REVROT_1:33;
W-min L~Cage(C,n) in rng Cage(C,n) by SPRECT_2:43;
then
A26: f/.1 = W-min L~f by A25,FINSEQ_6:92;
then (W-max L~Cage(C,n))..f <= (N-min L~Cage(C,n))..f by A25,SPRECT_5:23;
then (N-min L~Cage(C,n))..f > 1 by A25,A26,SPRECT_5:22,XXREAL_0:2;
then (N-max L~Cage(C,n))..f > 1 by A25,A26,SPRECT_5:24,XXREAL_0:2;
then
A27: (E-max L~Cage(C,n))..f > 1 by A25,A26,SPRECT_5:25,XXREAL_0:2;
E-max L~Cage(C,n) in rng Cage(C,n) by SPRECT_2:46;
then
A28: E-max L~Cage(C,n) in rng f by FINSEQ_6:90,SPRECT_2:43;
A29: len Lower_Seq(C,n) = len f-(E-max L~Cage(C,n))..f+1 by Th9;
now
let i1,j1 be object;
assume that
A30: i1 in dom Lower_Seq(C,n) and
A31: j1 in dom Lower_Seq(C,n) and
A32: Lower_Seq(C,n).i1 = Lower_Seq(C,n).j1 and
A33: i1 <> j1;
reconsider i2 = i1, j2 = j1 as Nat by A30,A31;
A34: i2 in Seg len Lower_Seq(C,n) by A30,FINSEQ_1:def 3;
then i2 >= 1 by FINSEQ_1:1;
then
A35: i2 = i2-'1+1 by XREAL_1:235;
A36: Lower_Seq(C,n).i1 = Lower_Seq(C,n)/.i2 by A30,PARTFUN1:def 6
.= f/.(i2-'1+(E-max L~Cage(C,n))..f) by A28,A30,A35,FINSEQ_5:52;
A37: j2 in Seg len Lower_Seq(C,n) by A31,FINSEQ_1:def 3;
then j2 >= 1 by FINSEQ_1:1;
then
A38: j2 = j2-'1+1 by XREAL_1:235;
A39: Lower_Seq(C,n).j1 = Lower_Seq(C,n)/.j2 by A31,PARTFUN1:def 6
.= f/.(j2-'1+(E-max L~Cage(C,n))..f) by A28,A31,A38,FINSEQ_5:52;
0+1 <= i2 by A34,FINSEQ_1:1;
then
A40: i2-1 >= 0 by XREAL_1:19;
i2 <= len f-(E-max L~Cage(C,n))..f+1 by A29,A34,FINSEQ_1:1;
then i2-1 <= len f-(E-max L~Cage(C,n))..f by XREAL_1:20;
then i2-1+(E-max L~Cage(C,n))..f <= len f by XREAL_1:19;
then
A41: i2-'1+(E-max L~Cage(C,n))..f <= len f by A40,XREAL_0:def 2;
0+1 <= j2 by A37,FINSEQ_1:1;
then
A42: j2-1 >= 0 by XREAL_1:19;
j2 <= len f-(E-max L~Cage(C,n))..f+1 by A29,A37,FINSEQ_1:1;
then j2-1 <= len f-(E-max L~Cage(C,n))..f by XREAL_1:20;
then j2-1+(E-max L~Cage(C,n))..f <= len f by XREAL_1:19;
then
A43: j2-'1+(E-max L~Cage(C,n))..f <= len f by A42,XREAL_0:def 2;
j2-'1+(E-max L~Cage(C,n))..f >= (E-max L~Cage(C,n))..f by NAT_1:11;
then
A44: 1 < j2-'1+(E-max L~Cage(C,n))..f by A27,XXREAL_0:2;
i2-'1+(E-max L~Cage(C,n))..f >= (E-max L~Cage(C,n))..f by NAT_1:11;
then
A45: 1 < i2-'1+(E-max L~Cage(C,n))..f by A27,XXREAL_0:2;
per cases by A33,XXREAL_0:1;
suppose
i2 < j2;
then i2-1 < j2-1 by XREAL_1:9;
then i2-1 < j2-'1 by XREAL_0:def 2;
then i2-'1 < j2-'1 by A40,XREAL_0:def 2;
then i2-'1+(E-max L~Cage(C,n))..f < j2-'1+(E-max L~Cage(C,n))..f by
XREAL_1:6;
hence contradiction by A32,A36,A39,A43,A45,GOBOARD7:37;
end;
suppose
j2 < i2;
then j2-1 < i2-1 by XREAL_1:9;
then j2-1 < i2-'1 by XREAL_0:def 2;
then j2-'1 < i2-'1 by A42,XREAL_0:def 2;
then j2-'1+(E-max L~Cage(C,n))..f < i2-'1+(E-max L~Cage(C,n))..f by
XREAL_1:6;
hence contradiction by A32,A36,A39,A41,A44,GOBOARD7:37;
end;
end;
hence Lower_Seq(C,n) is one-to-one by FUNCT_1:def 4;
E-max L~Cage(C,n) in rng Cage(C,n) by SPRECT_2:46;
then
A46: E-max L~Cage(C,n) in rng Rotate(Cage(C,n),W-min L~Cage(C,n)) by
FINSEQ_6:90,SPRECT_2:43;
hence Lower_Seq(C,n) is special by SPPOL_2:39;
thus Lower_Seq(C,n) is unfolded by A46,SPPOL_2:27;
let i,j be Nat;
assume
A47: i+1 < j;
i+1 >= 1 by NAT_1:11;
then j = j-'1+1 by A47,XREAL_1:235,XXREAL_0:2;
then
A48: LSeg(Lower_Seq(C,n),j) = LSeg(f,j-'1+(E-max L~Cage(C,n))..f) by A46,
SPPOL_2:10;
now
per cases;
suppose
i > 0;
then
A49: i >= 0+1 by NAT_1:13;
then i = i-'1+1 by XREAL_1:235;
then
A50: LSeg(Lower_Seq(C,n),i) = LSeg(f,i-'1+(E-max L~Cage(C,n)).. f) by A28,
SPPOL_2:10;
i+1-1 < j-1 by A47,XREAL_1:9;
then
A51: i-1+1 < j-'1 by XREAL_0:def 2;
i-1 >= 0 by A49,XREAL_1:19;
then i-'1+1 < j-'1 by A51,XREAL_0:def 2;
then i-'1+1+(E-max L~Cage(C,n))..f < j-'1+(E-max L~Cage(C,n))..f by
XREAL_1:6;
then
A52: i-'1+(E-max L~Cage(C,n))..f+1 < j-'1+(E-max L~Cage(C,n)).. f;
A53: i-'1+(E-max L~Cage(C,n))..f > 0+1 by A27,XREAL_1:8;
now
per cases;
suppose
j-'1+(E-max L~Cage(C,n))..f+1 <= len f;
then j-'1+(E-max L~Cage(C,n))..f < len f by NAT_1:13;
then LSeg(Lower_Seq(C,n),i) misses LSeg(Lower_Seq(C,n),j) by A48
,A50,A52,A53,GOBOARD5:def 4;
hence LSeg(Lower_Seq(C,n),i) /\ LSeg(Lower_Seq(C,n),j) = {};
end;
suppose
j-'1+(E-max L~Cage(C,n))..f+1 > len f;
then LSeg(Lower_Seq(C,n),j) = {} by A48,TOPREAL1:def 3;
hence LSeg(Lower_Seq(C,n),i) /\ LSeg(Lower_Seq(C,n),j) = {};
end;
end;
hence LSeg(Lower_Seq(C,n),i) /\ LSeg(Lower_Seq(C,n),j) = {};
end;
suppose
i = 0;
then LSeg(Lower_Seq(C,n),i) = {} by TOPREAL1:def 3;
hence LSeg(Lower_Seq(C,n),i) /\ LSeg(Lower_Seq(C,n),j) = {};
end;
end;
hence thesis;
end;
end;
theorem Th10:
for C be compact non vertical non horizontal Subset of TOP-REAL
2 for n be Nat holds len Upper_Seq(C,n) + len Lower_Seq(C,n) = len
Cage(C,n)+1
proof
let C be compact non vertical non horizontal Subset of TOP-REAL 2;
let n be Nat;
thus len Upper_Seq(C,n) + len Lower_Seq(C,n) = (E-max L~Cage(C,n))..Rotate(
Cage(C,n),W-min L~Cage(C,n))+ len Lower_Seq(C,n) by Th8
.= (E-max L~Cage(C,n))..Rotate(Cage(C,n),W-min L~Cage(C,n))+ (len Rotate
(Cage(C,n),W-min L~Cage(C,n))- (E-max L~Cage(C,n))..Rotate(Cage(C,n),W-min L~
Cage(C,n))+1) by Th9
.= (E-max L~Cage(C,n))..Rotate(Cage(C,n),W-min L~Cage(C,n))+ len Rotate(
Cage(C,n),W-min L~Cage(C,n))- (E-max L~Cage(C,n))..Rotate(Cage(C,n),W-min L~
Cage(C,n))+1
.= len Cage(C,n)+1 by FINSEQ_6:179;
end;
theorem Th11:
for C be compact non vertical non horizontal Subset of TOP-REAL
2 for n be Nat holds Rotate(Cage(C,n),W-min L~Cage(C,n)) = Upper_Seq
(C,n) ^' Lower_Seq(C,n)
proof
let C be compact non vertical non horizontal Subset of TOP-REAL 2;
let n be Nat;
A1: dom Rotate(Cage(C,n),W-min L~Cage(C,n)) = Seg len Rotate(Cage(C,n),W-min
L~Cage(C,n)) by FINSEQ_1:def 3;
A2: len (Upper_Seq(C,n) ^' Lower_Seq(C,n)) +1 = len Upper_Seq(C,n) + len
Lower_Seq(C,n) by FINSEQ_6:139
.= len Cage(C,n)+1 by Th10
.= len Rotate(Cage(C,n),W-min L~Cage(C,n))+1 by FINSEQ_6:179;
now
let i be Nat;
E-max L~Cage(C,n) in rng Cage(C,n) by SPRECT_2:46;
then
A3: E-max L~Cage(C,n) in rng Rotate(Cage(C,n),W-min L~Cage(C,n)) by FINSEQ_6:90
,SPRECT_2:43;
assume
A4: i in dom Rotate(Cage(C,n),W-min L~Cage(C,n));
then
A5: 1 <= i by A1,FINSEQ_1:1;
A6: i <= len Rotate(Cage(C,n),W-min L~Cage(C,n)) by A1,A4,FINSEQ_1:1;
per cases;
suppose
A7: i <= len Upper_Seq(C,n);
then
i <= (E-max L~Cage(C,n))..Rotate(Cage(C,n),W-min L~Cage(C,n)) by Th8;
then
A8: i in Seg ((E-max L~Cage(C,n))..Rotate(Cage(C,n), W-min L~Cage(C,n))
) by A5,FINSEQ_1:1;
len (Rotate(Cage(C,n),W-min L~Cage(C,n))-:E-max L~Cage(C,n)) = (
E-max L~Cage(C,n))..Rotate(Cage(C,n),W-min L~Cage(C,n)) by A3,FINSEQ_5:42;
then
A9: i in dom (Rotate(Cage(C,n),W-min L~Cage(C,n))-: E-max L~Cage(C,n))
by A8,FINSEQ_1:def 3;
thus (Upper_Seq(C,n) ^' Lower_Seq(C,n)).i = (Rotate(Cage(C,n),W-min L~
Cage(C,n))-:E-max L~Cage(C,n)).i by A5,A7,FINSEQ_6:140
.= (Rotate(Cage(C,n),W-min L~Cage(C,n))-:E-max L~Cage(C,n))/.i by A9,
PARTFUN1:def 6
.= Rotate(Cage(C,n),W-min L~Cage(C,n))/.i by A3,A8,FINSEQ_5:43
.= Rotate(Cage(C,n),W-min L~Cage(C,n)).i by A4,PARTFUN1:def 6;
end;
suppose
i > len Upper_Seq(C,n);
then i >= len Upper_Seq(C,n)+1 by NAT_1:13;
then consider j be Nat such that
A10: i = len Upper_Seq(C,n)+1+j by NAT_1:10;
reconsider j as Nat;
A11: i = len Upper_Seq(C,n)+(j+1) by A10;
then
A12: i = (E-max L~Cage(C,n))..Rotate(Cage(C,n),W-min L~Cage(C,n))+(j+1)
by Th8;
A13: len (Rotate(Cage(C,n),W-min L~Cage(C,n)):-E-max L~Cage(C,n)) = len
Rotate(Cage(C,n),W-min L~Cage(C,n))- (E-max L~Cage(C,n))..Rotate(Cage(C,n),
W-min L~Cage(C,n))+1 by A3,FINSEQ_5:50;
j+1+(E-max L~Cage(C,n))..Rotate(Cage(C,n),W-min L~Cage(C,n)) <= len
Rotate(Cage(C,n),W-min L~Cage(C,n)) by A6,A11,Th8;
then
j+1 <= len Rotate(Cage(C,n),W-min L~Cage(C,n))- (E-max L~Cage(C,n))
..Rotate(Cage(C,n),W-min L~Cage(C,n)) by XREAL_1:19;
then j+1+1 >= 1 & j+1+1 <= len (Rotate(Cage(C,n),W-min L~Cage(C,n)):- (
E-max L~ Cage(C,n))) by A13,NAT_1:11,XREAL_1:7;
then
A14: j+1+1 in dom (Rotate(Cage(C,n),W-min L~Cage(C,n)):- (E-max L~Cage(C
,n))) by FINSEQ_3:25;
i < len (Upper_Seq(C,n) ^' Lower_Seq(C,n))+1 by A2,A6,NAT_1:13;
then i < len Lower_Seq(C,n) + len Upper_Seq(C,n)
by FINSEQ_6:139;
then i-len Upper_Seq(C,n) < len Lower_Seq(C,n) by XREAL_1:19;
hence (Upper_Seq(C,n) ^' Lower_Seq(C,n)).i = (Rotate(Cage(C,n),W-min L~
Cage(C,n)):-(E-max L~Cage(C,n))). (j+1+1)
by A11,FINSEQ_6:141,NAT_1:11
.= (Rotate(Cage(C,n),W-min L~Cage(C,n)):-(E-max L~Cage(C,n)))/. (j+1
+1) by A14,PARTFUN1:def 6
.= Rotate(Cage(C,n),W-min L~Cage(C,n))/. (j+1+(E-max L~Cage(C,n))..
Rotate(Cage(C,n),W-min L~Cage(C,n))) by A3,A14,FINSEQ_5:52
.= Rotate(Cage(C,n),W-min L~Cage(C,n)).i by A4,A12,PARTFUN1:def 6;
end;
end;
hence thesis by A2,FINSEQ_2:9;
end;
theorem
for C be compact non vertical non horizontal Subset of TOP-REAL 2 for
n be Nat holds L~Cage(C,n) = L~(Upper_Seq(C,n) ^' Lower_Seq(C,n))
proof
let C be compact non vertical non horizontal Subset of TOP-REAL 2;
let n be Nat;
Rotate(Cage(C,n),W-min L~Cage(C,n)) = Upper_Seq(C,n) ^' Lower_Seq(C,n)
by Th11;
hence thesis by REVROT_1:33;
end;
theorem
for C be compact non vertical non horizontal non empty Subset of
TOP-REAL 2 for n be Nat holds L~Cage(C,n) = L~Upper_Seq(C,n) \/ L~
Lower_Seq(C,n)
proof
let C be compact non vertical non horizontal non empty Subset of TOP-REAL 2;
let n be Nat;
E-max L~Cage(C,n) in rng Cage(C,n) by SPRECT_2:46;
then E-max L~Cage(C,n) in rng Rotate(Cage(C,n),W-min L~Cage(C,n)) by
FINSEQ_6:90,SPRECT_2:43;
then
L~Rotate(Cage(C,n),W-min L~Cage(C,n)) = L~Upper_Seq(C,n) \/ L~Lower_Seq(
C,n) by SPPOL_2:24;
hence thesis by REVROT_1:33;
end;
theorem Th14:
for P be Simple_closed_curve holds W-min(P) <> E-min(P)
proof
let P be Simple_closed_curve;
now
assume W-min(P) = E-min(P);
then W-bound P= E-bound P by SPPOL_2:1;
hence contradiction by TOPREAL5:17;
end;
hence thesis;
end;
theorem Th15:
for C be compact non vertical non horizontal Subset of TOP-REAL
2 for n be Nat holds len Upper_Seq(C,n) >= 3 & len Lower_Seq(C,n) >=
3
proof
let C be compact non vertical non horizontal Subset of TOP-REAL 2;
let n be Nat;
set pWi = W-min L~Cage(C,n);
set pWa = W-max L~Cage(C,n);
set pEi = E-min L~Cage(C,n);
set pEa = E-max L~Cage(C,n);
A1: pWi <> pEa by TOPREAL5:19;
set f=Rotate(Cage(C,n),W-min L~Cage(C,n));
A2: W-min L~Cage(C,n) in rng Cage(C,n) by SPRECT_2:43;
E-max L~Cage(C,n) in rng Cage(C,n) by SPRECT_2:46;
then
A3: E-max L~Cage(C,n) in rng Rotate(Cage(C,n),W-min L~Cage(C,n)) by FINSEQ_6:90
,SPRECT_2:43;
then
Lower_Seq(C,n)/.(len Lower_Seq(C,n)) = Rotate(Cage(C,n),W-min L~Cage(C,
n))/. (len Rotate(Cage(C,n),W-min L~Cage(C,n))) by FINSEQ_5:54
.= Rotate(Cage(C,n),W-min L~Cage(C,n))/.1 by FINSEQ_6:def 1
.= W-min L~Cage(C,n) by A2,FINSEQ_6:92;
then
A4: pEa in rng Lower_Seq(C,n) & pWi in rng Lower_Seq(C,n) by FINSEQ_6:61
,FINSEQ_6:168;
(E-max L~Cage(C,n))..Rotate(Cage(C,n),W-min L~Cage(C,n)) <= (E-max L~
Cage(C,n))..Rotate(Cage(C,n),W-min L~Cage(C,n));
then
A5: pEa in rng Upper_Seq(C,n) by A3,FINSEQ_5:46;
pWa in rng Cage(C,n) by SPRECT_2:44;
then
A6: pWa in rng Rotate(Cage(C,n),W-min L~Cage(C,n)) by FINSEQ_6:90,SPRECT_2:43;
A7: Upper_Seq(C,n)/.1 = Rotate(Cage(C,n),W-min L~Cage(C,n))/.1 by A3,
FINSEQ_5:44;
then
A8: Upper_Seq(C,n)/.1 = W-min L~Cage(C,n) by A2,FINSEQ_6:92;
then
A9: pWi in rng Upper_Seq(C,n) by FINSEQ_6:42;
A10: L~Cage(C,n) = L~f by REVROT_1:33;
then (W-max L~f)..f <= (N-min L~f)..f by A2,A7,FINSEQ_6:92,SPRECT_5:23;
then
A11: (W-max L~f)..f < (N-max L~f)..f by A7,A8,A10,SPRECT_5:24,XXREAL_0:2;
(N-max L~f)..f <= (E-max L~f)..f by A2,A7,A10,FINSEQ_6:92,SPRECT_5:25;
then
A12: pWa in rng Upper_Seq(C,n) by A3,A6,A10,A11,FINSEQ_5:46,XXREAL_0:2;
{pWi,pWa,pEa} c= rng Upper_Seq(C,n)
by A5,A9,A12,ENUMSET1:def 1;
then
A13: card {pWi,pWa,pEa} c= card rng Upper_Seq(C,n) by CARD_1:11;
card rng Upper_Seq(C,n) c= card dom Upper_Seq(C,n) by CARD_2:61;
then
A14: card rng Upper_Seq(C,n) c= len Upper_Seq(C,n) by CARD_1:62;
pWi <> pWa & pWa <> pEa by JORDAN1B:5,SPRECT_2:58;
then card {pWi,pWa,pEa} = 3 by A1,CARD_2:58;
then Segm 3 c= Segm len Upper_Seq(C,n) by A13,A14;
hence len Upper_Seq(C,n) >= 3 by NAT_1:39;
A15: pWi <> pEa by TOPREAL5:19;
pEi in rng Cage(C,n) by SPRECT_2:45;
then
A16: pEi in rng Rotate(Cage(C,n),W-min L~Cage(C,n)) by FINSEQ_6:90,SPRECT_2:43;
pEi..Rotate(Cage(C,n),W-min L~Cage(C,n)) > pEa..Rotate(Cage(C,n),W-min
L~Cage(C,n)) by A2,A7,A10,FINSEQ_6:92,SPRECT_5:26;
then
A17: pEi in rng Lower_Seq(C,n) by A3,A16,FINSEQ_6:62;
{pWi,pEi,pEa} c= rng Lower_Seq(C,n)
by A4,A17,ENUMSET1:def 1;
then
A18: card {pWi,pEi,pEa} c= card rng Lower_Seq(C,n) by CARD_1:11;
card rng Lower_Seq(C,n) c= card dom Lower_Seq(C,n) by CARD_2:61;
then
A19: card rng Lower_Seq(C,n) c= len Lower_Seq(C,n) by CARD_1:62;
pWi <> pEi & pEi <> pEa by Th14,SPRECT_2:54;
then card {pWi,pEi,pEa} = 3 by A15,CARD_2:58;
then Segm 3 c= Segm len Lower_Seq(C,n) by A18,A19;
hence thesis by NAT_1:39;
end;
registration
let C be compact non vertical non horizontal Subset of TOP-REAL 2;
let n be Nat;
cluster Upper_Seq(C,n) -> being_S-Seq;
coherence
proof
len Upper_Seq(C,n) >= 3 by Th15;
then len Upper_Seq(C,n) >= 2 by XXREAL_0:2;
hence thesis;
end;
cluster Lower_Seq(C,n) -> being_S-Seq;
coherence
proof
len Lower_Seq(C,n) >= 3 by Th15;
then len Lower_Seq(C,n) >= 2 by XXREAL_0:2;
hence thesis;
end;
end;
theorem
for C be compact non vertical non horizontal Subset of TOP-REAL 2 for
n be Nat holds L~Upper_Seq(C,n) /\ L~Lower_Seq(C,n) = {W-min L~Cage(
C,n),E-max L~Cage(C,n)}
proof
let C be compact non vertical non horizontal Subset of TOP-REAL 2;
let n be Nat;
E-max L~Cage(C,n) in rng Cage(C,n) by SPRECT_2:46;
then
A1: E-max L~Cage(C,n) in rng Rotate(Cage(C,n),W-min L~Cage(C,n)) by FINSEQ_6:90
,SPRECT_2:43;
A2: len Upper_Seq(C,n) >= 3 by Th15;
then
A3: rng Upper_Seq(C,n) c= L~Upper_Seq(C,n) by SPPOL_2:18,XXREAL_0:2;
A4: W-min L~Cage(C,n) in rng Cage(C,n) by SPRECT_2:43;
thus L~Upper_Seq(C,n) /\ L~Lower_Seq(C,n) c= {W-min L~Cage(C,n),E-max L~Cage
(C,n)}
proof
set pW=W-min L~Cage(C,n);
set pE=E-max L~Cage(C,n);
set f=Rotate(Cage(C,n),W-min L~Cage(C,n));
let x be object;
assume
A5: x in L~Upper_Seq(C,n) /\ L~Lower_Seq(C,n);
then reconsider x1=x as Point of TOP-REAL 2;
assume
A6: not x in {W-min L~Cage(C,n),E-max L~Cage(C,n)};
x in L~Upper_Seq(C,n) by A5,XBOOLE_0:def 4;
then consider i1 be Nat such that
A7: 1 <= i1 and
A8: i1+1 <= len Upper_Seq(C,n) and
A9: x1 in LSeg(Upper_Seq(C,n),i1) by SPPOL_2:13;
A10: LSeg(Upper_Seq(C,n),i1) = LSeg(f,i1) by A8,SPPOL_2:9;
x in L~Lower_Seq(C,n) by A5,XBOOLE_0:def 4;
then consider i2 be Nat such that
A11: 1 <= i2 and
A12: i2+1 <= len Lower_Seq(C,n) and
A13: x1 in LSeg(Lower_Seq(C,n),i2) by SPPOL_2:13;
set i3=i2-'1;
A14: i3+1 = i2 by A11,XREAL_1:235;
then
A15: 1+pE..f <= i3+1+pE..f by A11,XREAL_1:7;
A16: len Lower_Seq(C,n) = len f-pE..f+1 by Th9;
then i2 < len f-pE..f+1 by A12,NAT_1:13;
then i2-1 < len f-pE..f by XREAL_1:19;
then
A17: i2-1+pE..f < len f by XREAL_1:20;
i2-1 >= 1-1 by A11,XREAL_1:9;
then
A18: i3+pE..f < len f by A17,XREAL_0:def 2;
A19: LSeg(Lower_Seq(C,n),i2) = LSeg(f,i3+pE..f) by A1,A14,SPPOL_2:10;
A20: len Upper_Seq(C,n) = pE..f by Th8;
then i1+1 < pE..f+1 by A8,NAT_1:13;
then i1+1 < i3+pE..f+1 by A15,XXREAL_0:2;
then
A21: i1+1 <= i3+pE..f by NAT_1:13;
A22: pE..f-'1+1 = pE..f by A1,FINSEQ_4:21,XREAL_1:235;
i3+1 < len f-pE..f+1 by A12,A14,A16,NAT_1:13;
then i3 < len f-pE..f by XREAL_1:7;
then
A23: i3+pE..f < len f by XREAL_1:20;
then
A24: i3+pE..f+1 <= len f by NAT_1:13;
now
per cases by A7,A21,XXREAL_0:1;
suppose
i1+1 < i3+pE..f & i1 > 1;
then LSeg(f,i1) misses LSeg(f,i3+pE..f) by A23,GOBOARD5:def 4;
then LSeg(f,i1) /\ LSeg(f,i3+pE..f) = {};
hence contradiction by A9,A13,A10,A19,XBOOLE_0:def 4;
end;
suppose
A25: i1 = 1;
i3+pE..f >= 0+3 by A2,A20,XREAL_1:7;
then
A26: i1+1 < i3+pE..f by A25,XXREAL_0:2;
now
per cases by A24,XXREAL_0:1;
suppose
i3+pE..f+1 < len f;
then LSeg(f,i1) misses LSeg(f,i3+pE..f) by A26,GOBOARD5:def 4;
then LSeg(f,i1) /\ LSeg(f,i3+pE..f) = {};
hence contradiction by A9,A13,A10,A19,XBOOLE_0:def 4;
end;
suppose
i3+pE..f+1 = len f;
then i3+pE..f = len f-1;
then i3+pE..f = len f-'1 by XREAL_0:def 2;
then LSeg(f,i1) /\ LSeg(f,i3+pE..f) = {f/.1} by A25,GOBOARD7:34
,REVROT_1:30;
then x1 in {f/.1} by A9,A13,A10,A19,XBOOLE_0:def 4;
then x1 = f/.1 by TARSKI:def 1
.= pW by A4,FINSEQ_6:92;
hence contradiction by A6,TARSKI:def 2;
end;
end;
hence contradiction;
end;
suppose
A27: i1+1 = i3+pE..f;
i3+pE..f >= pE..f by NAT_1:11;
then pE..f < len f by A18,XXREAL_0:2;
then pE..f+1 <= len f by NAT_1:13;
then
A28: pE..f-'1 + (1+1) <= len f by A22;
0+pE..f <= i3+pE..f by XREAL_1:7;
then pE..f = i1+1 by A8,A20,A27,XXREAL_0:1;
then LSeg(f,i1) /\ LSeg(f,i3+(pE..f)) = {f/.(pE..f)} by A7,A22,A27,A28,
TOPREAL1:def 6;
then x1 in {f/.(pE..f)} by A9,A13,A10,A19,XBOOLE_0:def 4;
then x1 = f/.(pE..f) by TARSKI:def 1
.= pE by A1,FINSEQ_5:38;
hence contradiction by A6,TARSKI:def 2;
end;
end;
hence contradiction;
end;
Lower_Seq(C,n)/.(len Lower_Seq(C,n)) = Rotate(Cage(C,n),W-min L~Cage(C,
n))/. (len Rotate(Cage(C,n),W-min L~Cage(C,n))) by A1,FINSEQ_5:54
.= Rotate(Cage(C,n),W-min L~Cage(C,n))/.1 by FINSEQ_6:def 1
.= W-min L~Cage(C,n) by A4,FINSEQ_6:92;
then
A29: W-min L~Cage(C,n) in rng Lower_Seq(C,n) by FINSEQ_6:168;
(E-max L~Cage(C,n))..Rotate(Cage(C,n),W-min L~Cage(C,n)) <= (E-max L~
Cage(C,n))..Rotate(Cage(C,n),W-min L~Cage(C,n));
then
A30: E-max L~Cage(C,n) in rng Lower_Seq(C,n) & E-max L~Cage(C,n) in rng
Upper_Seq (C,n) by A1,FINSEQ_5:46,FINSEQ_6:61;
len Lower_Seq(C,n) >= 3 by Th15;
then
A31: rng Lower_Seq(C,n) c= L~Lower_Seq(C,n) by SPPOL_2:18,XXREAL_0:2;
Upper_Seq(C,n)/.1 = Rotate(Cage(C,n),W-min L~Cage(C,n))/.1 by A1,FINSEQ_5:44
.= W-min L~Cage(C,n) by A4,FINSEQ_6:92;
then
A32: W-min L~Cage(C,n) in rng Upper_Seq(C,n) by FINSEQ_6:42;
thus {W-min L~Cage(C,n),E-max L~Cage(C,n)} c= L~Upper_Seq(C,n) /\ L~
Lower_Seq(C,n)
proof
let x be object;
assume
A33: x in {W-min L~Cage(C,n),E-max L~Cage(C,n)};
per cases by A33,TARSKI:def 2;
suppose
x = W-min L~Cage(C,n);
hence thesis by A31,A3,A32,A29,XBOOLE_0:def 4;
end;
suppose
x = E-max L~Cage(C,n);
hence thesis by A31,A3,A30,XBOOLE_0:def 4;
end;
end;
end;
theorem
for C be compact non vertical non horizontal Subset of TOP-REAL 2
holds Upper_Seq(C,n) is_in_the_area_of Cage(C,n)
proof
let C be compact non vertical non horizontal Subset of TOP-REAL 2;
E-max L~Cage(C,n) in rng Cage(C,n) by SPRECT_2:46;
then E-max L~Cage(C,n) in rng Rotate(Cage(C,n),W-min L~Cage(C,n)) by
FINSEQ_6:90,SPRECT_2:43;
hence thesis by Th1,JORDAN1B:10;
end;
theorem
for C be compact non vertical non horizontal Subset of TOP-REAL 2
holds Lower_Seq(C,n) is_in_the_area_of Cage(C,n)
proof
let C be compact non vertical non horizontal Subset of TOP-REAL 2;
E-max L~Cage(C,n) in rng Cage(C,n) by SPRECT_2:46;
then E-max L~Cage(C,n) in rng Rotate(Cage(C,n),W-min L~Cage(C,n)) by
FINSEQ_6:90,SPRECT_2:43;
hence thesis by Th2,JORDAN1B:10;
end;
theorem
for C be compact connected non vertical non horizontal Subset of
TOP-REAL 2 holds (Cage(C,n)/.2)`2 = N-bound L~Cage(C,n)
proof
let C be compact connected non vertical non horizontal Subset of TOP-REAL 2;
Cage(C,n)/.1 = N-min L~Cage(C,n) by JORDAN9:32;
then Cage(C,n)/.2 in N-most L~Cage(C,n) by SPRECT_2:30;
then (Cage(C,n)/.2)`2 = (N-min L~Cage(C,n))`2 by PSCOMP_1:39;
hence thesis by EUCLID:52;
end;
theorem
for C be compact connected non vertical non horizontal Subset of
TOP-REAL 2 for k be Nat st 1 <= k & k+1 <= len Cage(C,n) & Cage(C,n)
/.k = E-max L~Cage(C,n) holds (Cage(C,n)/.(k+1))`1 = E-bound L~Cage(C,n)
proof
let C be compact connected non vertical non horizontal Subset of TOP-REAL 2;
A1: Cage(C,n) is_sequence_on Gauge(C,n) by JORDAN9:def 1;
A2: len Gauge(C,n) = width Gauge(C,n) by JORDAN8:def 1;
A3: Cage(C,n)/.1 = N-min L~Cage(C,n) by JORDAN9:32;
then 1 < (N-max L~Cage(C,n))..Cage(C,n) by SPRECT_2:69;
then
A4: (E-max L~Cage(C,n))..Cage(C,n) > 1 by A3,SPRECT_2:70,XXREAL_0:2;
let k be Nat;
assume that
A5: 1 <= k and
A6: k+1 <= len Cage(C,n) and
A7: Cage(C,n)/.k = E-max L~Cage(C,n);
A8: k < len Cage(C,n) by A6,NAT_1:13;
then
A9: k in dom Cage(C,n) by A5,FINSEQ_3:25;
then reconsider k9=k-1 as Nat by FINSEQ_3:26;
(E-max L~Cage(C,n))..Cage(C,n) <= k by A7,A9,FINSEQ_5:39;
then
A10: k > 1 by A4,XXREAL_0:2;
then consider i1,j1,i2,j2 be Nat such that
A11: [i1,j1] in Indices Gauge(C,n) and
A12: Cage(C,n)/.k = Gauge(C,n)*(i1,j1) and
A13: [i2,j2] in Indices Gauge(C,n) and
A14: Cage(C,n)/.(k+1) = Gauge(C,n)*(i2,j2) and
A15: i1 = i2 & j1+1 = j2 or i1+1 = i2 & j1 = j2 or i1 = i2+1 & j1 = j2
or i1 = i2 & j1 = j2+1 by A1,A6,JORDAN8:3;
A16: 1 <= i1 by A11,MATRIX_0:32;
A17: k9+1 < len Cage(C,n) by A6,NAT_1:13;
A18: 1 <= j1 by A11,MATRIX_0:32;
A19: j2 <= width Gauge(C,n) by A13,MATRIX_0:32;
A20: i2 <= len Gauge(C,n) by A13,MATRIX_0:32;
A21: j1 <= width Gauge(C,n) by A11,MATRIX_0:32;
Gauge(C,n)*(i1,j1)`1 = E-bound L~Cage(C,n) by A7,A12,EUCLID:52
.= Gauge(C,n)*(len Gauge(C,n),j1)`1 by A18,A21,A2,JORDAN1A:71;
then
A22: i1 >= len Gauge(C,n) by A16,A18,A21,GOBOARD5:3;
k >= 1+1 by A10,NAT_1:13;
then
A23: k9 >= 1+1-1 by XREAL_1:9;
then consider i3,j3,i4,j4 be Nat such that
A24: [i3,j3] in Indices Gauge(C,n) and
A25: Cage(C,n)/.k9 = Gauge(C,n)*(i3,j3) and
A26: [i4,j4] in Indices Gauge(C,n) and
A27: Cage(C,n)/.(k9+1) = Gauge(C,n)*(i4,j4) and
A28: i3 = i4 & j3+1 = j4 or i3+1 = i4 & j3 = j4 or i3 = i4+1 & j3 = j4
or i3 = i4 & j3 = j4+1 by A1,A8,JORDAN8:3;
A29: i1 = i4 by A11,A12,A26,A27,GOBOARD1:5;
A30: j1 = j4 by A11,A12,A26,A27,GOBOARD1:5;
A31: 1 <= j3 by A24,MATRIX_0:32;
A32: j3 <= width Gauge(C,n) by A24,MATRIX_0:32;
A33: i1 <= len Gauge(C,n) by A11,MATRIX_0:32;
then
A34: i1 = len Gauge(C,n) by A22,XXREAL_0:1;
A35: j3 = j4
proof
assume
A36: j3 <> j4;
per cases by A28,A36;
suppose
i3 = i4 & j3+1 = j4;
hence contradiction by A8,A22,A23,A24,A25,A26,A27,A29,JORDAN10:1;
end;
suppose
A37: i3 = i4 & j3 = j4+1;
k9 < len Cage(C,n) by A17,NAT_1:13;
then
Gauge(C,n)*(i3,j3) in E-most L~Cage(C,n) by A34,A23,A25,A29,A31,A32,A37,
JORDAN1A:61;
then
A38: (Gauge(C,n)*(i4,j4+1))`2 <= (Gauge(C,n)*(i4,j4))`2 by A7,A27,A37,
PSCOMP_1:47;
j4 < j4+1 by NAT_1:13;
hence contradiction by A16,A33,A18,A29,A30,A32,A37,A38,GOBOARD5:4;
end;
end;
A39: 1 <= i2 & 1 <= j2 by A13,MATRIX_0:32;
A40: k9+1 = k;
A41: i3 <= len Gauge(C,n) by A24,MATRIX_0:32;
i1 = i2
proof
assume
A42: i1 <> i2;
per cases by A15,A42;
suppose
i1+1 = i2 & j1 = j2;
hence contradiction by A20,A22,NAT_1:13;
end;
suppose
A43: i1 = i2+1 & j1 = j2;
k9+(1+1) <= len Cage(C,n) by A6;
then
A44: LSeg(Cage(C,n),k9) /\ LSeg(Cage(C,n),k) = {Cage(C,n)/.k} by A23,A40,
TOPREAL1:def 6;
Cage(C,n)/.k9 in LSeg(Cage(C,n),k9) & Cage(C,n)/.(k+1) in LSeg(Cage
(C,n),k) by A5,A6,A8,A23,A40,TOPREAL1:21;
then
Cage(C,n)/.(k+1) in {Cage(C,n)/.k} by A14,A22,A25,A28,A29,A30,A41,A35,A43
,A44,NAT_1:13,XBOOLE_0:def 4;
then Cage(C,n)/.(k+1) = Cage(C,n)/.k by TARSKI:def 1;
hence contradiction by A11,A12,A13,A14,A42,GOBOARD1:5;
end;
end;
then Gauge(C,n)*(i1,j1)`1 = Gauge(C,n)*(i2,1)`1 by A16,A33,A18,A21,GOBOARD5:2
.= Gauge(C,n)*(i2,j2)`1 by A20,A39,A19,GOBOARD5:2;
hence thesis by A7,A12,A14,EUCLID:52;
end;
theorem
for C be compact connected non vertical non horizontal Subset of
TOP-REAL 2 for k be Nat st 1 <= k & k+1 <= len Cage(C,n) & Cage(C,n)
/.k = S-max L~Cage(C,n) holds (Cage(C,n)/.(k+1))`2 = S-bound L~Cage(C,n)
proof
let C be compact connected non vertical non horizontal Subset of TOP-REAL 2;
A1: Cage(C,n) is_sequence_on Gauge(C,n) by JORDAN9:def 1;
A2: Cage(C,n)/.1 = N-min L~Cage(C,n) by JORDAN9:32;
then 1 < (N-max L~Cage(C,n))..Cage(C,n) by SPRECT_2:69;
then 1 < (E-max L~Cage(C,n))..Cage(C,n) by A2,SPRECT_2:70,XXREAL_0:2;
then 1 < (E-min L~Cage(C,n))..Cage(C,n) by A2,SPRECT_2:71,XXREAL_0:2;
then
A3: (S-max L~Cage(C,n))..Cage(C,n) > 1 by A2,SPRECT_2:72,XXREAL_0:2;
let k be Nat;
assume that
A4: 1 <= k and
A5: k+1 <= len Cage(C,n) and
A6: Cage(C,n)/.k = S-max L~Cage(C,n);
A7: k < len Cage(C,n) by A5,NAT_1:13;
then
A8: k in dom Cage(C,n) by A4,FINSEQ_3:25;
then reconsider k9=k-1 as Nat by FINSEQ_3:26;
(S-max L~Cage(C,n))..Cage(C,n) <= k by A6,A8,FINSEQ_5:39;
then
A9: k > 1 by A3,XXREAL_0:2;
then consider i1,j1,i2,j2 be Nat such that
A10: [i1,j1] in Indices Gauge(C,n) and
A11: Cage(C,n)/.k = Gauge(C,n)*(i1,j1) and
A12: [i2,j2] in Indices Gauge(C,n) and
A13: Cage(C,n)/.(k+1) = Gauge(C,n)*(i2,j2) and
A14: i1 = i2 & j1+1 = j2 or i1+1 = i2 & j1 = j2 or i1 = i2+1 & j1 = j2
or i1 = i2 & j1 = j2+1 by A1,A5,JORDAN8:3;
A15: 1 <= i1 by A10,MATRIX_0:32;
A16: j2 <= width Gauge(C,n) by A12,MATRIX_0:32;
A17: 1 <= j2 by A12,MATRIX_0:32;
A18: j1 <= width Gauge(C,n) by A10,MATRIX_0:32;
A19: k9+1 < len Cage(C,n) by A5,NAT_1:13;
A20: i1 <= len Gauge(C,n) by A10,MATRIX_0:32;
Gauge(C,n)*(i1,j1)`2 = S-bound L~Cage(C,n) by A6,A11,EUCLID:52
.= Gauge(C,n)*(i1,1)`2 by A15,A20,JORDAN1A:72;
then
A21: j1 <= 1 by A15,A20,A18,GOBOARD5:4;
k >= 1+1 by A9,NAT_1:13;
then
A22: k9 >= 1+1-1 by XREAL_1:9;
then consider i3,j3,i4,j4 be Nat such that
A23: [i3,j3] in Indices Gauge(C,n) and
A24: Cage(C,n)/.k9 = Gauge(C,n)*(i3,j3) and
A25: [i4,j4] in Indices Gauge(C,n) and
A26: Cage(C,n)/.(k9+1) = Gauge(C,n)*(i4,j4) and
A27: i3 = i4 & j3+1 = j4 or i3+1 = i4 & j3 = j4 or i3 = i4+1 & j3 = j4
or i3 = i4 & j3 = j4+1 by A1,A7,JORDAN8:3;
A28: i1 = i4 by A10,A11,A25,A26,GOBOARD1:5;
A29: j1 = j4 by A10,A11,A25,A26,GOBOARD1:5;
A30: 1 <= i3 by A23,MATRIX_0:32;
A31: i3 <= len Gauge(C,n) by A23,MATRIX_0:32;
A32: 1 <= j1 by A10,MATRIX_0:32;
then
A33: j1 = 1 by A21,XXREAL_0:1;
A34: i3 = i4
proof
assume
A35: i3 <> i4;
per cases by A27,A35;
suppose
j3 = j4 & i3+1 = i4;
hence contradiction by A7,A21,A22,A23,A24,A25,A26,A29,JORDAN10:3;
end;
suppose
A36: j3 = j4 & i3 = i4+1;
k9 < len Cage(C,n) by A19,NAT_1:13;
then
Gauge(C,n)*(i3,j3) in S-most L~Cage(C,n) by A33,A22,A24,A29,A30,A31,A36,
JORDAN1A:60;
then
A37: (Gauge(C,n)*(i4+1,j4))`1 <= (Gauge(C,n)*(i4,j4))`1 by A6,A26,A36,
PSCOMP_1:55;
i4 < i4+1 by NAT_1:13;
hence contradiction by A15,A32,A18,A28,A29,A31,A36,A37,GOBOARD5:3;
end;
end;
A38: 1 <= i2 & i2 <= len Gauge(C,n) by A12,MATRIX_0:32;
A39: k9+1 = k;
A40: 1 <= j3 by A23,MATRIX_0:32;
j1 = j2
proof
assume
A41: j1 <> j2;
per cases by A14,A41;
suppose
j1 = j2+1 & i1 = i2;
hence contradiction by A17,A21,NAT_1:13;
end;
suppose
A42: j1+1 = j2 & i1 = i2;
k9+(1+1) <= len Cage(C,n) by A5;
then
A43: LSeg(Cage(C,n),k9) /\ LSeg(Cage(C,n),k) = {Cage(C,n)/.k} by A22,A39,
TOPREAL1:def 6;
Cage(C,n)/.k9 in LSeg(Cage(C,n),k9) & Cage(C,n)/.(k+1) in LSeg(Cage
(C,n),k) by A4,A5,A7,A22,A39,TOPREAL1:21;
then Cage(C,n)/.(k+1) in {Cage(C,n)/.k} by A13,A21,A24,A27,A28,A29,A40
,A34,A42,A43,NAT_1:13,XBOOLE_0:def 4;
then Cage(C,n)/.(k+1) = Cage(C,n)/.k by TARSKI:def 1;
hence contradiction by A10,A11,A12,A13,A41,GOBOARD1:5;
end;
end;
then Gauge(C,n)*(i1,j1)`2 = Gauge(C,n)*(1,j2)`2 by A15,A20,A32,A18,GOBOARD5:1
.= Gauge(C,n)*(i2,j2)`2 by A38,A17,A16,GOBOARD5:1;
hence thesis by A6,A11,A13,EUCLID:52;
end;
theorem
for C be compact connected non vertical non horizontal Subset of
TOP-REAL 2 for k be Nat st 1 <= k & k+1 <= len Cage(C,n) & Cage(C,n)
/.k = W-min L~Cage(C,n) holds (Cage(C,n)/.(k+1))`1 = W-bound L~Cage(C,n)
proof
let C be compact connected non vertical non horizontal Subset of TOP-REAL 2;
A1: Cage(C,n) is_sequence_on Gauge(C,n) by JORDAN9:def 1;
A2: Cage(C,n)/.1 = N-min L~Cage(C,n) by JORDAN9:32;
then 1 < (N-max L~Cage(C,n))..Cage(C,n) by SPRECT_2:69;
then 1 < (E-max L~Cage(C,n))..Cage(C,n) by A2,SPRECT_2:70,XXREAL_0:2;
then 1 < (E-min L~Cage(C,n))..Cage(C,n) by A2,SPRECT_2:71,XXREAL_0:2;
then 1 < (S-max L~Cage(C,n))..Cage(C,n) by A2,SPRECT_2:72,XXREAL_0:2;
then 1 < (S-min L~Cage(C,n))..Cage(C,n) by A2,SPRECT_2:73,XXREAL_0:2;
then
A3: (W-min L~Cage(C,n))..Cage(C,n) > 1 by A2,SPRECT_2:74,XXREAL_0:2;
let k be Nat;
assume that
A4: 1 <= k and
A5: k+1 <= len Cage(C,n) and
A6: Cage(C,n)/.k = W-min L~Cage(C,n);
A7: k < len Cage(C,n) by A5,NAT_1:13;
then
A8: k in dom Cage(C,n) by A4,FINSEQ_3:25;
then reconsider k9=k-1 as Nat by FINSEQ_3:26;
(W-min L~Cage(C,n))..Cage(C,n) <= k by A6,A8,FINSEQ_5:39;
then
A9: k > 1 by A3,XXREAL_0:2;
then consider i1,j1,i2,j2 be Nat such that
A10: [i1,j1] in Indices Gauge(C,n) and
A11: Cage(C,n)/.k = Gauge(C,n)*(i1,j1) and
A12: [i2,j2] in Indices Gauge(C,n) and
A13: Cage(C,n)/.(k+1) = Gauge(C,n)*(i2,j2) and
A14: i1 = i2 & j1+1 = j2 or i1+1 = i2 & j1 = j2 or i1 = i2+1 & j1 = j2
or i1 = i2 & j1 = j2+1 by A1,A5,JORDAN8:3;
A15: i1 <= len Gauge(C,n) by A10,MATRIX_0:32;
A16: j2 <= width Gauge(C,n) by A12,MATRIX_0:32;
A17: 1 <= i2 by A12,MATRIX_0:32;
A18: j1 <= width Gauge(C,n) by A10,MATRIX_0:32;
A19: len Gauge(C,n) = width Gauge(C,n) by JORDAN8:def 1;
A20: i2 <= len Gauge(C,n) & 1 <= j2 by A12,MATRIX_0:32;
A21: k9+1 = k;
A22: k9+1 < len Cage(C,n) by A5,NAT_1:13;
A23: 1 <= j1 by A10,MATRIX_0:32;
Gauge(C,n)*(i1,j1)`1 = W-bound L~Cage(C,n) by A6,A11,EUCLID:52
.= Gauge(C,n)*(1,j1)`1 by A23,A18,A19,JORDAN1A:73;
then
A24: i1 <= 1 by A15,A23,A18,GOBOARD5:3;
k >= 1+1 by A9,NAT_1:13;
then
A25: k9 >= 1+1-1 by XREAL_1:9;
then consider i3,j3,i4,j4 be Nat such that
A26: [i3,j3] in Indices Gauge(C,n) and
A27: Cage(C,n)/.k9 = Gauge(C,n)*(i3,j3) and
A28: [i4,j4] in Indices Gauge(C,n) and
A29: Cage(C,n)/.(k9+1) = Gauge(C,n)*(i4,j4) and
A30: i3 = i4 & j3+1 = j4 or i3+1 = i4 & j3 = j4 or i3 = i4+1 & j3 = j4
or i3 = i4 & j3 = j4+1 by A1,A7,JORDAN8:3;
A31: i1 = i4 by A10,A11,A28,A29,GOBOARD1:5;
A32: j1 = j4 by A10,A11,A28,A29,GOBOARD1:5;
A33: j3 <= width Gauge(C,n) by A26,MATRIX_0:32;
A34: 1 <= j3 by A26,MATRIX_0:32;
A35: 1 <= i1 by A10,MATRIX_0:32;
then
A36: i1 = 1 by A24,XXREAL_0:1;
A37: j3 = j4
proof
assume
A38: j3 <> j4;
per cases by A30,A38;
suppose
i3 = i4 & j3 = j4+1;
hence contradiction by A7,A24,A25,A26,A27,A28,A29,A31,JORDAN10:2;
end;
suppose
A39: i3 = i4 & j3+1 = j4;
k9 < len Cage(C,n) by A22,NAT_1:13;
then
Gauge(C,n)*(i3,j3) in W-most L~Cage(C,n) by A36,A25,A27,A31,A34,A33,A39,
JORDAN1A:59;
then
A40: (Gauge(C,n)*(i3,j3+1))`2 <= (Gauge(C,n)*(i3,j3))`2 by A6,A29,A39,
PSCOMP_1:31;
j3 < j3+1 by NAT_1:13;
hence contradiction by A35,A15,A18,A31,A32,A34,A39,A40,GOBOARD5:4;
end;
end;
A41: 1 <= i3 by A26,MATRIX_0:32;
i1 = i2
proof
assume
A42: i1 <> i2;
per cases by A14,A42;
suppose
i1 = i2+1 & j1 = j2;
hence contradiction by A17,A24,NAT_1:13;
end;
suppose
A43: i1+1 = i2 & j1 = j2;
k9+(1+1) <= len Cage(C,n) by A5;
then
A44: LSeg(Cage(C,n),k9) /\ LSeg(Cage(C,n),k) = {Cage(C,n)/.k} by A25,A21,
TOPREAL1:def 6;
Cage(C,n)/.k9 in LSeg(Cage(C,n),k9) & Cage(C,n)/.(k+1) in LSeg(Cage
(C,n),k) by A4,A5,A7,A25,A21,TOPREAL1:21;
then Cage(C,n)/.(k+1) in {Cage(C,n)/.k} by A13,A24,A27,A30,A31,A32,A41
,A37,A43,A44,NAT_1:13,XBOOLE_0:def 4;
then Cage(C,n)/.(k+1) = Cage(C,n)/.k by TARSKI:def 1;
hence contradiction by A10,A11,A12,A13,A42,GOBOARD1:5;
end;
end;
then Gauge(C,n)*(i1,j1)`1 = Gauge(C,n)*(i2,1)`1 by A35,A15,A23,A18,GOBOARD5:2
.= Gauge(C,n)*(i2,j2)`1 by A17,A20,A16,GOBOARD5:2;
hence thesis by A6,A11,A13,EUCLID:52;
end;