:: Some Properties of Cells and Arcs
:: by Robert Milewski , Andrzej Trybulec , Artur Korni{\l}owicz
:: and Adam Naumowicz
::
:: Received October 6, 2000
:: Copyright (c) 2000-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, RCOMP_1, SPPOL_1, SUBSET_1, EUCLID, RELAT_2, GOBOARD1,
PRE_TOPC, FINSEQ_1, XBOOLE_0, FINSEQ_5, XXREAL_0, JORDAN3, RELAT_1,
TOPREAL1, FUNCT_1, GROUP_2, ORDINAL4, ARYTM_3, TOPREAL2, PSCOMP_1,
ARYTM_1, PARTFUN1, CARD_1, NAT_1, RLTOPSP1, MCART_1, SPRECT_2, FINSEQ_6,
FINSEQ_4, ZFMISC_1, JORDAN1A, INT_1, JORDAN8, NEWTON, TARSKI, GOBOARD5,
TREES_1, REAL_1, JORDAN2C, JORDAN9, JORDAN6, COMPLEX1, CONNSP_1, SEQ_4,
XXREAL_2;
notations TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, XXREAL_0,
XREAL_0, REAL_1, COMPLEX1, INT_1, NAT_1, NAT_D, FUNCT_1, PARTFUN1,
FINSEQ_1, FINSEQ_4, NEWTON, FINSEQ_5, MATRIX_0, ZFMISC_1, FINSEQ_6,
STRUCT_0, PRE_TOPC, TOPREAL2, CONNSP_1, COMPTS_1, RLTOPSP1, EUCLID,
PSCOMP_1, SPRECT_2, GOBOARD1, TOPREAL1, GOBOARD5, SPPOL_1, JORDAN3,
JORDAN8, JORDAN2C, JORDAN6, JORDAN9, JORDAN1A;
constructors REAL_1, SQUARE_1, NAT_D, FINSEQ_4, NEWTON, RFINSEQ, FINSEQ_5,
CONNSP_1, MONOID_0, GOBOARD1, PSCOMP_1, JORDAN3, JORDAN6, JORDAN2C,
JORDAN8, JORDAN9, JORDAN1A, CONVEX1, RELSET_1;
registrations XBOOLE_0, XXREAL_0, XREAL_0, NAT_1, INT_1, FINSEQ_1, FINSEQ_5,
STRUCT_0, MONOID_0, EUCLID, TOPREAL2, TOPREAL5, SPRECT_2, TOPREAL6,
JORDAN8, FUNCT_1, RELAT_1, RLTOPSP1, SPPOL_2, JORDAN2C, ORDINAL1, NEWTON;
requirements NUMERALS, BOOLE, SUBSET, REAL, ARITHM;
definitions TARSKI;
expansions TARSKI;
theorems EUCLID, GOBRD11, JORDAN8, NEWTON, PSCOMP_1, JORDAN1A, NAT_1,
TOPREAL6, GOBOARD5, NAT_2, FINSEQ_1, FINSEQ_2, JORDAN6,
SPRECT_2, FINSEQ_4, FINSEQ_5, FINSEQ_6, GOBOARD9, SPPOL_1, SPPOL_2,
REVROT_1, TOPREAL1, SPRECT_3, BOOLMARK, JORDAN3, JORDAN2C, SUBSET_1,
JGRAPH_1, ABSVALUE, TOPREAL5, FINSEQ_3, XBOOLE_0, XBOOLE_1, PEPIN,
XREAL_1, XXREAL_0, INT_1, NAT_D, ORDINAL1, XREAL_0, RLTOPSP1, MATRIX_0;
begin
reserve E for compact non vertical non horizontal Subset of TOP-REAL 2,
C for compact connected non vertical non horizontal Subset of TOP-REAL 2,
G for Go-board,
i, j, m, n for Nat,
p for Point of TOP-REAL 2;
theorem
for f being FinSequence holds f is empty iff Rev f is empty
proof
let f be FinSequence;
thus f is empty implies Rev f is empty;
assume Rev f is empty;
then reconsider g=Rev f as empty FinSequence;
Rev g is empty;
hence thesis;
end;
theorem
for D being non empty set, f being FinSequence of D for i,j st 1 <= i
& i <= len f & 1 <= j & j <= len f holds mid(f,i,j) is non empty
proof
let D be non empty set, f be FinSequence of D;
let i,j;
assume that
A1: 1 <= i and
A2: i <= len f and
A3: 1 <= j and
A4: j <= len f;
A5: j in dom f by A3,A4,FINSEQ_3:25;
i in dom f by A1,A2,FINSEQ_3:25;
hence thesis by A5,SPRECT_2:7;
end;
theorem Th3:
for f be FinSequence of TOP-REAL 2 for p be Point of TOP-REAL 2
st 1 <= len f & p in L~f holds R_Cut(f,p).1 = f.1
proof
let f be FinSequence of TOP-REAL 2;
let p be Point of TOP-REAL 2;
assume that
A1: 1 <= len f and
A2: p in L~f;
A3: 1 <= Index(p,f) by A2,JORDAN3:8;
A4: 1 in dom f by A1,FINSEQ_3:25;
now
per cases;
suppose
p<>f.1;
then
A5: R_Cut(f,p) = mid(f,1,Index(p,f))^<*p*> by JORDAN3:def 4;
A6: Index(p,f) < len f by A2,JORDAN3:8;
then Index(p,f) in dom f by A3,FINSEQ_3:25;
then len mid(f,1,Index(p,f)) >= 1 by A4,SPRECT_2:5;
hence R_Cut(f,p).1 = mid(f,1,Index(p,f)).1 by A5,FINSEQ_6:109
.= f.1 by A1,A3,A6,FINSEQ_6:118;
end;
suppose
A7: p = f.1;
then R_Cut(f,p) = <*p*> by JORDAN3:def 4;
hence thesis by A7;
end;
end;
hence thesis;
end;
theorem
for f be FinSequence of TOP-REAL 2 for p be Point of TOP-REAL 2 st f
is being_S-Seq & p in L~f holds L_Cut(f,p).(len L_Cut(f,p)) = f.(len f)
proof
let f be FinSequence of TOP-REAL 2;
let p be Point of TOP-REAL 2 such that
A1: f is being_S-Seq and
A2: p in L~f;
Rev f is being_S-Seq by A1;
then
A3: 2 <= len Rev f by TOPREAL1:def 8;
A4: p in L~Rev f by A2,SPPOL_2:22;
then L_Cut(Rev Rev f,p) = Rev R_Cut(Rev f,p) by A1,JORDAN3:22;
hence L_Cut(f,p).(len L_Cut(f,p)) = Rev R_Cut(Rev f,p).(len R_Cut(Rev f,p))
by FINSEQ_5:def 3
.= R_Cut(Rev f,p).1 by FINSEQ_5:62
.= Rev f.1 by A4,A3,Th3,XXREAL_0:2
.= f.(len f) by FINSEQ_5:62;
end;
theorem
for P be Simple_closed_curve holds W-max(P) <> E-max(P)
proof
let P be Simple_closed_curve;
now
A1: |[E-bound P, upper_bound (proj2|E-most P)]|=E-max(P) by PSCOMP_1:def 23;
A2: |[W-bound P, upper_bound (proj2|W-most P)]|=W-max(P) by PSCOMP_1:def 20;
assume W-max(P) = E-max(P);
then W-bound P= E-bound P by A2,A1,SPPOL_2:1;
hence contradiction by TOPREAL5:17;
end;
hence thesis;
end;
theorem
for D be non empty set for f be FinSequence of D st 1 <= i & i < len f
holds mid(f,i,len f-'1)^<*f/.(len f)*> = mid(f,i,len f)
proof
let D be non empty set;
let f be FinSequence of D;
assume that
A1: 1 <= i and
A2: i < len f;
A3: i+1 <= len f by A2,NAT_1:13;
then
A4: i+1-1 <= len f-1 by XREAL_1:9;
then
A5: i <= len f-'1 by XREAL_0:def 2;
0+i <= len f-1 by A4;
then len f-1-i >= 0 by XREAL_1:19;
then
A6: len f-'1-i >= 0 by A4,XREAL_0:def 2;
A7: len f-i >= 0 by A3,XREAL_1:19;
len f <= len f+1 by NAT_1:11;
then len f-1 <= len f+1-1 by XREAL_1:9;
then
A8: len f-'1 <= len f by XREAL_0:def 2;
then
A9: len mid(f,i,len f-'1) + 1 = len f-'1-'i+1+1 by A1,A5,FINSEQ_6:186
.= len f-'1-i+1+1 by A6,XREAL_0:def 2
.= len f-1-i+1+1 by A4,XREAL_0:def 2
.= len f-'i+1 by A7,XREAL_0:def 2
.= len mid(f,i,len f) by A1,A2,FINSEQ_6:186;
A10: now
1 < len f by A1,A2,XXREAL_0:2;
then len f in Seg len f by FINSEQ_1:1;
then
A11: len f in dom f by FINSEQ_1:def 3;
i in Seg len f by A1,A2,FINSEQ_1:1;
then
A12: i in dom f by FINSEQ_1:def 3;
let j be Nat;
assume that
A13: 1 <= j and
A14: j <= len mid(f,i,len f);
per cases by A14,XXREAL_0:1;
suppose
j < len mid(f,i,len f);
then
A15: j <= len mid(f,i,len f-'1) by A9,NAT_1:13;
then j in Seg len mid(f,i,len f-'1) by A13,FINSEQ_1:1;
then
A16: j in dom mid(f,i,len f-'1) by FINSEQ_1:def 3;
1 <= len f-'1 by A1,A5,XXREAL_0:2;
then len f-'1 in Seg len f by A8,FINSEQ_1:1;
then
A17: len f-'1 in dom f by FINSEQ_1:def 3;
j in Seg len mid(f,i,len f) by A13,A14,FINSEQ_1:1;
then
A18: j in dom mid(f,i,len f) by FINSEQ_1:def 3;
j in NAT by ORDINAL1:def 12;
hence
(mid(f,i,len f-'1)^<*f/.(len f)*>)/.j = mid(f,i,len f-'1)/.j by A13,A15,
BOOLMARK:7
.= f/.(j+i-'1) by A5,A12,A16,A17,SPRECT_2:3
.= mid(f,i,len f)/.j by A2,A12,A11,A18,SPRECT_2:3;
end;
suppose
A19: j = len mid(f,i,len f);
hence (mid(f,i,len f-'1)^<*f/.(len f)*>)/.j = f/.(len f) by A9,
FINSEQ_4:67
.= mid(f,i,len f)/.j by A12,A11,A19,SPRECT_2:9;
end;
end;
len (mid(f,i,len f-'1)^<*f/.(len f)*>) = len mid(f,i,len f-'1) + 1 by
FINSEQ_2:16;
hence thesis by A9,A10,FINSEQ_5:13;
end;
theorem
for p,q be Point of TOP-REAL 2 st p <> q & LSeg(p,q) is vertical holds
<*p,q*> is being_S-Seq
proof
let p,q be Point of TOP-REAL 2;
assume that
A1: p <> q and
A2: LSeg(p,q) is vertical;
p`1 = q`1 by A2,SPPOL_1:16;
hence thesis by A1,SPPOL_2:43;
end;
theorem
for p,q be Point of TOP-REAL 2 st p <> q & LSeg(p,q) is horizontal
holds <*p,q*> is being_S-Seq
proof
let p,q be Point of TOP-REAL 2;
assume that
A1: p <> q and
A2: LSeg(p,q) is horizontal;
p`2 = q`2 by A2,SPPOL_1:15;
hence thesis by A1,SPPOL_2:43;
end;
theorem Th9:
for p,q be FinSequence of TOP-REAL 2 for v be Point of TOP-REAL
2 st p is_in_the_area_of q holds Rotate(p,v) is_in_the_area_of q
proof
let p,q be FinSequence of TOP-REAL 2;
let v be Point of TOP-REAL 2;
assume
A1: p is_in_the_area_of q;
per cases;
suppose
A2: v in rng p;
now
let n;
assume n in dom Rotate(p,v);
then n in dom p by FINSEQ_6:180;
then
A3: n in Seg len p by FINSEQ_1:def 3;
then
A4: n <= len p by FINSEQ_1:1;
A5: 0+1 <= n by A3,FINSEQ_1:1;
then
A6: n-1 >= 0 by XREAL_1:19;
per cases;
suppose
A7: n <= len(p:-v);
then n <= len p-v..p+1 by A2,FINSEQ_5:50;
then n-1 <= len p-v..p by XREAL_1:20;
then n-1+v..p <= len p by XREAL_1:19;
then
A8: n-'1+v..p <= len p by A6,XREAL_0:def 2;
1 <= v..p by A2,FINSEQ_4:21;
then 0+1 <= n-'1+v..p by XREAL_1:7;
then n-'1+v..p in Seg len p by A8,FINSEQ_1:1;
then
A9: n-'1+v..p in dom p by FINSEQ_1:def 3;
A10: Rotate(p,v)/.n = p/.(n-'1+v..p) by A2,A5,A7,FINSEQ_6:174;
hence W-bound L~q <= (Rotate(p,v)/.n)`1 by A1,A9,SPRECT_2:def 1;
thus (Rotate(p,v)/.n)`1 <= E-bound L~q by A1,A10,A9,SPRECT_2:def 1;
thus S-bound L~q <= (Rotate(p,v)/.n)`2 by A1,A10,A9,SPRECT_2:def 1;
thus (Rotate(p,v)/.n)`2 <= N-bound L~q by A1,A10,A9,SPRECT_2:def 1;
end;
suppose
A11: n > len(p:-v);
then n > len p-v..p+1 by A2,FINSEQ_5:50;
then n > 1+len p-v..p;
then n+v..p > 1+len p by XREAL_1:19;
then n+v..p-len p > 1 by XREAL_1:20;
then
A12: 1 <= n+v..p-'len p by XREAL_0:def 2;
v..p <= len p by A2,FINSEQ_4:21;
then n+v..p <= len p+len p by A4,XREAL_1:7;
then n+v..p-len p <= len p by XREAL_1:20;
then n+v..p-'len p <= len p by XREAL_0:def 2;
then n+v..p-'len p in Seg len p by A12,FINSEQ_1:1;
then
A13: n+v..p-'len p in dom p by FINSEQ_1:def 3;
A14: Rotate(p,v)/.n = p/.(n+v..p-'len p) by A2,A4,A11,FINSEQ_6:177;
hence W-bound L~q <= (Rotate(p,v)/.n)`1 by A1,A13,SPRECT_2:def 1;
thus (Rotate(p,v)/.n)`1 <= E-bound L~q by A1,A14,A13,SPRECT_2:def 1;
thus S-bound L~q <= (Rotate(p,v)/.n)`2 by A1,A14,A13,SPRECT_2:def 1;
thus (Rotate(p,v)/.n)`2 <= N-bound L~q by A1,A14,A13,SPRECT_2:def 1;
end;
end;
hence thesis by SPRECT_2:def 1;
end;
suppose
not v in rng p;
hence thesis by A1,FINSEQ_6:def 2;
end;
end;
theorem
for p be non trivial FinSequence of TOP-REAL 2 for v be Point of
TOP-REAL 2 holds Rotate(p,v) is_in_the_area_of p by Th9,SPRECT_2:21;
theorem Th11:
for f be FinSequence holds Center f >= 1
proof
let f be FinSequence;
len f div 2 + 1 >= 0+1 by XREAL_1:6;
hence thesis by JORDAN1A:def 1;
end;
theorem
for f be FinSequence st len f >= 1 holds Center f <= len f
proof
let f be FinSequence;
assume len f >= 1;
then 0 + len f < len f + len f by XREAL_1:6;
then len f+1 <= 2*len f by NAT_1:13;
then (len f+1+1) div 2 <= len f by NAT_2:25;
then (len f+(1+1)) div 2 <= len f;
then len f div 2+1 <= len f by NAT_2:14;
hence thesis by JORDAN1A:def 1;
end;
theorem Th13:
Center G <= len G
proof
0 < len G by GOBRD11:34;
then
A1: len G div (2 qua Integer) < len G by INT_1:56;
Center G = len G div 2 + 1 by JORDAN1A:def 1;
hence thesis by A1,NAT_1:13;
end;
theorem Th14:
for f be FinSequence st len f >= 2 holds Center f > 1
proof
let f be FinSequence;
assume len f >= 2;
then len f div 2 >= 1 by NAT_2:13;
then len f div 2 + 1 > 1 by NAT_1:13;
hence thesis by JORDAN1A:def 1;
end;
theorem Th15:
for f be FinSequence st len f >= 3 holds Center f < len f
proof
let f be FinSequence;
assume len f >= 3;
then len f+(2+1) <= len f+len f by XREAL_1:6;
then len f+2+1 <= 2*len f;
then (len f+2+1+1) div 2 <= len f by NAT_2:25;
then (len f+2+(1+1)) div 2 <= len f;
then (len f+2) div 2+1 <= len f by NAT_2:14;
then (len f+2) div 2 < len f by NAT_1:13;
then len f div 2 + 1 < len f by NAT_2:14;
hence thesis by JORDAN1A:def 1;
end;
Lm1: now
let E be non empty Subset of TOP-REAL 2;
thus len Gauge(E,0)-'1 = 2|^0 + 3 -' 1 by JORDAN8:def 1
.= 1+3-'1 by NEWTON:4
.= 3 by NAT_D:34;
end;
theorem
Center Gauge(E,n) = 2|^(n-'1) + 2
proof
reconsider n as Nat;
set G = Gauge(E,n);
per cases;
suppose
A1: n = 0;
A2: 4 = 2 * 2 + 0;
A3: 0-1 < 0;
Center G = len G div 2 + 1 by JORDAN1A:def 1;
then Center G = (2|^0 + 3) div 2 + 1 by A1,JORDAN8:def 1
.= (1+3) div 2 + 1 by NEWTON:4
.= 1 + 1 + 1 by A2
.= 2|^0 + 1 + 1 by NEWTON:4
.= 2|^(0-'1) + 1 + 1 by A3,XREAL_0:def 2
.= 2|^(n-'1) + 2 by A1;
hence thesis;
end;
suppose
A4: n > 0;
then
A5: 0+1 <= n by NAT_1:13;
A6: 2|^n div 2 = 2|^n / 2 by A4,PEPIN:64
.= 2|^n / 2|^1
.= 2|^(n-'1) by A5,TOPREAL6:10;
3 = 2 * 1 + 1;
then
A7: 3 div 2 = 1 by NAT_D:def 1;
A8: 2|^n mod 2 = 0 by A4,PEPIN:36;
len G div 2 + 1 = (2|^n + 3) div 2 + 1 by JORDAN8:def 1
.= (2|^n div 2) + (3 div 2) + 1 by A8,NAT_D:19
.= (2|^n div 2) + (1 + 1) by A7;
hence thesis by A6,JORDAN1A:def 1;
end;
end;
theorem Th17:
E c= cell(Gauge(E,0),2,2)
proof
set G = Gauge(E,0);
let x be object;
A1: len G = width G by JORDAN8:def 1;
assume
A2: x in E;
then reconsider x as Point of TOP-REAL 2;
A3: 4 <= len G by JORDAN8:10;
then
A4: 1 < len G by XXREAL_0:2;
then G*(1,2)`2 = S-bound E by JORDAN8:13;
then
A5: G*(1,2)`2 <= x`2 by A2,PSCOMP_1:24;
2 < len G by A3,XXREAL_0:2;
then
A6: cell(G,2,2) = { |[p,q]| where p, q is Real:
G*(2,1)`1 <= p & p <= G*(2+
1,1)`1 & G*(1,2)`2 <= q & q <= G*(1,2+1)`2 } by A1,GOBRD11:32;
G*(2,1)`1 = W-bound E by A4,JORDAN8:11;
then
A7: G*(2,1)`1 <= x`1 by A2,PSCOMP_1:24;
A8: len G-'1 = 3 by Lm1;
then G*(2+1,1)`1 = E-bound E by A4,JORDAN8:12;
then
A9: x`1 <= G*(2+1,1)`1 by A2,PSCOMP_1:24;
G*(1,2+1)`2 = N-bound E by A8,A4,JORDAN8:14;
then
A10: x`2 <= G*(1,2+1)`2 by A2,PSCOMP_1:24;
x = |[x`1,x`2]| by EUCLID:53;
hence thesis by A7,A9,A5,A10,A6;
end;
theorem Th18:
not cell(Gauge(E,0),2,2) c= BDD E
proof
assume
A1: cell(Gauge(E,0),2,2) c= BDD E;
E c= cell(Gauge(E,0),2,2) by Th17;
then
A2: E c= BDD E by A1;
set e = the Element of E;
A3: BDD E misses E by JORDAN1A:7;
e in E;
hence thesis by A2,A3,XBOOLE_0:3;
end;
theorem
Gauge(C,1)*(Center Gauge(C,1),1) = |[(W-bound C + E-bound C)/2,S-bound
L~Cage(C,1)]|
proof
set G = Gauge(C,1);
1 <= len G by GOBRD11:34;
then
A1: G*(Center G,1)`1 = (W-bound C + E-bound C) / 2 by JORDAN1A:38;
Center G <= len G by Th13;
then G*(Center G,1)`2 = S-bound L~Cage(C,1) by Th11,JORDAN1A:72;
hence thesis by A1,EUCLID:53;
end;
theorem
Gauge(C,1)*(Center Gauge(C,1),len Gauge(C,1)) = |[(W-bound C + E-bound
C)/2,N-bound L~Cage(C,1)]|
proof
set G = Gauge(C,1);
1 <= len G by GOBRD11:34;
then
A1: G*(Center G,len G)`1 = (W-bound C + E-bound C) / 2 by JORDAN1A:38;
1 <= Center G by Th11;
then G*(Center G,len G)`2 = N-bound L~Cage(C,1) by Th13,JORDAN1A:70;
hence thesis by A1,EUCLID:53;
end;
Lm2: i <= m & m <= i+1 implies i = m or i = m -' 1
proof
assume that
A1: i <= m and
A2: m <= i+1 and
A3: i <> m;
i < m by A1,A3,XXREAL_0:1;
then i+1 <= m by NAT_1:13;
then m = i+1 by A2,XXREAL_0:1;
hence thesis by NAT_D:34;
end;
theorem Th21:
1 <= j & j < width G & 1 <= m & m <= len G & 1 <= n & n <= width
G & p in cell(G,len G,j) & p`1 = G*(m,n)`1 implies len G = m
proof
assume that
A1: 1 <= j and
A2: j < width G and
A3: 1 <= m and
A4: m <= len G and
A5: 1 <= n and
A6: n <= width G and
A7: p in cell(G,len G,j) and
A8: p`1 = G*(m,n)`1;
A9: G*(m,1)`1 = G*(m,n)`1 by A3,A4,A5,A6,GOBOARD5:2;
A10: cell(G,len G,j) = { |[r,s]| where r, s is Real:
G*(len G,1)`1 <= r & G*
(1,j)`2 <= s & s <= G*(1,j+1)`2 } by A1,A2,GOBRD11:29;
A11: 1 <= width G by A1,A2,XXREAL_0:2;
consider r, s being Real such that
A12: p = |[r,s]| and
A13: G*(len G,1)`1 <= r and
G*(1,j)`2 <= s and
s <= G*(1,j+1)`2 by A7,A10;
p`1 = r by A12,EUCLID:52;
then len G <= m by A3,A8,A11,A9,A13,GOBOARD5:3;
hence thesis by A4,XXREAL_0:1;
end;
theorem
1 <= i & i <= len G & 1 <= j & j < width G & 1 <= m & m <= len G & 1
<= n & n <= width G & p in cell(G,i,j) & p`1 = G*(m,n)`1 implies i = m or i = m
-' 1
proof
assume that
A1: 1 <= i and
A2: i <= len G and
A3: 1 <= j and
A4: j < width G and
A5: 1 <= m and
A6: m <= len G and
A7: 1 <= n and
A8: n <= width G and
A9: p in cell(G,i,j) and
A10: p`1 = G*(m,n)`1;
A11: G*(m,1)`1 = G*(m,n)`1 by A5,A6,A7,A8,GOBOARD5:2;
A12: 1 <= width G by A3,A4,XXREAL_0:2;
per cases by A2,XXREAL_0:1;
suppose
i = len G;
hence thesis by A3,A4,A5,A6,A7,A8,A9,A10,Th21;
end;
suppose
i < len G;
then
cell(G,i,j) = { |[r,s]| where r, s is Real:
G*(i,1)`1 <= r & r <= G*(
i+1,1)`1 & G*(1,j)`2 <= s & s <= G*(1,j+1)`2 } by A1,A3,A4,GOBRD11:32;
then consider r, s being Real such that
A13: p = |[r,s]| and
A14: G*(i,1)`1 <= r and
A15: r <= G*(i+1,1)`1 and
G*(1,j)`2 <= s and
s <= G*(1,j+1)`2 by A9;
A16: p`1 = r by A13,EUCLID:52;
i <= m & m <= i+1
proof
assume
A17: not thesis;
per cases by A17;
suppose
i > m;
hence contradiction by A2,A5,A10,A12,A11,A14,A16,GOBOARD5:3;
end;
suppose
A18: m > i+1;
1 <= i+1 by NAT_1:11;
hence contradiction by A6,A10,A12,A11,A15,A16,A18,GOBOARD5:3;
end;
end;
hence thesis by Lm2;
end;
end;
theorem Th23:
1 <= i & i < len G & 1 <= m & m <= len G & 1 <= n & n <= width G
& p in cell(G,i,width G) & p`2 = G*(m,n)`2 implies width G = n
proof
assume that
A1: 1 <= i and
A2: i < len G and
A3: 1 <= m and
A4: m <= len G and
A5: 1 <= n and
A6: n <= width G and
A7: p in cell(G,i,width G) and
A8: p`2 = G*(m,n)`2;
A9: G*(1,n)`2 = G*(m,n)`2 by A3,A4,A5,A6,GOBOARD5:1;
A10: cell(G,i,width G) = { |[r,s]| where r, s is Real:
G*(i,1)`1 <= r & r <=
G*(i+1,1)`1 & G*(1,width G)`2 <= s } by A1,A2,GOBRD11:31;
A11: 1 <= len G by A1,A2,XXREAL_0:2;
consider r, s being Real such that
A12: p = |[r,s]| and
G*(i,1)`1 <= r and
r <= G*(i+1,1)`1 and
A13: G*(1,width G)`2 <= s by A7,A10;
p`2 = s by A12,EUCLID:52;
then width G <= n by A5,A8,A11,A9,A13,GOBOARD5:4;
hence thesis by A6,XXREAL_0:1;
end;
theorem
1 <= i & i < len G & 1 <= j & j <= width G & 1 <= m & m <= len G & 1
<= n & n <= width G & p in cell(G,i,j) & p`2 = G*(m,n)`2 implies j = n or j = n
-' 1
proof
assume that
A1: 1 <= i and
A2: i < len G and
A3: 1 <= j and
A4: j <= width G and
A5: 1 <= m and
A6: m <= len G and
A7: 1 <= n and
A8: n <= width G and
A9: p in cell(G,i,j) and
A10: p`2 = G*(m,n)`2;
A11: G*(1,n)`2 = G*(m,n)`2 by A5,A6,A7,A8,GOBOARD5:1;
A12: 1 <= len G by A1,A2,XXREAL_0:2;
per cases by A4,XXREAL_0:1;
suppose
j = width G;
hence thesis by A1,A2,A5,A6,A7,A8,A9,A10,Th23;
end;
suppose
j < width G;
then
cell(G,i,j) = { |[r,s]| where r, s is Real:
G*(i,1)`1 <= r & r <= G*(
i+1,1)`1 & G*(1,j)`2 <= s & s <= G*(1,j+1)`2 } by A1,A2,A3,GOBRD11:32;
then consider r, s being Real such that
A13: p = |[r,s]| and
G*(i,1)`1 <= r and
r <= G*(i+1,1)`1 and
A14: G*(1,j)`2 <= s and
A15: s <= G*(1,j+1)`2 by A9;
A16: p`2 = s by A13,EUCLID:52;
j <= n & n <= j+1
proof
assume
A17: not thesis;
per cases by A17;
suppose
j > n;
hence contradiction by A4,A7,A10,A12,A11,A14,A16,GOBOARD5:4;
end;
suppose
A18: n > j+1;
1 <= j+1 by NAT_1:11;
hence contradiction by A8,A10,A12,A11,A15,A16,A18,GOBOARD5:4;
end;
end;
hence thesis by Lm2;
end;
end;
theorem Th25:
for C be Simple_closed_curve for i be Nat st 1 < i &
i < len Gauge(C,n) holds LSeg(Gauge(C,n)*(i,1),Gauge(C,n)*(i,len Gauge(C,n)))
meets Upper_Arc C
proof
let C be Simple_closed_curve;
let i be Nat;
assume that
A1: 1 < i and
A2: i < len Gauge(C,n);
set r = (Gauge(C,n)*(i,2))`1;
4 <= len Gauge(C,n) by JORDAN8:10;
then
A3: 1+1 <= len Gauge(C,n) by XXREAL_0:2;
then 1 <= len Gauge(C,n)-1 by XREAL_1:19;
then
A4: 1 <= len Gauge(C,n)-'1 by XREAL_0:def 2;
A5: len Gauge(C,n) = width Gauge(C,n) by JORDAN8:def 1;
then
A6: Gauge(C,n)*(i,2) in LSeg(Gauge(C,n)*(i,1),Gauge(C,n)*(i,len Gauge(C,n))
) by A1,A2,A3,JORDAN1A:16;
A7: len Gauge(C,n)-'1 <= len Gauge(C,n) by NAT_D:35;
then
A8: Gauge(C,n)*(i,len Gauge(C,n)-'1) in LSeg(Gauge(C,n)*(i,1),Gauge(C,n)*(i
,len Gauge(C,n))) by A1,A2,A5,A4,JORDAN1A:16;
A9: r = (Gauge(C,n)*(i,1))`1 by A1,A2,A5,A3,GOBOARD5:2
.= (Gauge(C,n)*(i,len Gauge(C,n)-'1))`1 by A1,A2,A5,A4,A7,GOBOARD5:2;
1+1 <= i by A1,NAT_1:13;
then (Gauge(C,n)*(2,2))`1 <= r by A2,A5,A3,SPRECT_3:13;
then
A10: W-bound C <= r by A3,JORDAN8:11;
i+1 <= len Gauge(C,n) by A2,NAT_1:13;
then i <= len Gauge(C,n)-1 by XREAL_1:19;
then i <= len Gauge(C,n)-'1 by XREAL_0:def 2;
then
r <= Gauge(C,n)*(len Gauge(C,n)-'1,len Gauge(C,n)-'1)`1 by A1,A5,A4,A7,A9,
SPRECT_3:13;
then
A11: r <= E-bound C by A4,JORDAN8:12,NAT_D:35;
A12: Gauge(C,n)*(i,len Gauge(C,n)-'1) = |[(Gauge(C,n)*(i,len Gauge(C,n)-'1))
`1, (Gauge(C,n)*(i,len Gauge(C,n)-'1))`2]| by EUCLID:53
.= |[(Gauge(C,n)*(i,len Gauge(C,n)-'1))`1,N-bound C]| by A1,A2,JORDAN8:14;
Gauge(C,n)*(i,2) = |[(Gauge(C,n)*(i,2))`1,(Gauge(C,n)*(i,2))`2]| by EUCLID:53
.= |[(Gauge(C,n)*(i,2))`1,S-bound C]| by A1,A2,JORDAN8:13;
then
LSeg(Gauge(C,n)*(i,2),Gauge(C,n)*(i,len Gauge(C,n)-'1)) meets Upper_Arc
C by A12,A9,A10,A11,JORDAN6:69;
hence thesis by A6,A8,TOPREAL1:6,XBOOLE_1:63;
end;
theorem Th26:
for C be Simple_closed_curve for i be Nat st 1 < i &
i < len Gauge(C,n) holds LSeg(Gauge(C,n)*(i,1),Gauge(C,n)*(i,len Gauge(C,n)))
meets Lower_Arc C
proof
let C be Simple_closed_curve;
let i be Nat;
assume that
A1: 1 < i and
A2: i < len Gauge(C,n);
set r = (Gauge(C,n)*(i,2))`1;
4 <= len Gauge(C,n) by JORDAN8:10;
then
A3: 1+1 <= len Gauge(C,n) by XXREAL_0:2;
then 1 <= len Gauge(C,n)-1 by XREAL_1:19;
then
A4: 1 <= len Gauge(C,n)-'1 by XREAL_0:def 2;
A5: len Gauge(C,n) = width Gauge(C,n) by JORDAN8:def 1;
then
A6: Gauge(C,n)*(i,2) in LSeg(Gauge(C,n)*(i,1),Gauge(C,n)*(i,len Gauge(C,n))
) by A1,A2,A3,JORDAN1A:16;
A7: len Gauge(C,n)-'1 <= len Gauge(C,n) by NAT_D:35;
then
A8: Gauge(C,n)*(i,len Gauge(C,n)-'1) in LSeg(Gauge(C,n)*(i,1),Gauge(C,n)*(i
,len Gauge(C,n))) by A1,A2,A5,A4,JORDAN1A:16;
A9: r = (Gauge(C,n)*(i,1))`1 by A1,A2,A5,A3,GOBOARD5:2
.= (Gauge(C,n)*(i,len Gauge(C,n)-'1))`1 by A1,A2,A5,A4,A7,GOBOARD5:2;
1+1 <= i by A1,NAT_1:13;
then (Gauge(C,n)*(2,2))`1 <= r by A2,A5,A3,SPRECT_3:13;
then
A10: W-bound C <= r by A3,JORDAN8:11;
i+1 <= len Gauge(C,n) by A2,NAT_1:13;
then i <= len Gauge(C,n)-1 by XREAL_1:19;
then i <= len Gauge(C,n)-'1 by XREAL_0:def 2;
then
r <= Gauge(C,n)*(len Gauge(C,n)-'1,len Gauge(C,n)-'1)`1 by A1,A5,A4,A7,A9,
SPRECT_3:13;
then
A11: r <= E-bound C by A4,JORDAN8:12,NAT_D:35;
A12: Gauge(C,n)*(i,len Gauge(C,n)-'1) = |[(Gauge(C,n)*(i,len Gauge(C,n)-'1))
`1, (Gauge(C,n)*(i,len Gauge(C,n)-'1))`2]| by EUCLID:53
.= |[(Gauge(C,n)*(i,len Gauge(C,n)-'1))`1,N-bound C]| by A1,A2,JORDAN8:14;
Gauge(C,n)*(i,2) = |[(Gauge(C,n)*(i,2))`1,(Gauge(C,n)*(i,2))`2]| by EUCLID:53
.= |[(Gauge(C,n)*(i,2))`1,S-bound C]| by A1,A2,JORDAN8:13;
then
LSeg(Gauge(C,n)*(i,2),Gauge(C,n)*(i,len Gauge(C,n)-'1)) meets Lower_Arc
C by A12,A9,A10,A11,JORDAN6:70;
hence thesis by A6,A8,TOPREAL1:6,XBOOLE_1:63;
end;
theorem
for C be Simple_closed_curve holds LSeg(Gauge(C,n)*(Center Gauge(C,n),
1), Gauge(C,n)*(Center Gauge(C,n),len Gauge(C,n))) meets Upper_Arc C
proof
let C be Simple_closed_curve;
A1: 4 <= len Gauge(C,n) by JORDAN8:10;
then len Gauge(C,n) >= 2 by XXREAL_0:2;
then
A2: 1 < Center Gauge(C,n) by Th14;
len Gauge(C,n) >= 3 by A1,XXREAL_0:2;
hence thesis by A2,Th15,Th25;
end;
theorem
for C be Simple_closed_curve holds LSeg(Gauge(C,n)*(Center Gauge(C,n),
1), Gauge(C,n)*(Center Gauge(C,n),len Gauge(C,n))) meets Lower_Arc C
proof
let C be Simple_closed_curve;
A1: 4 <= len Gauge(C,n) by JORDAN8:10;
then len Gauge(C,n) >= 2 by XXREAL_0:2;
then
A2: 1 < Center Gauge(C,n) by Th14;
len Gauge(C,n) >= 3 by A1,XXREAL_0:2;
hence thesis by A2,Th15,Th26;
end;
theorem Th29:
for C be compact connected non vertical non horizontal Subset of
TOP-REAL 2 for i be Nat st 1 <= i & i <= len Gauge(C,n) holds LSeg(
Gauge(C,n)*(i,1),Gauge(C,n)*(i,len Gauge(C,n))) meets Upper_Arc L~Cage(C,n)
proof
let C be compact connected non vertical non horizontal Subset of TOP-REAL 2;
let i be Nat;
assume that
A1: 1 <= i and
A2: i <= len Gauge(C,n);
A3: Gauge(C,n)*(i,1) = |[(Gauge(C,n)*(i,1))`1,(Gauge(C,n)*(i,1))`2]| by
EUCLID:53
.= |[(Gauge(C,n)*(i,1))`1,S-bound L~Cage(C,n)]| by A1,A2,JORDAN1A:72;
A4: Gauge(C,n)*(i,len Gauge(C,n)) = |[(Gauge(C,n)*(i,len Gauge(C,n)))`1, (
Gauge(C,n)*(i,len Gauge(C,n)))`2]| by EUCLID:53
.= |[(Gauge(C,n)*(i,len Gauge(C,n)))`1, N-bound L~Cage(C,n)]| by A1,A2,
JORDAN1A:70;
set r = (Gauge(C,n)*(i,1))`1;
4 <= len Gauge(C,n) by JORDAN8:10;
then
A5: 1 <= len Gauge(C,n) by XXREAL_0:2;
A6: len Gauge(C,n) = width Gauge(C,n) by JORDAN8:def 1;
then (Gauge(C,n)*(1,1))`1 <= r by A1,A2,A5,SPRECT_3:13;
then
A7: W-bound L~Cage(C,n) <= r by A5,JORDAN1A:73;
r <= Gauge(C,n)*(len Gauge(C,n),1)`1 by A1,A2,A6,A5,SPRECT_3:13;
then
A8: r <= E-bound L~Cage(C,n) by A5,JORDAN1A:71;
r = (Gauge(C,n)*(i,len Gauge(C,n)))`1 by A1,A2,A6,A5,GOBOARD5:2;
hence thesis by A3,A4,A7,A8,JORDAN6:69;
end;
theorem Th30:
for C be compact connected non vertical non horizontal Subset of
TOP-REAL 2 for i be Nat st 1 <= i & i <= len Gauge(C,n) holds LSeg(
Gauge(C,n)*(i,1),Gauge(C,n)*(i,len Gauge(C,n))) meets Lower_Arc L~Cage(C,n)
proof
let C be compact connected non vertical non horizontal Subset of TOP-REAL 2;
let i be Nat;
assume that
A1: 1 <= i and
A2: i <= len Gauge(C,n);
A3: Gauge(C,n)*(i,1) = |[(Gauge(C,n)*(i,1))`1,(Gauge(C,n)*(i,1))`2]| by
EUCLID:53
.= |[(Gauge(C,n)*(i,1))`1,S-bound L~Cage(C,n)]| by A1,A2,JORDAN1A:72;
A4: Gauge(C,n)*(i,len Gauge(C,n)) = |[(Gauge(C,n)*(i,len Gauge(C,n)))`1, (
Gauge(C,n)*(i,len Gauge(C,n)))`2]| by EUCLID:53
.= |[(Gauge(C,n)*(i,len Gauge(C,n)))`1, N-bound L~Cage(C,n)]| by A1,A2,
JORDAN1A:70;
set r = (Gauge(C,n)*(i,1))`1;
4 <= len Gauge(C,n) by JORDAN8:10;
then
A5: 1 <= len Gauge(C,n) by XXREAL_0:2;
A6: len Gauge(C,n) = width Gauge(C,n) by JORDAN8:def 1;
then (Gauge(C,n)*(1,1))`1 <= r by A1,A2,A5,SPRECT_3:13;
then
A7: W-bound L~Cage(C,n) <= r by A5,JORDAN1A:73;
r <= Gauge(C,n)*(len Gauge(C,n),1)`1 by A1,A2,A6,A5,SPRECT_3:13;
then
A8: r <= E-bound L~Cage(C,n) by A5,JORDAN1A:71;
r = (Gauge(C,n)*(i,len Gauge(C,n)))`1 by A1,A2,A6,A5,GOBOARD5:2;
hence thesis by A3,A4,A7,A8,JORDAN6:70;
end;
theorem
for C be compact connected non vertical non horizontal Subset of
TOP-REAL 2 holds LSeg(Gauge(C,n)*(Center Gauge(C,n),1), Gauge(C,n)*(Center
Gauge(C,n),len Gauge(C,n))) meets Upper_Arc L~Cage(C,n)
proof
let C be compact connected non vertical non horizontal Subset of TOP-REAL 2;
A1: 4 <= len Gauge(C,n) by JORDAN8:10;
then len Gauge(C,n) >= 3 by XXREAL_0:2;
then
A2: Center Gauge(C,n) < len Gauge(C,n) by Th15;
len Gauge(C,n) >= 2 by A1,XXREAL_0:2;
then 1 < Center Gauge(C,n) by Th14;
hence thesis by A2,Th29;
end;
theorem
for C be compact connected non vertical non horizontal Subset of
TOP-REAL 2 holds LSeg(Gauge(C,n)*(Center Gauge(C,n),1), Gauge(C,n)*(Center
Gauge(C,n),len Gauge(C,n))) meets Lower_Arc L~Cage(C,n)
proof
let C be compact connected non vertical non horizontal Subset of TOP-REAL 2;
A1: 4 <= len Gauge(C,n) by JORDAN8:10;
then len Gauge(C,n) >= 3 by XXREAL_0:2;
then
A2: Center Gauge(C,n) < len Gauge(C,n) by Th15;
len Gauge(C,n) >= 2 by A1,XXREAL_0:2;
then 1 < Center Gauge(C,n) by Th14;
hence thesis by A2,Th30;
end;
theorem Th33:
j <= width G implies cell(G,0,j) is not bounded
proof
assume
A1: j <= width G;
per cases by A1,NAT_1:14,XXREAL_0:1;
suppose
j = 0;
then
A2: cell(G,0,j) = { |[r,s]| where r, s is Real:
r <= G*(1,1)`1 & s <= G*(
1,1)`2 } by GOBRD11:24;
not ex r being Real st
for q being Point of TOP-REAL 2 st q in cell(G,0,j) holds |.q.| < r
proof
let r be Real;
take q = |[min(-r,G*(1,1)`1),min(-r,G*(1,1)`2)]|;
A3: min(-r,G*(1,1)`2) <= G*(1,1)`2 by XXREAL_0:17;
min(-r,G*(1,1)`1) <= G*(1,1)`1 by XXREAL_0:17;
hence q in cell(G,0,j) by A2,A3;
A4: |.q`1.|<=|.q.| by JGRAPH_1:33;
per cases;
suppose
r <= 0;
hence thesis;
end;
suppose
A5: r > 0;
q`1 = min(-r,G*(1,1)`1) by EUCLID:52;
then
A6: |.-r.| <= |.q`1.| by A5,TOPREAL6:3,XXREAL_0:17;
--r > 0 by A5;
then -r < 0;
then --r <= |.q`1.| by A6,ABSVALUE:def 1;
hence thesis by A4,XXREAL_0:2;
end;
end;
hence thesis by JORDAN2C:34;
end;
suppose
A7: j >= 1 & j < width G;
then
A8: cell(G,0,j) = { |[r,s]| where r is Real, s is Real:
r <= G*(1,1)`1 & G*(1,j)`2 <= s & s <= G* (1,j+1)`2 } by GOBRD11:26;
not ex r being Real st
for q being Point of TOP-REAL 2 st q in cell(G,0,j) holds |.q.| < r
proof
len G <> 0 by MATRIX_0:def 10;
then
A9: 1 <= len G by NAT_1:14;
let r be Real;
take q = |[min(-r,G*(1,1)`1),G*(1,j)`2]|;
A10: j < j+1 by NAT_1:13;
A11: min(-r,G*(1,1)`1) <= G*(1,1)`1 by XXREAL_0:17;
j+1 <= width G by A7,NAT_1:13;
then G*(1,j)`2 <= G*(1,j+1)`2 by A7,A9,A10,GOBOARD5:4;
hence q in cell(G,0,j) by A8,A11;
A12: |.q`1.|<=|.q.| by JGRAPH_1:33;
per cases;
suppose
r <= 0;
hence thesis;
end;
suppose
A13: r > 0;
q`1 = min(-r,G*(1,1)`1) by EUCLID:52;
then
A14: |.-r.| <= |.q`1.| by A13,TOPREAL6:3,XXREAL_0:17;
--r > 0 by A13;
then -r < 0;
then --r <= |.q`1.| by A14,ABSVALUE:def 1;
hence thesis by A12,XXREAL_0:2;
end;
end;
hence thesis by JORDAN2C:34;
end;
suppose
j = width G;
then
A15: cell(G,0,j) = { |[r,s]| where r is Real, s is Real:
r <= G*(1,1)`1 & G*(1,width G)`2 <= s } by GOBRD11:25;
not ex r being Real st
for q being Point of TOP-REAL 2 st q in cell(G,0,j) holds |.q.| < r
proof
let r be Real;
take q = |[G*(1,1)`1,max(r,G*(1,width G)`2)]|;
A16: |.q`2.|<=|.q.| by JGRAPH_1:33;
G*(1, width G)`2 <= max(r,G*(1,width G)`2) by XXREAL_0:25;
hence q in cell(G,0,j) by A15;
per cases;
suppose
r <= 0;
hence thesis;
end;
suppose
A17: r > 0;
q`2 = max(r,G*(1,width G)`2) by EUCLID:52;
then r <= q`2 by XXREAL_0:25;
then r <= |.q`2.| by A17,ABSVALUE:def 1;
hence thesis by A16,XXREAL_0:2;
end;
end;
hence thesis by JORDAN2C:34;
end;
end;
theorem Th34:
i <= width G implies cell(G,len G,i) is not bounded
proof
assume
A1: i <= width G;
per cases by A1,NAT_1:14,XXREAL_0:1;
suppose
A2: i = 0;
A3: cell(G,len G,0) = { |[r,s]| where r is Real, s is Real:
G*(len G,1)`1 <= r & s <= G*(1,1)`2 } by GOBRD11:27;
not ex r being Real st
for q being Point of TOP-REAL 2 st q in cell(G,len G,0) holds |.q.| < r
proof
let r be Real;
take q = |[G*(len G,1)`1,min(-r,G*(1,1)`2)]|;
A4: |.q`2.|<=|.q.| by JGRAPH_1:33;
min(-r,G*(1,1)`2) <= G*(1,1)`2 by XXREAL_0:17;
hence q in cell(G,len G,0) by A3;
per cases;
suppose
r <= 0;
hence thesis;
end;
suppose
A5: r > 0;
q`2 = min(-r,G*(1,1)`2) by EUCLID:52;
then
A6: |.-r.| <= |.q`2.| by A5,TOPREAL6:3,XXREAL_0:17;
--r > 0 by A5;
then -r < 0;
then --r <= |.q`2.| by A6,ABSVALUE:def 1;
hence thesis by A4,XXREAL_0:2;
end;
end;
hence thesis by A2,JORDAN2C:34;
end;
suppose
A7: i >= 1 & i < width G;
then
A8: cell(G,len G,i) = { |[r,s]| where r,s is Real:
G*(len G,1)`1 <= r & G*(1,i)`2 <=s & s <= G*(1,i+1)`2 } by
GOBRD11:29;
not ex r being Real st
for q being Point of TOP-REAL 2 st q in cell(G,len G,i) holds |.q.| < r
proof
len G <> 0 by MATRIX_0:def 10;
then
A9: 1 <= len G by NAT_1:14;
let r be Real;
take q = |[max(r,G*(len G,1)`1),G*(1,i)`2]|;
A10: i < i+1 by NAT_1:13;
A11: max(r,G*(len G,1)`1) >= G*(len G,1)`1 by XXREAL_0:25;
i+1 <= width G by A7,NAT_1:13;
then G*(1,i)`2 <= G*(1,i+1)`2 by A7,A9,A10,GOBOARD5:4;
hence q in cell(G,len G,i) by A8,A11;
A12: |.q`1.|<=|.q.| by JGRAPH_1:33;
per cases;
suppose
r <= 0;
hence thesis;
end;
suppose
A13: r > 0;
q`1 = max(r,G*(len G,1)`1) by EUCLID:52;
then q`1 >= r by XXREAL_0:25;
then r <= |.q`1.| by A13,ABSVALUE:def 1;
hence thesis by A12,XXREAL_0:2;
end;
end;
hence thesis by JORDAN2C:34;
end;
suppose
A14: i = width G;
A15: cell(G,len G,width G) = { |[r,s]| where r, s is Real:
G*(len G,1)`1 <= r & G*(1,width G)`2 <= s } by GOBRD11:28;
not ex r being Real st
for q being Point of TOP-REAL 2 st q in cell(G,len G,i) holds |.q.| < r
proof
let r be Real;
take q = |[G*(len G,1)`1,max(r,G*(1,width G)`2)]|;
A16: |.q`2.|<=|.q.| by JGRAPH_1:33;
G*(1,width G)`2 <= max(r,G*(1,width G)`2) by XXREAL_0:25;
hence q in cell(G,len G,i) by A14,A15;
per cases;
suppose
r <= 0;
hence thesis;
end;
suppose
A17: r > 0;
q`2 = max(r,G*(1,width G)`2) by EUCLID:52;
then r <= q`2 by XXREAL_0:25;
then r <= |.q`2.| by A17,ABSVALUE:def 1;
hence thesis by A16,XXREAL_0:2;
end;
end;
hence thesis by JORDAN2C:34;
end;
end;
theorem Th35:
j <= width Gauge(C,n) implies cell(Gauge(C,n),0,j) c= UBD C
proof
assume
A1: j <= width Gauge(C,n);
A2: C` is non empty by JORDAN2C:66;
A3: len Gauge(C,n) = width Gauge(C,n) by JORDAN8:def 1;
then
A4: cell(Gauge(C,n),0,j) is non empty by A1,JORDAN1A:24;
cell(Gauge(C,n),0,j) misses C by A3,A1,JORDAN8:18;
then
A5: cell(Gauge(C,n),0,j) c= C` by SUBSET_1:23;
cell(Gauge(C,n),0,j) is connected by A3,A1,JORDAN1A:25;
then consider W being Subset of TOP-REAL 2 such that
A6: W is_a_component_of C` and
A7: cell(Gauge(C,n),0,j) c= W by A5,A2,A4,GOBOARD9:3;
W is not bounded by A1,A7,Th33,RLTOPSP1:42;
then W is_outside_component_of C by A6,JORDAN2C:def 3;
then W c= UBD C by JORDAN2C:23;
hence thesis by A7;
end;
theorem Th36:
j <= len Gauge(E,n) implies cell(Gauge(E,n),len Gauge(E,n),j) c= UBD E
proof
A1: E` is non empty by JORDAN2C:66;
assume
A2: j <= len Gauge(E,n);
then cell(Gauge(E,n),len Gauge(E,n),j) misses E by JORDAN8:16;
then
A3: cell(Gauge(E,n),len Gauge(E,n),j) c= E` by SUBSET_1:23;
A4: width Gauge(E,n) = len Gauge(E,n) by JORDAN8:def 1;
then
A5: cell(Gauge(E,n),len Gauge(E,n),j) is non empty by A2,JORDAN1A:24;
cell(Gauge(E,n),len Gauge(E,n),j) is connected by A4,A2,JORDAN1A:25;
then consider W being Subset of TOP-REAL 2 such that
A6: W is_a_component_of E` and
A7: cell(Gauge(E,n),len Gauge(E,n),j) c= W by A3,A1,A5,GOBOARD9:3;
W is not bounded by A4,A2,A7,Th34,RLTOPSP1:42;
then W is_outside_component_of E by A6,JORDAN2C:def 3;
then W c= UBD E by JORDAN2C:23;
hence thesis by A7;
end;
Lm3: j <= width Gauge(C,n) & cell(Gauge(C,n),i,j) c= BDD C implies i <> 0
proof
assume that
A1: j <= width Gauge(C,n) and
A2: cell(Gauge(C,n),i,j) c= BDD C and
A3: i = 0;
A4: cell(Gauge(C,n),0,j) c= UBD C by A1,Th35;
0 <= len Gauge(C,n);
then cell(Gauge(C,n),0,j) is non empty by A1,JORDAN1A:24;
hence contradiction by A2,A3,A4,JORDAN2C:24,XBOOLE_1:68;
end;
Lm4: i <= len Gauge(C,n) & cell(Gauge(C,n),i,j) c= BDD C implies j <> 0
proof
assume that
A1: i <= len Gauge(C,n) and
A2: cell(Gauge(C,n),i,j) c= BDD C and
A3: j = 0;
A4: cell(Gauge(C,n),i,0) c= UBD C by A1,JORDAN1A:49;
0 <= width Gauge(C,n);
then cell(Gauge(C,n),i,0) is non empty by A1,JORDAN1A:24;
hence contradiction by A2,A3,A4,JORDAN2C:24,XBOOLE_1:68;
end;
Lm5: j <= width Gauge(C,n) & cell(Gauge(C,n),i,j) c= BDD C implies i <> len
Gauge(C,n)
proof
assume that
A1: j <= width Gauge(C,n) and
A2: cell(Gauge(C,n),i,j) c= BDD C;
A3: cell(Gauge(C,n),len Gauge(C,n),j) is non empty by A1,JORDAN1A:24;
assume
A4: i = len Gauge(C,n);
len Gauge(C,n) = width Gauge(C,n) by JORDAN8:def 1;
then cell(Gauge(C,n),len Gauge(C,n),j) c= UBD C by A1,Th36;
hence contradiction by A2,A4,A3,JORDAN2C:24,XBOOLE_1:68;
end;
Lm6: i <= len Gauge(C,n) & cell(Gauge(C,n),i,j) c= BDD C implies j <> width
Gauge(C,n)
proof
assume that
A1: i <= len Gauge(C,n) and
A2: cell(Gauge(C,n),i,j) c= BDD C;
A3: cell(Gauge(C,n),i,width Gauge(C,n)) c= UBD C by A1,JORDAN1A:50;
assume
A4: j = width Gauge(C,n);
cell(Gauge(C,n),i,width Gauge(C,n)) is non empty by A1,JORDAN1A:24;
hence contradiction by A2,A4,A3,JORDAN2C:24,XBOOLE_1:68;
end;
theorem Th37:
i <= len Gauge(C,n) & j <= width Gauge(C,n) & cell(Gauge(C,n),i,
j) c= BDD C implies j > 1
proof
assume that
A1: i <= len Gauge(C,n) and
A2: j <= width Gauge(C,n) and
A3: cell(Gauge(C,n),i,j) c= BDD C and
A4: j <= 1;
per cases by A4,NAT_1:25;
suppose
j = 0;
hence contradiction by A1,A3,Lm4;
end;
suppose
A5: j = 1;
BDD C c= C` by JORDAN2C:25;
then
A6: cell(Gauge(C,n),i,1) c= C` by A3,A5;
A7: i <> 0 by A2,A3,Lm3;
UBD C is_outside_component_of C by JORDAN2C:68;
then
A8: UBD C is_a_component_of C` by JORDAN2C:def 3;
A9: width Gauge(C,n) <> 0 by MATRIX_0:def 10;
then
A10: 0+1 <= width Gauge(C,n) by NAT_1:14;
then
A11: cell(Gauge(C,n),i,1) is non empty by A1,JORDAN1A:24;
i < len Gauge(C,n) by A1,A2,A3,Lm5,XXREAL_0:1;
then
cell(Gauge(C,n),i,0) /\ cell(Gauge(C,n),i,0+1) = LSeg(Gauge(C,n)*(i,0
+1),Gauge(C,n)*(i+1,0+1)) by A9,A7,GOBOARD5:26,NAT_1:14;
then
A12: cell(Gauge(C,n),i,0) meets cell(Gauge(C,n),i,0+1) by XBOOLE_0:def 7;
cell(Gauge(C,n),i,0) c= UBD C by A1,JORDAN1A:49;
then cell(Gauge(C,n),i,1) c= UBD C by A1,A10,A12,A8,A6,GOBOARD9:4
,JORDAN1A:25;
hence contradiction by A3,A5,A11,JORDAN2C:24,XBOOLE_1:68;
end;
end;
theorem Th38:
i <= len Gauge(C,n) & j <= width Gauge(C,n) & cell(Gauge(C,n),i,
j) c= BDD C implies i > 1
proof
assume that
A1: i <= len Gauge(C,n) and
A2: j <= width Gauge(C,n) and
A3: cell(Gauge(C,n),i,j) c= BDD C and
A4: i <= 1;
per cases by A4,NAT_1:25;
suppose
i = 0;
hence contradiction by A2,A3,Lm3;
end;
suppose
A5: i = 1;
BDD C c= C` by JORDAN2C:25;
then
A6: cell(Gauge(C,n),1,j) c= C` by A3,A5;
A7: j <> 0 by A1,A3,Lm4;
UBD C is_outside_component_of C by JORDAN2C:68;
then
A8: UBD C is_a_component_of C` by JORDAN2C:def 3;
A9: len Gauge(C,n) <> 0 by MATRIX_0:def 10;
then
A10: 0+1 <= len Gauge(C,n) by NAT_1:14;
then
A11: cell(Gauge(C,n),1,j) is non empty by A2,JORDAN1A:24;
j < width Gauge(C,n) by A1,A2,A3,Lm6,XXREAL_0:1;
then
cell(Gauge(C,n),0,j) /\ cell(Gauge(C,n),0+1,j) = LSeg(Gauge(C,n)*(0+1
,j),Gauge(C,n)*(0+1,j+1)) by A9,A7,GOBOARD5:25,NAT_1:14;
then
A12: cell(Gauge(C,n),0,j) meets cell(Gauge(C,n),0+1,j) by XBOOLE_0:def 7;
cell(Gauge(C,n),0,j) c= UBD C by A2,Th35;
then cell(Gauge(C,n),1,j) c= UBD C by A2,A10,A12,A8,A6,GOBOARD9:4
,JORDAN1A:25;
hence contradiction by A3,A5,A11,JORDAN2C:24,XBOOLE_1:68;
end;
end;
theorem Th39:
i <= len Gauge(C,n) & j <= width Gauge(C,n) & cell(Gauge(C,n),i,
j) c= BDD C implies j+1 < width Gauge(C,n)
proof
assume that
A1: i <= len Gauge(C,n) and
A2: j <= width Gauge(C,n) and
A3: cell(Gauge(C,n),i,j) c= BDD C;
A4: j < width Gauge(C,n) or j = width Gauge(C,n) by A2,XXREAL_0:1;
assume j + 1 >= width Gauge(C,n);
then
A5: j + 1 > width Gauge(C,n) or j + 1 = width Gauge(C,n) by XXREAL_0:1;
per cases by A5,A4,NAT_1:13;
suppose
j = width Gauge(C,n);
hence contradiction by A1,A3,Lm6;
end;
suppose
j + 1 = width Gauge(C,n);
then
A6: cell(Gauge(C,n),i,width Gauge(C,n)-'1) c= BDD C by A3,NAT_D:34;
BDD C c= C` by JORDAN2C:25;
then
A7: cell(Gauge(C,n),i,width Gauge(C,n)-'1) c= C` by A6;
A8: width Gauge(C,n) <> 0 by MATRIX_0:def 10;
then
A9: width Gauge(C,n)-'1+1 = width Gauge(C,n) by NAT_1:14,XREAL_1:235;
width Gauge(C,n)-'1 <= width Gauge(C,n) by NAT_D:44;
then
A10: cell(Gauge(C,n),i,width Gauge(C,n)-'1) is non empty by A1,JORDAN1A:24;
A11: cell(Gauge(C,n),i,width Gauge(C,n)) c= UBD C by A1,JORDAN1A:50;
UBD C is_outside_component_of C by JORDAN2C:68;
then
A12: UBD C is_a_component_of C` by JORDAN2C:def 3;
A13: i <> 0 by A2,A3,Lm3;
A14: width Gauge(C,n)-1 < width Gauge(C,n) by XREAL_1:146;
i < len Gauge(C,n) by A1,A2,A3,Lm5,XXREAL_0:1;
then
cell(Gauge(C,n),i,width Gauge(C,n)) /\ cell(Gauge(C,n),i,width Gauge(
C,n)-'1) = LSeg(Gauge(C,n)*(i,width Gauge(C,n)), Gauge(C,n)*(i+1,width Gauge(C,
n))) by A14,A9,A13,GOBOARD5:26,NAT_1:14;
then
A15: cell(Gauge(C,n),i,width Gauge(C,n)) meets cell(Gauge(C,n),i,width
Gauge(C,n)-'1) by XBOOLE_0:def 7;
width Gauge(C,n)-'1 < width Gauge(C,n) by A8,A14,NAT_1:14,XREAL_1:233;
then cell(Gauge(C,n),i,width Gauge(C,n)-'1) c= UBD C by A1,A11,A15,A12,A7,
GOBOARD9:4,JORDAN1A:25;
hence contradiction by A6,A10,JORDAN2C:24,XBOOLE_1:68;
end;
end;
theorem Th40:
i <= len Gauge(C,n) & j <= width Gauge(C,n) & cell(Gauge(C,n),i,
j) c= BDD C implies i+1 < len Gauge(C,n)
proof
assume that
A1: i <= len Gauge(C,n) and
A2: j <= width Gauge(C,n) and
A3: cell(Gauge(C,n),i,j) c= BDD C;
A4: i < len Gauge(C,n) or i = len Gauge(C,n) by A1,XXREAL_0:1;
assume i + 1 >= len Gauge(C,n);
then
A5: i + 1 > len Gauge(C,n) or i + 1 = len Gauge(C,n) by XXREAL_0:1;
per cases by A5,A4,NAT_1:13;
suppose
i = len Gauge(C,n);
hence contradiction by A2,A3,Lm5;
end;
suppose
i + 1 = len Gauge(C,n);
then
A6: cell(Gauge(C,n),len Gauge(C,n)-'1,j) c= BDD C by A3,NAT_D:34;
BDD C c= C` by JORDAN2C:25;
then
A7: cell(Gauge(C,n),len Gauge(C,n)-'1,j) c= C` by A6;
A8: len Gauge(C,n) <> 0 by MATRIX_0:def 10;
then
A9: len Gauge(C,n)-'1+1 = len Gauge(C,n) by NAT_1:14,XREAL_1:235;
len Gauge(C,n)-'1 <= len Gauge(C,n) by NAT_D:44;
then
A10: cell(Gauge(C,n),len Gauge(C,n)-'1,j) is non empty by A2,JORDAN1A:24;
A11: j <> 0 by A1,A3,Lm4;
UBD C is_outside_component_of C by JORDAN2C:68;
then
A12: UBD C is_a_component_of C` by JORDAN2C:def 3;
len Gauge(C,n) = width Gauge(C,n) by JORDAN8:def 1;
then
A13: cell(Gauge(C,n),len Gauge(C,n),j) c= UBD C by A2,Th36;
A14: len Gauge(C,n)-1 < len Gauge(C,n) by XREAL_1:146;
j < width Gauge(C,n) by A1,A2,A3,Lm6,XXREAL_0:1;
then
cell(Gauge(C,n),len Gauge(C,n),j) /\ cell(Gauge(C,n),len Gauge(C,n)-'
1,j) = LSeg(Gauge(C,n)*(len Gauge(C,n),j), Gauge(C,n)*(len Gauge(C,n),j+1)) by
A14,A9,A11,GOBOARD5:25,NAT_1:14;
then
A15: cell(Gauge(C,n),len Gauge(C,n),j) meets cell(Gauge(C,n),len Gauge(C,n
)-'1,j) by XBOOLE_0:def 7;
len Gauge(C,n)-'1 < len Gauge(C,n) by A8,A14,NAT_1:14,XREAL_1:233;
then cell(Gauge(C,n),len Gauge(C,n)-'1,j) c= UBD C by A2,A13,A15,A12,A7,
GOBOARD9:4,JORDAN1A:25;
hence contradiction by A6,A10,JORDAN2C:24,XBOOLE_1:68;
end;
end;
theorem
(ex i,j st i <= len Gauge(C,n) & j <= width Gauge(C,n) & cell(Gauge(C,
n),i,j) c= BDD C) implies n >= 1
proof
A1: 2|^0 = 1 by NEWTON:4;
given i,j such that
A2: i <= len Gauge(C,n) and
A3: j <= width Gauge(C,n) and
A4: cell(Gauge(C,n),i,j) c= BDD C;
A5: j + 1 < width Gauge(C,n) by A2,A3,A4,Th39;
A6: i + 1 < len Gauge(C,n) by A2,A3,A4,Th40;
assume
A7: n < 1;
len Gauge(C,n) = 2|^n + 3 by JORDAN8:def 1;
then
A8: len Gauge(C,n) = 1 + 3 by A1,A7,NAT_1:14;
width Gauge(C,n) = 2|^n + 3 by JORDAN1A:28;
then
A9: width Gauge(C,n) = 1 + 3 by A1,A7,NAT_1:14;
i <= 4 by A8,A2;
then
A10: i = 0 or ... or i = 4;
j <= 4 by A3,A9;
then j = 0 or ... or j = 4;
then per cases by A10;
suppose
j= 0 or j=1;
hence thesis by A2,A3,A4,Th37;
end;
suppose
i= 0 or i=1;
hence thesis by A2,A3,A4,Th38;
end;
suppose
j=2 & i=2;
then cell(Gauge(C,0),2,2) c= BDD C by A4,A7,NAT_1:14;
hence contradiction by Th18;
end;
suppose
j=3 or j=4 or i=3 or i=4;
hence thesis by A5,A6,A9,A8;
end;
end;