:: Gauges and Cages
:: by Artur Korni{\l}owicz, Robert Milewski, Adam Naumowicz and
:: Andrzej Trybulec
::
:: Received September 12, 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, SUBSET_1, XBOOLE_0, EUCLID, RCOMP_1, SPPOL_1, RELAT_2,
GOBOARD1, PRE_TOPC, RELAT_1, ARYTM_3, INT_1, CARD_1, FINSEQ_1, ABIAN,
ARYTM_1, TOPREAL2, FUNCT_1, GOBOARD5, TOPREAL1, PSCOMP_1, MCART_1,
RLTOPSP1, JORDAN2C, JORDAN6, TARSKI, XXREAL_1, XXREAL_0, REAL_1, TREES_1,
MATRIX_1, PARTFUN1, TOPS_1, COMPLEX1, JORDAN8, NEWTON, CONNSP_1, JORDAN9,
GOBOARD9, JORDAN1A, CONVEX1, XXREAL_2, NAT_1;
notations TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, XXREAL_0,
XREAL_0, REAL_1, NAT_1, NAT_D, FUNCT_1, RELSET_1, PARTFUN1, FUNCT_2,
COMPLEX1, STRUCT_0, FINSEQ_1, NEWTON, PRE_TOPC, TOPS_1, CONNSP_1,
COMPTS_1, GOBOARD1, MATRIX_0, RCOMP_1, RLTOPSP1, EUCLID, TOPREAL1,
TOPREAL2, PSCOMP_1, SPPOL_1, ABIAN, GOBOARD5, GOBOARD9, JORDAN6, JORDAN8,
JORDAN9, JORDAN2C;
constructors REAL_1, SQUARE_1, NAT_D, RCOMP_1, NEWTON, ABIAN, TOPS_1,
CONNSP_1, MONOID_0, PSCOMP_1, GOBOARD9, JORDAN6, JORDAN2C, JORDAN8,
GOBRD13, JORDAN9, RELSET_1, CONVEX1;
registrations ORDINAL1, RELSET_1, NUMBERS, XREAL_0, NAT_1, STRUCT_0, MONOID_0,
EUCLID, JORDAN1, PSCOMP_1, SPRECT_1, SPRECT_2, SPRECT_3, JORDAN2C,
TOPREAL6, JORDAN8, JORDAN10, FUNCT_1, NEWTON, INT_1;
requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM;
definitions TARSKI, ABIAN, XBOOLE_0;
equalities XBOOLE_0, PSCOMP_1;
expansions TARSKI, XBOOLE_0;
theorems EUCLID, GOBOARD7, JORDAN8, JORDAN9, JORDAN10, PSCOMP_1, NAT_1,
NEWTON, SPRECT_1, FUNCT_1, ABSVALUE, TOPREAL1, SPRECT_3, GOBRD11,
GOBOARD5, JORDAN2C, GOBRD14, SUBSET_1, ZFMISC_1, TARSKI, TOPREAL3,
FINSEQ_1, GOBOARD1, SPPOL_1, SPPOL_2, GOBOARD9, CONNSP_1, TOPREAL6,
FINSEQ_6, SPRECT_2, INT_1, TOPS_1, JGRAPH_1, JORDAN6, FUNCT_2, XBOOLE_0,
XBOOLE_1, XCMPLX_1, PEPIN, XREAL_1, XXREAL_0, PREPOWER, ABIAN, NAT_D,
PARTFUN1, MATRIX_0, XXREAL_1, RLTOPSP1;
schemes NAT_1;
begin :: Preliminaries
reserve i, i1, i2, j, j1, j2, k, m, n, t for Nat,
D for non empty Subset of TOP-REAL 2,
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,
p, q, x for Point of TOP-REAL 2,
r, s for Real;
3 = 2 * 1 + 1;
then
Lm1: 3 div 2 = 1 by NAT_D:def 1;
1 = 2 * 0 + 1;
then
Lm2: 1 div 2 = 0 by NAT_D:def 1;
definition
let f be FinSequence;
func Center f -> Nat equals
len f div 2 + 1;
coherence;
end;
theorem
for f being FinSequence st len f is odd holds len f = 2 * Center f - 1
proof
let f be FinSequence;
assume len f is odd;
then consider k being Nat such that
A1: len f = 2*k+1 by ABIAN:9;
A2: 2*k mod 2 = 0;
thus len f = 2 * ((2*k div 2) + (1 div 2)) + 1 by A1,Lm2
.= 2 * (len f div 2) + (2*1 - 1) by A1,A2,NAT_D:19
.= 2 * Center f - 1;
end;
theorem
for f being FinSequence st len f is even holds len f = 2 * Center f - 2
proof
let f be FinSequence;
assume ex k being Nat st len f = 2*k;
hence len f = 2 * (len f div 2) + 2*1 - 2
.= 2 * Center f - 2;
end;
begin :: Some subsets of the plane
registration
cluster compact non vertical non horizontal being_simple_closed_curve non
empty for Subset of TOP-REAL 2;
existence
proof
set f = the non constant standard special_circular_sequence;
take L~f;
thus thesis;
end;
end;
theorem Th3:
p in N-most D implies p`2 = N-bound D
proof
assume p in N-most D;
then
A1: p in LSeg(NW-corner D, NE-corner D) by XBOOLE_0:def 4;
(NE-corner D)`2 = N-bound D by EUCLID:52
.= (NW-corner D)`2 by EUCLID:52;
hence p`2 = (NW-corner D)`2 by A1,GOBOARD7:6
.= N-bound D by EUCLID:52;
end;
theorem Th4:
p in E-most D implies p`1 = E-bound D
proof
assume p in E-most D;
then
A1: p in LSeg(SE-corner D, NE-corner D) by XBOOLE_0:def 4;
(SE-corner D)`1 = E-bound D by EUCLID:52
.= (NE-corner D)`1 by EUCLID:52;
hence p`1 = (SE-corner D)`1 by A1,GOBOARD7:5
.= E-bound D by EUCLID:52;
end;
theorem Th5:
p in S-most D implies p`2 = S-bound D
proof
assume p in S-most D;
then
A1: p in LSeg(SW-corner D, SE-corner D) by XBOOLE_0:def 4;
(SE-corner D)`2 = S-bound D by EUCLID:52
.= (SW-corner D)`2 by EUCLID:52;
hence p`2 = (SW-corner D)`2 by A1,GOBOARD7:6
.= S-bound D by EUCLID:52;
end;
theorem Th6:
p in W-most D implies p`1 = W-bound D
proof
assume p in W-most D;
then
A1: p in LSeg(SW-corner D, NW-corner D) by XBOOLE_0:def 4;
(SW-corner D)`1 = W-bound D by EUCLID:52
.= (NW-corner D)`1 by EUCLID:52;
hence p`1 = (SW-corner D)`1 by A1,GOBOARD7:5
.= W-bound D by EUCLID:52;
end;
theorem
for D being Subset of TOP-REAL 2 holds BDD D misses D
proof
let D be Subset of TOP-REAL 2;
D misses D` by SUBSET_1:24;
hence thesis by JORDAN2C:25,XBOOLE_1:63;
end;
theorem Th8:
p in Vertical_Line(p`1)
proof
p in {q where q is Point of TOP-REAL 2: p`1=q`1};
hence thesis by JORDAN6:def 6;
end;
theorem
|[r,s]| in Vertical_Line r
proof
|[r,s]|`1 = r by EUCLID:52;
hence thesis by Th8;
end;
theorem
for A being Subset of TOP-REAL 2 st A c= Vertical_Line s holds A is vertical
proof
A1: Vertical_Line(s) = {p where p is Point of TOP-REAL 2: p`1=s} by
JORDAN6:def 6;
let A being Subset of TOP-REAL 2 such that
A2: A c= Vertical_Line s;
for p,q being Point of TOP-REAL 2 st p in A & q in A holds p`1=q`1
proof
let p,q be Point of TOP-REAL 2;
assume p in A;
then p in Vertical_Line s by A2;
then
A3: ex p1 being Point of TOP-REAL 2 st p1 = p & p1`1 =s by A1;
assume q in A;
then q in Vertical_Line s by A2;
then ex p1 being Point of TOP-REAL 2 st p1 = q & p1`1 =s by A1;
hence thesis by A3;
end;
hence thesis by SPPOL_1:def 3;
end;
theorem
p`1 = q`1 & r in [. proj2.p,proj2.q .] implies |[p`1,r]| in LSeg(p,q)
proof
assume
A1: p`1 = q`1;
assume
A2: r in [. proj2.p,proj2.q .];
A3: |[p`1,r]|`2 = r by EUCLID:52;
proj2.q = q`2 by PSCOMP_1:def 6;
then
A4: |[p`1,r]|`2 <= q`2 by A2,A3,XXREAL_1:1;
proj2.p = p`2 by PSCOMP_1:def 6;
then p`1 = |[p`1,r]|`1 & p`2 <= |[p`1,r]|`2 by A2,A3,EUCLID:52,XXREAL_1:1;
hence thesis by A1,A4,GOBOARD7:7;
end;
theorem
p`2 = q`2 & r in [. proj1.p,proj1.q .] implies |[r,p`2]| in LSeg(p,q)
proof
assume
A1: p`2 = q`2;
assume
A2: r in [. proj1.p,proj1.q .];
A3: |[r,p`2]|`1 = r by EUCLID:52;
proj1.q = q`1 by PSCOMP_1:def 5;
then
A4: |[r,p`2]|`1 <= q`1 by A2,A3,XXREAL_1:1;
proj1.p = p`1 by PSCOMP_1:def 5;
then p`2 = |[r,p`2]|`2 & p`1 <= |[r,p`2]|`1 by A2,A3,EUCLID:52,XXREAL_1:1;
hence thesis by A1,A4,GOBOARD7:8;
end;
theorem
p in Vertical_Line s & q in Vertical_Line s implies LSeg(p,q) c=
Vertical_Line s
proof
A1: Vertical_Line(s) = {p1 where p1 is Point of TOP-REAL 2: p1`1=s} by
JORDAN6:def 6;
assume p in Vertical_Line s & q in Vertical_Line s;
then
A2: p`1 = s & q`1 = s by JORDAN6:31;
let u be object;
assume
A3: u in LSeg(p,q);
then reconsider p1 = u as Point of TOP-REAL 2;
p1`1 = s by A2,A3,GOBOARD7:5;
hence thesis by A1;
end;
theorem :: Uogolnic i przenisc !!!
for A,B being Subset of TOP-REAL 2 st A meets B holds proj2.:A meets proj2.:B
proof
let A,B be Subset of TOP-REAL 2;
assume A meets B;
then consider e being object such that
A1: e in A and
A2: e in B by XBOOLE_0:3;
reconsider e as Point of TOP-REAL 2 by A1;
e`2 = proj2.e by PSCOMP_1:def 6;
then e`2 in proj2.:A & e`2 in proj2.:B by A1,A2,FUNCT_2:35;
hence thesis by XBOOLE_0:3;
end;
theorem
for A,B being Subset of TOP-REAL 2 st A misses B & A c= Vertical_Line
s & B c= Vertical_Line s holds proj2.:A misses proj2.:B
proof
let A,B being Subset of TOP-REAL 2 such that
A1: A misses B and
A2: A c= Vertical_Line s and
A3: B c= Vertical_Line s;
assume proj2.:A meets proj2.:B;
then consider e being object such that
A4: e in proj2.:A and
A5: e in proj2.:B by XBOOLE_0:3;
reconsider e as Real by A4;
consider d being Point of TOP-REAL 2 such that
A6: d in B and
A7: e = proj2.d by A5,FUNCT_2:65;
A8: d`1 = s by A3,A6,JORDAN6:31;
consider c being Point of TOP-REAL 2 such that
A9: c in A and
A10: e = proj2.c by A4,FUNCT_2:65;
c`1 = s by A2,A9,JORDAN6:31;
then c = |[d`1,c`2]| by A8,EUCLID:53
.= |[d`1,e]| by A10,PSCOMP_1:def 6
.= |[d`1,d`2]| by A7,PSCOMP_1:def 6
.= d by EUCLID:53;
hence contradiction by A1,A9,A6,XBOOLE_0:3;
end;
begin :: Goboards
theorem
1 <= i & i <= len G & 1 <= j & j <= width G implies G*(i,j) in LSeg(G*
(i,1),G*(i,width G))
proof
assume that
A1: 1 <= i & i <= len G and
A2: 1 <= j & j <= width G;
A3: G*(i,j)`2 <= G* (i,width G)`2 by A1,A2,SPRECT_3:12;
1 <= width G by A2,XXREAL_0:2;
then
A4: G*(i,1)`1 = G* (i,width G)`1 by A1,GOBOARD5:2;
G*(i,1)`1 = G*(i,j)`1 & G*(i,1)`2 <= G*(i,j)`2 by A1,A2,GOBOARD5:2
,SPRECT_3:12;
hence thesis by A4,A3,GOBOARD7:7;
end;
theorem
1 <= i & i <= len G & 1 <= j & j <= width G implies G*(i,j) in LSeg(G*
(1,j),G*(len G,j))
proof
assume that
A1: 1 <= i & i <= len G and
A2: 1 <= j & j <= width G;
A3: G*(i,j)`1 <= G* (len G,j)`1 by A1,A2,SPRECT_3:13;
1 <= len G by A1,XXREAL_0:2;
then
A4: G*(1,j)`2 = G*(len G,j)`2 by A2,GOBOARD5:1;
G*(1,j)`2 = G*(i,j)`2 & G*(1,j)`1 <= G*(i,j)`1 by A1,A2,GOBOARD5:1
,SPRECT_3:13;
hence thesis by A4,A3,GOBOARD7:8;
end;
theorem Th18:
1 <= j1 & j1 <= width G & 1 <= j2 & j2 <= width G & 1 <= i1 & i1
<= i2 & i2 <= len G implies G*(i1,j1)`1 <= G*(i2,j2)`1
proof
assume that
A1: 1 <= j1 & j1 <= width G and
A2: 1 <= j2 & j2 <= width G and
A3: 1 <= i1 & i1 <= i2 and
A4: i2 <= len G;
A5: 1 <= i2 by A3,XXREAL_0:2;
then G*(i2,j1)`1 = G*(i2,1)`1 by A1,A4,GOBOARD5:2
.= G*(i2,j2)`1 by A2,A4,A5,GOBOARD5:2;
hence thesis by A1,A3,A4,SPRECT_3:13;
end;
theorem Th19:
1 <= i1 & i1 <= len G & 1 <= i2 & i2 <= len G & 1 <= j1 & j1 <=
j2 & j2 <= width G implies G*(i1,j1)`2 <= G*(i2,j2)`2
proof
assume that
A1: 1 <= i1 & i1 <= len G and
A2: 1 <= i2 & i2 <= len G and
A3: 1 <= j1 & j1 <= j2 and
A4: j2 <= width G;
A5: 1 <= j2 by A3,XXREAL_0:2;
then G*(i1,j2)`2 = G*(1,j2)`2 by A1,A4,GOBOARD5:1
.= G*(i2,j2)`2 by A2,A4,A5,GOBOARD5:1;
hence thesis by A1,A3,A4,SPRECT_3:12;
end;
theorem Th20:
for f being non constant standard special_circular_sequence st f
is_sequence_on G & 1 <= t & t <= len G holds G*(t,width G)`2 >= N-bound L~f
proof
let f be non constant standard special_circular_sequence;
N-min L~f in rng f by SPRECT_2:39;
then consider x being object such that
A1: x in dom f and
A2: f.x = N-min L~f by FUNCT_1:def 3;
reconsider x as Nat by A1;
assume f is_sequence_on G;
then consider i,j such that
A3: [i,j] in Indices G and
A4: f/.x = G*(i,j) by A1,GOBOARD1:def 9;
A5: 1 <= i & i <= len G by A3,MATRIX_0:32;
assume
A6: 1 <= t & t <= len G;
1 <= j & j <= width G by A3,MATRIX_0:32;
then N-bound L~f = (N-min L~f)`2 & G*(t,width G)`2 >= G*(i,j)`2 by A6,A5,Th19
,EUCLID:52;
hence thesis by A1,A2,A4,PARTFUN1:def 6;
end;
theorem Th21:
for f being non constant standard special_circular_sequence st f
is_sequence_on G & 1 <= t & t <= width G holds G*(1,t)`1 <= W-bound L~f
proof
let f be non constant standard special_circular_sequence;
W-min L~f in rng f by SPRECT_2:43;
then consider x being object such that
A1: x in dom f and
A2: f.x = W-min L~f by FUNCT_1:def 3;
reconsider x as Nat by A1;
assume f is_sequence_on G;
then consider i,j such that
A3: [i,j] in Indices G and
A4: f/.x = G*(i,j) by A1,GOBOARD1:def 9;
A5: 1 <= i & i <= len G by A3,MATRIX_0:32;
assume
A6: 1 <= t & t <= width G;
1 <= j & j <= width G by A3,MATRIX_0:32;
then W-bound L~f = (W-min L~f)`1 & G*(1,t)`1 <= G*(i,j)`1 by A6,A5,Th18,
EUCLID:52;
hence thesis by A1,A2,A4,PARTFUN1:def 6;
end;
theorem Th22:
for f being non constant standard special_circular_sequence st f
is_sequence_on G & 1 <= t & t <= len G holds G*(t,1)`2 <= S-bound L~f
proof
let f be non constant standard special_circular_sequence;
S-min L~f in rng f by SPRECT_2:41;
then consider x being object such that
A1: x in dom f and
A2: f.x = S-min L~f by FUNCT_1:def 3;
reconsider x as Nat by A1;
assume f is_sequence_on G;
then consider i,j such that
A3: [i,j] in Indices G and
A4: f/.x = G*(i,j) by A1,GOBOARD1:def 9;
A5: 1 <= i & i <= len G by A3,MATRIX_0:32;
assume
A6: 1 <= t & t <= len G;
1 <= j & j <= width G by A3,MATRIX_0:32;
then S-bound L~f = (S-min L~f)`2 & G*(t,1)`2 <= G*(i,j)`2 by A6,A5,Th19,
EUCLID:52;
hence thesis by A1,A2,A4,PARTFUN1:def 6;
end;
theorem Th23:
for f being non constant standard special_circular_sequence st f
is_sequence_on G & 1 <= t & t <= width G holds G*(len G,t)`1 >= E-bound L~f
proof
let f be non constant standard special_circular_sequence;
E-min L~f in rng f by SPRECT_2:45;
then consider x being object such that
A1: x in dom f and
A2: f.x = E-min L~f by FUNCT_1:def 3;
reconsider x as Nat by A1;
assume f is_sequence_on G;
then consider i,j such that
A3: [i,j] in Indices G and
A4: f/.x = G*(i,j) by A1,GOBOARD1:def 9;
A5: 1 <= i & i <= len G by A3,MATRIX_0:32;
assume
A6: 1 <= t & t <= width G;
1 <= j & j <= width G by A3,MATRIX_0:32;
then E-bound L~f = (E-min L~f)`1 & G*(len G,t)`1 >= G*(i,j)`1 by A6,A5,Th18,
EUCLID:52;
hence thesis by A1,A2,A4,PARTFUN1:def 6;
end;
theorem Th24:
i<=len G & j<=width G implies cell(G,i,j) is non empty
proof
assume i<=len G & j<=width G;
then Int cell(G,i,j) is non empty by GOBOARD9:14;
hence thesis by TOPS_1:16,XBOOLE_1:3;
end;
theorem Th25:
i<=len G & j<=width G implies cell(G,i,j) is connected
proof
assume
A1: i<=len G & j<=width G;
then Int cell(G,i,j) is convex by GOBOARD9:17;
then Cl Int cell(G,i,j) is connected by CONNSP_1:19;
hence thesis by A1,GOBRD11:35;
end;
theorem Th26:
i <= len G implies cell(G,i,0) is not bounded
proof
assume
A1: i <= len G;
per cases by A1,NAT_1:14,XXREAL_0:1;
suppose
i = 0;
then
A2: cell(G,i,0) = { |[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,i,0) holds |.q.| < r
proof
let r be Real;
take q = |[min(-r,G*(1,1)`1),min(-r,G*(1,1)`2)]|;
A3: |.q`1.|<=|.q.| by JGRAPH_1:33;
min(-r,G*(1,1)`1) <= G*(1,1)`1 & min(-r,G*(1,1)`2) <= G*(1,1)`2 by
XXREAL_0:17;
hence q in cell(G,i,0) by A2;
per cases;
suppose
r <= 0;
hence thesis;
end;
suppose
A4: r > 0;
q`1 = min(-r,G*(1,1)`1) by EUCLID:52;
then
A5: |.-r.| <= |.q`1.| by A4,TOPREAL6:3,XXREAL_0:17;
--r > 0 by A4;
then -r < 0;
then --r <= |.q`1.| by A5,ABSVALUE:def 1;
hence thesis by A3,XXREAL_0:2;
end;
end;
hence thesis by JORDAN2C:34;
end;
suppose
A6: i >= 1 & i < len G;
then
A7: cell(G,i,0) = { |[r,s]| where r is Real, s is Real:
G*(i,1)`1 <= r & r <= G*(i+1,1)`1 & s <= G*(1,1)`2 } by GOBRD11:30;
not ex r being Real
st for q being Point of TOP-REAL 2 st q in cell(G,i,0) holds |.q.| < r
proof
let r be Real;
take q = |[G*(i,1)`1,min(-r,G*(1,1)`2)]|;
A8: min(-r,G*(1,1)`2) <= G*(1,1)`2 by XXREAL_0:17;
width G <> 0 by MATRIX_0:def 10;
then
A9: 1 <= width G by NAT_1:14;
i < i+1 & i+1 <= len G by A6,NAT_1:13;
then G*(i,1)`1 <= G*(i+1,1)`1 by A6,A9,GOBOARD5:3;
hence q in cell(G,i,0) by A7,A8;
A10: |.q`2.|<=|.q.| by JGRAPH_1:33;
per cases;
suppose
r <= 0;
hence thesis;
end;
suppose
A11: r > 0;
q`2 = min(-r,G*(1,1)`2) by EUCLID:52;
then
A12: |.-r.| <= |.q`2.| by A11,TOPREAL6:3,XXREAL_0:17;
--r > 0 by A11;
then -r < 0;
then --r <= |.q`2.| by A12,ABSVALUE:def 1;
hence thesis by A10,XXREAL_0:2;
end;
end;
hence thesis by JORDAN2C:34;
end;
suppose
i = len G;
then
A13: cell(G,i,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,i,0) holds |.q.| < r
proof
let r be Real;
take q = |[max(r,G*(len G,1)`1),G*(1,1)`2]|;
A14: |.q`1.|<=|.q.| by JGRAPH_1:33;
G*(len G,1)`1 <= max(r,G*(len G,1)`1) by XXREAL_0:25;
hence q in cell(G,i,0) by A13;
per cases;
suppose
r <= 0;
hence thesis;
end;
suppose
A15: r > 0;
q`1 = max(r,G*(len G,1)`1) by EUCLID:52;
then r <= q`1 by XXREAL_0:25;
then r <= |.q`1.| by A15,ABSVALUE:def 1;
hence thesis by A14,XXREAL_0:2;
end;
end;
hence thesis by JORDAN2C:34;
end;
end;
theorem Th27:
i <= len G implies cell(G,i,width G) is not bounded
proof
assume
A1: i <= len G;
per cases by A1,NAT_1:14,XXREAL_0:1;
suppose
A2: i = 0;
A3: cell(G,0,width G) = { |[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,width G) holds |.q.| < r
proof
let r be Real;
take q = |[min(-r,G*(1,1)`1),G*(1,width G)`2]|;
A4: |.q`1.|<=|.q.| by JGRAPH_1:33;
min(-r,G*(1,1)`1) <= G*(1,1)`1 by XXREAL_0:17;
hence q in cell(G,0,width G) by A3;
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 A2,JORDAN2C:34;
end;
suppose
A7: i >= 1 & i < len G;
then
A8: cell(G,i,width G) = { |[r,s]| where r is Real, s is Real:
G*(i,1)`1 <= r & r <= G*(i+1,1)`1 & G*(1,width G)`2 <= s } by
GOBRD11:31;
not ex r being Real st
for q being Point of TOP-REAL 2 st q in cell(G,i,width G) holds |.q.| < r
proof
let r be Real;
take q = |[G*(i,1)`1,max(r,G*(1,width G)`2)]|;
A9: max(r,G*(1,width G)`2) >= G*(1,width G)`2 by XXREAL_0:25;
width G <> 0 by MATRIX_0:def 10;
then
A10: 1 <= width G by NAT_1:14;
i < i+1 & i+1 <= len G by A7,NAT_1:13;
then G*(i,1)`1 <= G*(i+1,1)`1 by A7,A10,GOBOARD5:3;
hence q in cell(G,i,width G) by A8,A9;
A11: |.q`2.|<=|.q.| by JGRAPH_1:33;
per cases;
suppose
r <= 0;
hence thesis;
end;
suppose
A12: r > 0;
q`2 = max(r,G*(1,width G)`2) by EUCLID:52;
then q`2 >= r by XXREAL_0:25;
then r <= |.q`2.| by A12,ABSVALUE:def 1;
hence thesis by A11,XXREAL_0:2;
end;
end;
hence thesis by JORDAN2C:34;
end;
suppose
A13: i = len G;
A14: 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,i,width G) holds |.q.| < r
proof
let r be Real;
take q = |[max(r,G*(len G,1)`1),G*(1,width G)`2]|;
A15: |.q`1.|<=|.q.| by JGRAPH_1:33;
G*(len G,1)`1 <= max(r,G*(len G,1)`1) by XXREAL_0:25;
hence q in cell(G,i,width G) by A13,A14;
per cases;
suppose
r <= 0;
hence thesis;
end;
suppose
A16: r > 0;
q`1 = max(r,G*(len G,1)`1) by EUCLID:52;
then r <= q`1 by XXREAL_0:25;
then r <= |.q`1.| by A16,ABSVALUE:def 1;
hence thesis by A15,XXREAL_0:2;
end;
end;
hence thesis by JORDAN2C:34;
end;
end;
begin :: Gauges
theorem
width Gauge(D,n) = 2|^n + 3
proof
thus width Gauge(D,n) = len Gauge(D,n) by JORDAN8:def 1
.= 2|^n + 3 by JORDAN8:def 1;
end;
theorem
i < j implies len Gauge(D,i) < len Gauge(D,j)
proof
assume i < j;
then
A1: 2|^i < 2|^j by PEPIN:66;
len Gauge(D,i) = 2|^i + 3 & len Gauge(D,j) =2|^j + 3 by JORDAN8:def 1;
hence thesis by A1,XREAL_1:6;
end;
theorem
i <= j implies len Gauge(D,i) <= len Gauge(D,j)
proof
assume i <= j;
then
A1: 2|^i <= 2|^j by PREPOWER:93;
len Gauge(D,i) = 2|^i + 3 & len Gauge(D,j) =2|^j + 3 by JORDAN8:def 1;
hence thesis by A1,XREAL_1:6;
end;
theorem Th31:
m <= n & 1 < i & i < len Gauge(D,m) implies 1 < 2|^(n-'m)*(i-2)+
2 & 2|^(n-'m)*(i-2)+2 < len Gauge(D,n)
proof
assume that
A1: m <= n and
A2: 1 < i and
A3: i < len Gauge(D,m);
1+1 <= i by A2,NAT_1:13;
then reconsider i2 = i-2 as Element of NAT by INT_1:5;
0 < 2|^(n-'m)*(i2)+1;
then 0+1 < 2|^(n-'m)*(i-2)+1+1 by XREAL_1:6;
hence 1 < 2|^(n-'m)*(i-2)+2;
len Gauge(D,m) = 2|^m + (2+1) by JORDAN8:def 1
.= 2|^m + 2+1;
then i <= 2|^m + 2 by A3,NAT_1:13;
then i2 <= 2|^m by XREAL_1:20;
then 2|^(n-'m)*(i2) <= 2|^(n-'m)*2|^m by XREAL_1:64;
then 2|^(n-'m)*(i2) <= 2|^(n-'m+m) by NEWTON:8;
then 2|^(n-'m)*(i2) <= 2|^n by A1,XREAL_1:235;
then 2|^(n-'m)*(i2) < 2|^n + 1 by NAT_1:13;
then 2|^(n-'m)*(i-2)+2 < 2|^n + 1+2 by XREAL_1:6;
then 2|^(n-'m)*(i-2)+2 < 2|^n + (1+2);
hence thesis by JORDAN8:def 1;
end;
theorem Th32:
m <= n & 1 < i & i < width Gauge(D,m) implies 1 < 2|^(n-'m)*(i-2
)+2 & 2|^(n-'m)*(i-2)+2 < width Gauge(D,n)
proof
len Gauge(D,n) = width Gauge(D,n) & len Gauge(D,m) = width Gauge(D,m) by
JORDAN8:def 1;
hence thesis by Th31;
end;
theorem Th33:
m <= n & 1 < i & i < len Gauge(D,m) & 1 < j & j < width Gauge(D,
m) implies for i1,j1 being Nat st i1 = 2|^(n-'m)*(i-2)+2 & j1 = 2|^(
n-'m)*(j-2)+2 holds Gauge(D,m)*(i,j) = Gauge(D,n)*(i1,j1)
proof
assume that
A1: m <= n and
A2: 1 < i & i < len Gauge(D,m) and
A3: 1 < j & j < width Gauge(D,m);
let i1,j1 be Nat such that
A4: i1 = 2|^(n-'m)*(i-2)+2 and
A5: j1 = 2|^(n-'m)*(j-2)+2;
A6: 1 < i1 & i1 < len Gauge(D,n) by A1,A2,A4,Th31;
(j-2)/(2|^m) = (j-2)/(2|^(n-'(n-'m))) by A1,NAT_D:58
.= (j-2)/((2|^n)/(2|^(n-'m))) by NAT_D:50,TOPREAL6:10
.= (j1-2)/(2|^n) by A5,XCMPLX_1:77;
then
A7: (((N-bound D)-(S-bound D))/(2|^m))*(j-2) = ((N-bound D)-(S-bound D))*((
j1-2)/(2|^n)) by XCMPLX_1:75
.= (((N-bound D)-(S-bound D))/(2|^n))*(j1-2) by XCMPLX_1:75;
(i-2)/(2|^m) = (i-2)/(2|^(n-'(n-'m))) by A1,NAT_D:58
.= (i-2)/((2|^n)/(2|^(n-'m))) by NAT_D:50,TOPREAL6:10
.= (i1-2)/(2|^n) by A4,XCMPLX_1:77;
then
A8: (((E-bound D)-(W-bound D))/(2|^m))*(i-2) = ((E-bound D)-(W-bound D))*((
i1-2)/(2|^n)) by XCMPLX_1:75
.= (((E-bound D)-(W-bound D))/(2|^n))*(i1-2) by XCMPLX_1:75;
1 < j1 & j1 < width Gauge(D,n) by A1,A3,A5,Th32;
then
A9: [i1,j1] in Indices Gauge(D,n) by A6,MATRIX_0:30;
[i,j] in Indices Gauge(D,m) by A2,A3,MATRIX_0:30;
hence
Gauge(D,m)*(i,j) = |[(W-bound D)+(((E-bound D)-(W-bound D))/(2|^m))*(i-
2), (S-bound D)+(((N-bound D)-(S-bound D))/(2|^m))*(j-2)]| by JORDAN8:def 1
.= Gauge(D,n)*(i1,j1) by A9,A8,A7,JORDAN8:def 1;
end;
theorem Th34:
m <= n & 1 < i & i+1 < len Gauge(D,m) implies 1 < 2|^(n-'m)*(i-1
)+2 & 2|^(n-'m)*(i-1)+2 <= len Gauge(D,n)
proof
assume that
A1: m <= n and
A2: 1 < i and
A3: i+1 < len Gauge(D,m);
reconsider i2 = i-1 as Element of NAT by A2,INT_1:5;
0 < 2|^(n-'m)*(i2)+1;
then 0+1 < 2|^(n-'m)*(i-1)+1+1 by XREAL_1:6;
hence 1 < 2|^(n-'m)*(i-1)+2;
len Gauge(D,m) = 2|^m + (2+1) by JORDAN8:def 1
.= 2|^m + 2+1;
then i+1 <= 2|^m + 1 + 1 by A3,NAT_1:13;
then i <= 2|^m + 1 by XREAL_1:6;
then i2 <= 2|^m by XREAL_1:20;
then 2|^(n-'m)*(i2) <= 2|^(n-'m)*2|^m by XREAL_1:64;
then 2|^(n-'m)*(i2) <= 2|^(n-'m+m) by NEWTON:8;
then 2|^(n-'m)*(i2) <= 2|^n by A1,XREAL_1:235;
then 2|^(n-'m)*(i2) <= 2|^n + 1 by NAT_1:13;
then 2|^(n-'m)*(i-1)+2 <= 2|^n + 1+2 by XREAL_1:6;
then 2|^(n-'m)*(i-1)+2 <= 2|^n + (1+2);
hence thesis by JORDAN8:def 1;
end;
theorem Th35:
m <= n & 1 < i & i+1 < width Gauge(D,m) implies 1 < 2|^(n-'m)*(i
-1)+2 & 2|^(n-'m)*(i-1)+2 <= width Gauge(D,n)
proof
len Gauge(D,n) = width Gauge(D,n) & len Gauge(D,m) = width Gauge(D,m) by
JORDAN8:def 1;
hence thesis by Th34;
end;
Lm3: now
let D, n;
set G = Gauge(D,n);
0 + 1 <= len G div 2 + 1 by XREAL_1:6;
hence 1 <= Center G;
0 < len G by JORDAN8:10;
then len G div 2 < len G by INT_1:56;
hence Center G <= len G by NAT_1:13;
end;
Lm4: now
let D, n, j;
set G = Gauge(D,n);
assume
A1: 1 <= j & j <= len G;
A2: len G = width G & 0 + 1 <= len G div 2 + 1 by JORDAN8:def 1,XREAL_1:6;
Center G <= len G by Lm3;
hence [Center G,j] in Indices G by A1,A2,MATRIX_0:30;
end;
Lm5: now
let D, n, j;
set G = Gauge(D,n);
assume
A1: 1 <= j & j <= len G;
A2: len G = width G & 0 + 1 <= len G div 2 + 1 by JORDAN8:def 1,XREAL_1:6;
Center G <= len G by Lm3;
hence [j,Center G] in Indices G by A1,A2,MATRIX_0:30;
end;
Lm6: for w being Real holds n > 0 implies w/(2|^n)*(Center Gauge(D,n) -
2) = w/2
proof
let w be Real;
set G = Gauge(D,n);
A1: 2|^n <> 0 by NEWTON:83;
assume
A2: n > 0;
then
A3: 2|^n mod 2 = 0 by PEPIN:36;
thus w/(2|^n)*(Center G - 2) = w/(2|^n)*((2|^n + 3) div 2 + 1 - 2) by
JORDAN8:def 1
.= w/(2|^n)*((2|^n + 3) div 2 + (1 - 2))
.= w/(2|^n)*((2|^n div 2) + 1 +- 1) by A3,Lm1,NAT_D:19
.= w/(2|^n)*(2|^n / 2) by A2,PEPIN:64
.= w/2 by A1,XCMPLX_1:98;
end;
Lm7: now
let m, n;
let c, d be Real;
assume
A1: 0 <= c;
assume m <= n;
then 0 < 2|^m & 2|^m <= 2|^n by NEWTON:83,PREPOWER:93;
hence c/(2|^n) <= c/(2|^m) by A1,XREAL_1:118;
end;
Lm8: for m,n for c,d being Real st 0 <= c & m <= n
holds d+c/2|^n <= d+c/2|^m by XREAL_1:6,Lm7;
Lm9: now
let m, n;
let c, d be Real;
assume 0 <= c & m <= n;
then c/(2|^n) <= c/(2|^m) by Lm7;
hence d-c/2|^m <= d-c/2|^n by XREAL_1:13;
end;
theorem Th36:
1 <= i & i <= len Gauge (D,n) & 1 <= j & j <= len Gauge (D,m) &
(n > 0 & m > 0 or n = 0 & m = 0) implies Gauge(D,n)*(Center Gauge(D,n), i)`1 =
Gauge(D,m)*(Center Gauge(D,m), j)`1
proof
set a = N-bound D, s = S-bound D, w = W-bound D, e = E-bound D, G = Gauge(D,
n), M = Gauge(D,m);
assume 1 <= i & i <= len G;
then
A1: [Center G,i] in Indices G by Lm4;
assume 1 <= j & j <= len M;
then
A2: [Center M,j] in Indices M by Lm4;
assume
A3: n > 0 & m > 0 or n = 0 & m = 0;
per cases by A3;
suppose that
A4: n > 0 and
A5: m > 0;
thus G*(Center G,i)`1 = |[w+(e-w)/(2|^n)*(Center G - 2), s+(a-s)/(2|^n)*(i
- 2)]|`1 by A1,JORDAN8:def 1
.= w+(e-w)/(2|^n)*(Center G - 2) by EUCLID:52
.= w+(e-w)/2 by A4,Lm6
.= w+(e-w)/(2|^m)*(Center M - 2) by A5,Lm6
.= |[w+(e-w)/(2|^m)*(Center M - 2), s+(a-s)/(2|^m)*(j - 2)]|`1 by
EUCLID:52
.= M*(Center M,j)`1 by A2,JORDAN8:def 1;
end;
suppose
A6: n = 0 & m = 0;
thus G*(Center G,i)`1 = |[w+(e-w)/(2|^n)*(Center G - 2), s+(a-s)/(2|^n)*(i
- 2)]|`1 by A1,JORDAN8:def 1
.= w+(e-w)/(2|^m)*(Center M - 2) by A6,EUCLID:52
.= |[w+(e-w)/(2|^m)*(Center M - 2), s+(a-s)/(2|^m)*(j - 2)]|`1 by
EUCLID:52
.= M*(Center M,j)`1 by A2,JORDAN8:def 1;
end;
end;
theorem
1 <= i & i <= len Gauge (D,n) & 1 <= j & j <= len Gauge (D,m) & (n > 0
& m > 0 or n = 0 & m = 0) implies Gauge(D,n)*(i, Center Gauge(D,n))`2 = Gauge(D
,m)*(j, Center Gauge(D,m))`2
proof
set a = N-bound D, s = S-bound D, w = W-bound D, e = E-bound D, G = Gauge(D,
n), M = Gauge(D,m);
assume 1 <= i & i <= len G;
then
A1: [i,Center G] in Indices G by Lm5;
assume 1 <= j & j <= len M;
then
A2: [j,Center M] in Indices M by Lm5;
assume
A3: n > 0 & m > 0 or n = 0 & m = 0;
per cases by A3;
suppose that
A4: n > 0 and
A5: m > 0;
thus G*(i,Center G)`2 = |[w+(e-w)/(2|^n)*(i - 2), s+(a-s)/(2|^n)*(Center G
- 2)]|`2 by A1,JORDAN8:def 1
.= s+(a-s)/(2|^n)*(Center G - 2) by EUCLID:52
.= s+(a-s)/2 by A4,Lm6
.= s+(a-s)/(2|^m)*(Center M - 2) by A5,Lm6
.= |[w+(e-w)/(2|^m)*(j - 2), s+(a-s)/(2|^m)*(Center M - 2)]|`2 by
EUCLID:52
.= M*(j,Center M)`2 by A2,JORDAN8:def 1;
end;
suppose
A6: n = 0 & m = 0;
thus G*(i,Center G)`2 = |[w+(e-w)/(2|^n)*(i - 2), s+(a-s)/(2|^n)*(Center G
- 2)]|`2 by A1,JORDAN8:def 1
.= s+(a-s)/(2|^m)*(Center M - 2) by A6,EUCLID:52
.= |[w+(e-w)/(2|^m)*(j - 2), s+(a-s)/(2|^m)*(Center M - 2)]|`2 by
EUCLID:52
.= M*(j,Center M)`2 by A2,JORDAN8:def 1;
end;
end;
Lm10: now
let D, n;
let e, w be Real;
A1: 2|^n <> 0 by NEWTON:83;
thus w+(e-w)/(2|^n)*(len Gauge(D,n)-2) = w+(e-w)/(2|^n)*(2|^n+3-2) by
JORDAN8:def 1
.= w+(e-w)/(2|^n)*2|^n+(e-w)/(2|^n)
.= w+(e-w)+(e-w)/(2|^n) by A1,XCMPLX_1:87
.= e+(e-w)/(2|^n);
end;
Lm11: now
let D, n, i;
set a = N-bound D, s = S-bound D, w = W-bound D, e = E-bound D, G = Gauge(D,
n);
assume [i,1] in Indices G;
hence G*(i,1)`2 = |[w+(e-w)/(2|^n)*(i - 2), s+(a-s)/(2|^n)*(1 - 2)]|`2 by
JORDAN8:def 1
.= s-(a-s)/(2|^n) by EUCLID:52;
end;
Lm12: now
let D, n, i;
set a = N-bound D, s = S-bound D, w = W-bound D, e = E-bound D, G = Gauge(D,
n);
assume [1,i] in Indices G;
hence G*(1,i)`1 = |[w+(e-w)/(2|^n)*(1 - 2), s+(a-s)/(2|^n)*(i - 2)]|`1 by
JORDAN8:def 1
.= w-(e-w)/(2|^n) by EUCLID:52;
end;
Lm13: now
let D, n, i;
set a = N-bound D, s = S-bound D, w = W-bound D, e = E-bound D, G = Gauge(D,
n);
assume [i,len G] in Indices G;
hence G*(i,len G)`2 = |[w+(e-w)/(2|^n)*(i - 2), s+(a-s)/(2|^n)*(len G - 2)]|
`2 by JORDAN8:def 1
.= s+(a-s)/(2|^n)*(len G-2) by EUCLID:52
.= a+(a-s)/(2|^n) by Lm10;
end;
Lm14: now
let D, n, i;
set a = N-bound D, s = S-bound D, w = W-bound D, e = E-bound D, G = Gauge(D,
n);
assume [len G,i] in Indices G;
hence G*(len G,i)`1 = |[w+(e-w)/(2|^n)*(len G - 2), s+(a-s)/(2|^n)*(i - 2)]|
`1 by JORDAN8:def 1
.= w+(e-w)/(2|^n)*(len G-2) by EUCLID:52
.= e+(e-w)/(2|^n) by Lm10;
end;
theorem
1 <= i & i <= len Gauge(C,1) implies Gauge(C,1)*(Center Gauge(C,1),i)
`1 = (W-bound C + E-bound C) / 2
proof
set a = N-bound C, s = S-bound C, w = W-bound C, e = E-bound C, G = Gauge(C,
1);
assume 1 <= i & i <= len G;
then [Center G,i] in Indices G by Lm4;
hence
G*(Center G,i)`1 = |[w+((e-w)/(2|^1))*(Center G-2),s+((a-s)/(2|^1))*(i-
2)]|`1 by JORDAN8:def 1
.= w+(e-w)/(2|^1)*(Center G-2) by EUCLID:52
.= w+(e-w)/2 by Lm6
.= (w + e) / 2;
end;
theorem
1 <= i & i <= len Gauge(C,1) implies Gauge(C,1)*(i,Center Gauge(C,1))
`2 = (S-bound C + N-bound C) / 2
proof
set a = N-bound C, s = S-bound C, w = W-bound C, e = E-bound C, G = Gauge(C,
1);
assume 1 <= i & i <= len G;
then [i,Center G] in Indices G by Lm5;
hence
G*(i,Center G)`2 = |[w+((e-w)/(2|^1))*(i-2),s+((a-s)/(2|^1))*(Center G-
2)]|`2 by JORDAN8:def 1
.= s+(a-s)/(2|^1)*(Center G-2) by EUCLID:52
.= s+(a-s)/2 by Lm6
.= (s + a) / 2;
end;
theorem Th40:
1 <= i & i <= len Gauge(E,n) & 1 <= j & j <= len Gauge(E,m) & m
<= n implies Gauge(E,n)*(i,len Gauge(E,n))`2 <= Gauge(E,m)*(j,len Gauge(E,m))`2
proof
set a = N-bound E, s = S-bound E, G = Gauge(E,n), M = Gauge(E,m);
assume that
A1: 1 <= i & i <= len G and
A2: 1 <= j & j <= len M and
A3: m <= n;
A4: len M = width M by JORDAN8:def 1;
1 <= len M by A2,XXREAL_0:2;
then [j,len M] in Indices M by A2,A4,MATRIX_0:30;
then
A5: M*(j,len M)`2 = a+(a-s)/(2|^m) by Lm13;
A6: len G = width G by JORDAN8:def 1;
1 <= len G by A1,XXREAL_0:2;
then [i,len G] in Indices G by A1,A6,MATRIX_0:30;
then 0 < a - s & G*(i,len G)`2 = a+(a-s)/(2|^n) by Lm13,SPRECT_1:32
,XREAL_1:50;
hence thesis by A3,A5,Lm8;
end;
theorem
1 <= i & i <= len Gauge(E,n) & 1 <= j & j <= len Gauge(E,m) & m <= n
implies Gauge(E,n)*(len Gauge(E,n),i)`1 <= Gauge(E,m)*(len Gauge(E,m),j)`1
proof
set w = W-bound E, e = E-bound E, G = Gauge(E,n), M = Gauge(E,m);
assume that
A1: 1 <= i & i <= len G and
A2: 1 <= j & j <= len M and
A3: m <= n;
A4: len M = width M by JORDAN8:def 1;
1 <= len M by A2,XXREAL_0:2;
then [len M,j] in Indices M by A2,A4,MATRIX_0:30;
then
A5: M*(len M,j)`1 = e+(e-w)/(2|^m) by Lm14;
A6: len G = width G by JORDAN8:def 1;
1 <= len G by A1,XXREAL_0:2;
then [len G,i] in Indices G by A1,A6,MATRIX_0:30;
then 0 < e - w & G*(len G,i)`1 = e+(e-w)/(2|^n) by Lm14,SPRECT_1:31
,XREAL_1:50;
hence thesis by A3,A5,Lm8;
end;
theorem
1 <= i & i <= len Gauge(E,n) & 1 <= j & j <= len Gauge(E,m) & m <= n
implies Gauge(E,m)*(1,j)`1 <= Gauge(E,n)*(1,i)`1
proof
set w = W-bound E, e = E-bound E, G = Gauge(E,n), M = Gauge(E,m);
assume that
A1: 1 <= i & i <= len G and
A2: 1 <= j & j <= len M and
A3: m <= n;
A4: len M = width M by JORDAN8:def 1;
1 <= len M by A2,XXREAL_0:2;
then [1,j] in Indices M by A2,A4,MATRIX_0:30;
then
A5: M*(1,j)`1 = w-(e-w)/(2|^m) by Lm12;
A6: len G = width G by JORDAN8:def 1;
1 <= len G by A1,XXREAL_0:2;
then [1,i] in Indices G by A1,A6,MATRIX_0:30;
then 0 < e - w & G*(1,i)`1 = w-(e-w)/(2|^n) by Lm12,SPRECT_1:31,XREAL_1:50;
hence thesis by A3,A5,Lm9;
end;
theorem
1 <= i & i <= len Gauge(E,n) & 1 <= j & j <= len Gauge(E,m) & m <= n
implies Gauge(E,m)*(j,1)`2 <= Gauge(E,n)*(i,1)`2
proof
set a = N-bound E, s = S-bound E, G = Gauge(E,n), M = Gauge(E,m);
assume that
A1: 1 <= i & i <= len G and
A2: 1 <= j & j <= len M and
A3: m <= n;
A4: len M = width M by JORDAN8:def 1;
1 <= len M by A2,XXREAL_0:2;
then [j,1] in Indices M by A2,A4,MATRIX_0:30;
then
A5: M*(j,1)`2 = s-(a-s)/(2|^m) by Lm11;
A6: len G = width G by JORDAN8:def 1;
1 <= len G by A1,XXREAL_0:2;
then [i,1] in Indices G by A1,A6,MATRIX_0:30;
then 0 < a - s & G*(i,1)`2 = s-(a-s)/(2|^n) by Lm11,SPRECT_1:32,XREAL_1:50;
hence thesis by A3,A5,Lm9;
end;
theorem
1 <= m & m <= n implies LSeg(Gauge(E,n)*(Center Gauge(E,n),1), Gauge(E
,n)*(Center Gauge(E,n),len Gauge(E,n))) c= LSeg(Gauge(E,m)*(Center Gauge(E,m),1
), Gauge(E,m)*(Center Gauge(E,m),len Gauge(E,m)))
proof
set a = N-bound E, s = S-bound E, G = Gauge(E,n), M = Gauge(E,m), sn =
Center G, sm = Center M;
assume
A1: 1 <= m;
A2: 1 <= len M by GOBRD11:34;
then [sm,1] in Indices M by Lm4;
then
A3: M*(sm,1)`2 = s-(a-s)/(2|^m) by Lm11;
[sm,len M] in Indices M by A2,Lm4;
then
A4: M*(sm,len M)`2 = a+(a-s)/(2|^m) by Lm13;
A5: sn <= len G by Lm3;
A6: 1 <= len G by GOBRD11:34;
assume
A7: m <= n;
then
A8: M*(sm,1)`1 = G*(sn,len G)`1 & G*(sn,len G)`1 = M*(sm,len M)`1 by A1,A6,A2
,Th36;
0 < a - s by SPRECT_1:32,XREAL_1:50;
then
A9: (a-s)/(2|^n) <= (a-s)/(2|^m) by A7,Lm7;
len G = width G & 1 <= sn by Lm3,JORDAN8:def 1;
then
A10: G*(sn,1)`2 <= G*(sn,len G)`2 by A6,A5,SPRECT_3:12;
[sn,len G] in Indices G by A6,Lm4;
then G*(sn,len G)`2 = a+(a-s)/(2|^n) by Lm13;
then
A11: G*(sn,len G)`2 <= M*(sm,len M)`2 by A9,A4,XREAL_1:7;
then
A12: G*(sn,1)`2 <= M*(sm,len M)`2 by A10,XXREAL_0:2;
[sn,1] in Indices G by A6,Lm4;
then G*(sn,1)`2 = s-(a-s)/(2|^n) by Lm11;
then
A13: M*(sm,1)`2 <= G*(sn,1)`2 by A9,A3,XREAL_1:13;
then M*(sm,1)`2 <= G*(sn,len G)`2 by A10,XXREAL_0:2;
then
A14: G*(sn,len G) in LSeg(M*(sm,1),M*(sm,len M)) by A11,A8,GOBOARD7:7;
M*(sm,1)`1 = G*(sn,1)`1 & G*(sn,1)`1 = M*(sm,len M)`1 by A1,A7,A6,A2,Th36;
then G*(sn,1) in LSeg(M*(sm,1),M*(sm,len M)) by A13,A12,GOBOARD7:7;
hence thesis by A14,TOPREAL1:6;
end;
theorem
1 <= m & m <= n & 1 <= j & j <= width Gauge(E,n) implies LSeg(Gauge(E,
n)*(Center Gauge(E,n),1), Gauge(E,n)*(Center Gauge(E,n),j)) c= LSeg(Gauge(E,m)*
(Center Gauge(E,m),1), Gauge(E,n)*(Center Gauge(E,n),j))
proof
set a = N-bound E, s = S-bound E, w = W-bound E, e = E-bound E, G = Gauge(E,
n), M = Gauge(E,m), sn = Center G, sm = Center M;
assume that
A1: 1 <= m and
A2: m <= n and
A3: 1 <= j and
A4: j <= width G;
now
A5: 0 < a - s by SPRECT_1:32,XREAL_1:50;
then
A6: s-(a-s)/(2|^m) <= s-0 by XREAL_1:13;
A7: (a-s)/(2|^n) <= (a-s)/(2|^m) by A2,A5,Lm7;
A8: 1 <= len M by GOBRD11:34;
then [sm,1] in Indices M by Lm4;
then
A9: M*(sm,1)`2 = s-(a-s)/(2|^m) by Lm11;
let t be Nat;
assume that
A10: 1 <= t and
A11: t <= j;
1 <= sn & sn <= len G by Lm3;
then
A12: G*(sn,t)`2 <= G*(sn,j)`2 by A4,A10,A11,SPRECT_3:12;
A13: len G = width G by JORDAN8:def 1;
then
A14: t <= len G by A4,A11,XXREAL_0:2;
then
A15: M*(sm,1)`1 = G*(sn,t)`1 by A1,A2,A10,A8,Th36;
A16: [sn,t] in Indices G by A10,A14,Lm4;
then
A17: G*(sn,t)`2 = |[w+(e-w)/(2|^n)*(sn - 2), s+(a-s)/(2|^n)*(t - 2)]| `2
by JORDAN8:def 1
.= s+(a-s)/(2|^n)*(t-2) by EUCLID:52;
A18: now
per cases by A10,XXREAL_0:1;
suppose
t = 1;
then G*(sn,t)`2 = s-(a-s)/(2|^n) by A16,Lm11;
hence M*(sm,1)`2 <= G*(sn,t)`2 by A7,A9,XREAL_1:13;
end;
suppose
t > 1;
then t >= 1+1 by NAT_1:13;
then t-2 >= 2-2 by XREAL_1:9;
then s+0 <= s+(a-s)/(2|^n)*(t-2) by A5,XREAL_1:6;
hence M*(sm,1)`2 <= G*(sn,t)`2 by A17,A6,A9,XXREAL_0:2;
end;
end;
G*(sn,t)`1 = G*(sn,j)`1 by A1,A2,A3,A4,A10,A13,A14,Th36;
hence G*(sn,t) in LSeg(M*(sm,1),G*(sn,j)) by A15,A18,A12,GOBOARD7:7;
end;
then
G*(sn,1) in LSeg(M*(sm,1),G*(sn,j)) & G*(sn,j) in LSeg(M*(sm,1),G*(sn,j
)) by A3;
hence thesis by TOPREAL1:6;
end;
theorem
1 <= m & m <= n & 1 <= j & j <= width Gauge(E,n) implies LSeg(Gauge(E,
m)*(Center Gauge(E,m),1), Gauge(E,n)*(Center Gauge(E,n),j)) c= LSeg(Gauge(E,m)*
(Center Gauge(E,m),1), Gauge(E,m)*(Center Gauge(E,m),len Gauge(E,m)))
proof
set a = N-bound E, s = S-bound E, w = W-bound E, e = E-bound E, G = Gauge(E,
n), M = Gauge(E,m), sn = Center G, sm = Center M;
assume that
A1: 1 <= m and
A2: m <= n and
A3: 1 <= j and
A4: j <= width G;
A5: 1 <= sm & sm <= len M by Lm3;
A6: 1 <= sn & sn <= len G by Lm3;
then
A7: G*(sn,len G)`2 <= M*(sm,len M)`2 by A2,A5,Th40;
len G = width G by JORDAN8:def 1;
then G*(sn,j)`2 <= G*(sn,len G)`2 by A3,A4,A6,SPRECT_3:12;
then
A8: G*(sn,j)`2 <= M*(sm,len M)`2 by A7,XXREAL_0:2;
A9: 0 < a - s by SPRECT_1:32,XREAL_1:50;
then
A10: s-(a-s)/(2|^m) <= s-0 by XREAL_1:13;
A11: 1 <= len M by GOBRD11:34;
then [sm,1] in Indices M by Lm4;
then
A12: M*(sm,1)`2 = s-(a-s)/(2|^m) by Lm11;
A13: (a-s)/(2|^n) <= (a-s)/(2|^m) by A2,A9,Lm7;
A14: len G = width G by JORDAN8:def 1;
then
A15: [sn,j] in Indices G by A3,A4,Lm4;
then
A16: G*(sn,j)`2 = |[w+(e-w)/(2|^n)*(sn - 2), s+(a-s)/(2|^n)*(j - 2)]|`2 by
JORDAN8:def 1
.= s+(a-s)/(2|^n)*(j-2) by EUCLID:52;
A17: now
per cases by A3,XXREAL_0:1;
suppose
j = 1;
then G*(sn,j)`2 = s-(a-s)/(2|^n) by A15,Lm11;
hence M*(sm,1)`2 <= G*(sn,j)`2 by A13,A12,XREAL_1:13;
end;
suppose
j > 1;
then j >= 1+1 by NAT_1:13;
then j-2 >= 2-2 by XREAL_1:9;
then s+0 <= s+(a-s)/(2|^n)*(j-2) by A9,XREAL_1:6;
hence M*(sm,1)`2 <= G*(sn,j)`2 by A12,A16,A10,XXREAL_0:2;
end;
end;
len M = width M by JORDAN8:def 1;
then
A18: M*(sm,1)`2 <= M*(sm,len M)`2 by A11,A5,SPRECT_3:12;
M*(sm,1)`1 = M*(sm,len M)`1 by A1,A11,Th36;
then
A19: M*(sm,1) in LSeg(M*(sm,1),M*(sm,len M)) by A18,GOBOARD7:7;
M*(sm,1)`1 = G*(sn,j)`1 & G*(sn,j)`1 = M*(sm,len M)`1 by A1,A2,A3,A4,A11,A14
,Th36;
then G*(sn,j) in LSeg(M*(sm,1),M*(sm,len M)) by A17,A8,GOBOARD7:7;
hence thesis by A19,TOPREAL1:6;
end;
theorem Th47:
m <= n & 1 < i & i+1 < len Gauge(E,m) & 1 < j & j+1 < width
Gauge(E,m) implies for i1,j1 being Nat st 2|^(n-'m)*(i-2)+2 <= i1 &
i1 < 2|^(n-'m)*(i-1)+2 & 2|^(n-'m)*(j-2)+2 <= j1 & j1 < 2|^(n-'m)*(j-1)+2 holds
cell(Gauge(E,n),i1,j1) c= cell(Gauge(E,m),i,j)
proof
set G = Gauge(E,m), G1 = Gauge(E,n);
assume that
A1: m <= n and
A2: 1 < i and
A3: i+1 < len G and
A4: 1 < j and
A5: j+1 < width G;
set i2 = 2|^(n-'m)*(i-'2)+2, j2 = 2|^(n-'m)*(j-'2)+2, i3 = 2|^(n-'m)*(i-'1)+
2, j3 = 2|^(n-'m)*(j-'1)+2;
let i1,j1 be Nat such that
A6: 2|^(n-'m)*(i-2)+2 <= i1 and
A7: i1 < 2|^(n-'m)*(i-1)+2 and
A8: 2|^(n-'m)*(j-2)+2 <= j1 and
A9: j1 < 2|^(n-'m)*(j-1)+2;
A10: j-1 = j-'1 by A4,XREAL_1:233;
then
A11: j3 <= width G1 by A1,A4,A5,Th35;
A12: 1+1 <= i by A2,NAT_1:13;
then
A13: i2 = 2|^(n-'m)*(i-2)+2 by XREAL_1:233;
i < i+1 by XREAL_1:29;
then
A14: i < len G by A3,XXREAL_0:2;
then
A15: 1 <= 2|^(n-'m)*(i-2)+2 by A1,A2,Th31;
then
A16: 1 <= i1 by A6,XXREAL_0:2;
j1+1 <= 2|^(n-'m)*(j-'1)+2 by A9,A10,NAT_1:13;
then
A17: j1+1 < j3 or j1+1 = j3 by XXREAL_0:1;
let e be object;
assume
A18: e in cell(G1,i1,j1);
then reconsider p = e as Point of TOP-REAL 2;
2|^(n-'m)*(i-1)+2 <= len G1 by A1,A2,A3,Th34;
then
A19: i1 < len G1 by A7,XXREAL_0:2;
then
A20: i1+1 <= len G1 by NAT_1:13;
A21: j+1-(1+1) = j-1 .= j-'1 by A4,XREAL_1:233;
1 < j+1 by A4,XREAL_1:29;
then
A22: G*(i,j+1) = G1*(i2,j3) by A1,A2,A5,A14,A21,A13,Th33;
A23: i-1 = i-'1 by A2,XREAL_1:233;
then
A24: i3 <= len G1 by A1,A2,A3,Th34;
i1+1 <= 2|^(n-'m)*(i-'1)+2 by A7,A23,NAT_1:13;
then
A25: i1+1 < i3 or i1+1 = i3 by XXREAL_0:1;
A26: i2 = 2|^(n-'m)*(i-2)+2 by A12,XREAL_1:233;
A27: i+1-(1+1) = i-1 .= i-'1 by A2,XREAL_1:233;
A28: i2 = 2|^(n-'m)*(i-2)+2 by A12,XREAL_1:233;
then
A29: i2 <= len G1 by A6,A19,XXREAL_0:2;
j < j+1 by XREAL_1:29;
then
A30: j < width G by A5,XXREAL_0:2;
then
A31: 1 <= 2|^(n-'m)*(j-2)+2 by A1,A4,Th32;
then
A32: 1 <= j1 by A8,XXREAL_0:2;
then 1 < j1+1 by NAT_1:13;
then
A33: G1*(i1,j1+1)`2 <= G1*(i1,j3)`2 by A19,A16,A11,A17,GOBOARD5:4;
2|^(n-'m)*(j-1)+2 <= width G1 by A1,A4,A5,Th35;
then
A34: j1 < width G1 by A9,XXREAL_0:2;
then
A35: j1+1 <= width G1 by NAT_1:13;
then
A36: G1*(i1,j1)`1 <= p`1 by A18,A20,A16,A32,JORDAN9:17;
A37: 1+1 <= j by A4,NAT_1:13;
then
A38: j2 = 2|^(n-'m)*(j-2)+2 by XREAL_1:233;
then j2 < j1 or j2 = j1 by A8,XXREAL_0:1;
then
A39: G1*(i1,j2)`2 <= G1*(i1,j1)`2 by A19,A34,A16,A31,A38,GOBOARD5:4;
A40: j2 = 2|^(n-'m)*(j-2)+2 by A37,XREAL_1:233;
then
A41: G*(i,j) = Gauge(E,n)*(i2,j2) by A1,A2,A4,A14,A30,A28,Th33;
1 < i+1 by A2,XREAL_1:29;
then
A42: G*(i+1,j) = G1*(i3,j2) by A1,A3,A4,A30,A27,A38,Th33;
A43: p`1 <= G1*(i1+1,j1)`1 by A18,A20,A35,A16,A32,JORDAN9:17;
1 < i1+1 by A16,NAT_1:13;
then
A44: G1*(i1+1,j1)`1 <= G1*(i3,j1)`1 by A34,A32,A24,A25,GOBOARD5:3;
A45: G1*(i1,j1)`2 <= p`2 by A18,A20,A35,A16,A32,JORDAN9:17;
A46: j2 <= width G1 by A8,A34,A40,XXREAL_0:2;
then G1*(i1,j2)`2 = G1*(1,j2)`2 by A19,A16,A31,A38,GOBOARD5:1
.= G1*(i2,j2)`2 by A15,A31,A29,A46,A26,A38,GOBOARD5:1;
then
A47: G*(i,j)`2 <= p`2 by A45,A41,A39,XXREAL_0:2;
A48: p`2 <= G1* (i1,j1+1)`2 by A18,A20,A35,A16,A32,JORDAN9:17;
A49: 1 < j3 by A9,A32,A10,XXREAL_0:2;
then G1*(i1,j3)`2 = G1*(1,j3)`2 by A19,A16,A11,GOBOARD5:1
.= G1*(i2,j3)`2 by A15,A29,A13,A11,A49,GOBOARD5:1;
then
A50: p`2 <= G*(i,j+1)`2 by A48,A22,A33,XXREAL_0:2;
i2 < i1 or i2 = i1 by A6,A28,XXREAL_0:1;
then
A51: G1*(i2,j1)`1 <= G1*(i1,j1)`1 by A19,A34,A15,A32,A28,GOBOARD5:3;
A52: 1 < i3 by A7,A16,A23,XXREAL_0:2;
then G1*(i3,j1)`1 = G1*(i3,1)`1 by A34,A32,A24,GOBOARD5:2
.= G1*(i3,j2)`1 by A31,A46,A38,A24,A52,GOBOARD5:2;
then
A53: p`1 <= G*(i+1,j)`1 by A43,A42,A44,XXREAL_0:2;
G1*(i2,j1)`1 = G1*(i2,1)`1 by A34,A15,A32,A28,A29,GOBOARD5:2
.= G1*(i2,j2)`1 by A15,A31,A28,A40,A29,A46,GOBOARD5:2;
then G*(i,j)`1 <= p`1 by A36,A41,A51,XXREAL_0:2;
hence thesis by A2,A3,A4,A5,A53,A47,A50,JORDAN9:17;
end;
theorem
m <= n & 3 <= i & i < len Gauge(E,m) & 1 < j & j+1 < width Gauge(E,m)
implies for i1,j1 being Nat st i1 = 2|^(n-'m)*(i-2)+2 & j1 = 2|^(n-'
m)*(j-2)+2 holds cell(Gauge(E,n),i1-'1,j1) c= cell(Gauge(E,m),i-'1,j)
proof
assume that
A1: m <= n and
A2: 3 <= i and
A3: i < len Gauge(E,m) and
A4: 1 < j & j+1 < width Gauge(E,m);
A5: i-2 = i-'2 by A2,XREAL_1:233,XXREAL_0:2;
A6: 2+1 <= i by A2;
then 1+1 < i by NAT_1:13;
then
A7: 1 < i-1 by XREAL_1:20;
A8: 2|^(n-'m) > 0 by NEWTON:83;
A9: i-3 = i-'3 by A2,XREAL_1:233;
then i -' 3 < i -' 2 by A5,XREAL_1:10;
then 2|^(n-'m)*(i-'3) < 2|^(n-'m)*(i-'2) by A8,XREAL_1:68;
then 2|^(n-'m)*(i-'3) + 1 <= 2|^(n-'m)*(i-'2) by NAT_1:13;
then 2|^(n-'m)*(i-'3) <= 2|^(n-'m)*(i-'2)-'1 by NAT_D:55;
then
A10: 2|^(n-'m)*(i-'3)+2 <= 2|^(n-'m)*(i-'2)-'1+2 by XREAL_1:6;
A11: i-'1 = i-1 by A2,XREAL_1:233,XXREAL_0:2;
then
A12: i -'1 -1 = i-(1+1);
i > 2+0 by A6,NAT_1:13;
then i-2 > 0 by XREAL_1:20;
then
A13: 2|^(n-'m)*(i-'2) > 0 by A8,A5,XREAL_1:129;
then 2|^(n-'m)*(i-'2) >= 0+1 by NAT_1:13;
then
A14: 2|^(n-'m)*(i-'1-2)+2 <= 2|^(n-'m)*(i-'2)+2-'1 by A9,A11,A10,NAT_D:38;
A15: i-'1+1 < len Gauge(E,m) by A2,A3,XREAL_1:235,XXREAL_0:2;
let i1,j1 be Nat such that
A16: i1 = 2|^(n-'m)*(i-2)+2 and
A17: j1 = 2|^(n-'m)*(j-2)+2;
i1 < i1+1 by XREAL_1:29;
then
A18: i1-1 < i1 by XREAL_1:19;
i1 > 0+2 by A16,A5,A13,XREAL_1:6;
then
A19: i1-'1 < i1 by A18,XREAL_1:233,XXREAL_0:2;
j-2 < j-1 by XREAL_1:10;
then 2|^(n-'m)*(j-2) < 2|^(n-'m)*(j-1) by A8,XREAL_1:68;
then j1 < 2|^(n-'m)*(j-1)+2 by A17,XREAL_1:6;
hence thesis by A1,A4,A16,A17,A7,A15,A5,A14,A12,A19,Th47;
end;
theorem
for C being compact non vertical non horizontal Subset of TOP-REAL 2
holds i <= len Gauge(C,n) implies cell(Gauge(C,n),i,0) c= UBD C
proof
let C be compact non vertical non horizontal Subset of TOP-REAL 2;
assume
A1: i <= len Gauge(C,n);
then cell(Gauge(C,n),i,0) misses C by JORDAN8:17;
then
A2: cell(Gauge(C,n),i,0) c= C` by SUBSET_1:23;
0 <= width Gauge(C,n);
then
cell(Gauge(C,n),i,0) is connected & cell(Gauge(C,n),i,0) is non empty by A1
,Th24,Th25;
then consider W being Subset of TOP-REAL 2 such that
A3: W is_a_component_of C` and
A4: cell(Gauge(C,n),i,0) c= W by A2,GOBOARD9:3;
W is not bounded by A1,A4,Th26,RLTOPSP1:42;
then W is_outside_component_of C by A3,JORDAN2C:def 3;
then W c= UBD C by JORDAN2C:23;
hence thesis by A4;
end;
theorem
for C being compact non vertical non horizontal Subset of TOP-REAL 2
holds i <= len Gauge(E,n) implies cell(Gauge(E,n),i,width Gauge(E,n)) c= UBD E
proof
let C be compact non vertical non horizontal Subset of TOP-REAL 2;
assume
A1: i <= len Gauge(E,n);
width Gauge(E,n) = len Gauge(E,n) by JORDAN8:def 1;
then cell(Gauge(E,n),i,width Gauge(E,n)) misses E by A1,JORDAN8:15;
then
A2: cell(Gauge(E,n),i,width Gauge(E,n)) c= E` by SUBSET_1:23;
cell(Gauge(E,n),i,width Gauge(E,n)) is connected & cell(Gauge(E,n),i,
width Gauge(E,n)) is non empty by A1,Th24,Th25;
then consider W being Subset of TOP-REAL 2 such that
A3: W is_a_component_of E` and
A4: cell(Gauge(E,n),i,width Gauge(E,n)) c= W by A2,GOBOARD9:3;
W is not bounded by A1,A4,Th27,RLTOPSP1:42;
then W is_outside_component_of E by A3,JORDAN2C:def 3;
then W c= UBD E by JORDAN2C:23;
hence thesis by A4;
end;
begin :: Cages
theorem Th51:
p in C implies north_halfline p meets L~Cage(C,n)
proof
set f = Cage(C,n);
assume
A1: p in C;
set X = {q where q is Point of TOP-REAL 2: q`1 = p`1 & q`2 >= p`2};
A2: X = north_halfline p by TOPREAL1:30;
max(N-bound (L~f),p`2)+1 > N-bound (L~f)+0 by XREAL_1:8,XXREAL_0:25;
then
f/.1 = N-min L~f & |[p`1,max(N-bound (L~f),p`2)+1]|`2 > N-bound (L~f) by
EUCLID:52,JORDAN9:32;
then |[p`1,max(N-bound (L~f),p`2)+1]| in LeftComp f by JORDAN2C:113;
then
A3: |[p`1,max(N-bound (L~f),p`2)+1]| in UBD L~f by GOBRD14:36;
LeftComp f is_outside_component_of L~f by GOBRD14:34;
then LeftComp f is_a_component_of (L~f)` by JORDAN2C:def 3;
then
A4: UBD L~f is_a_component_of (L~f)` by GOBRD14:36;
reconsider X as connected Subset of TOP-REAL 2 by A2;
A5: C c= BDD L~f & p in X by JORDAN10:12;
max(N-bound (L~f),p`2) >= p`2 by XXREAL_0:25;
then max(N-bound (L~f),p`2)+1 >= p`2+0 by XREAL_1:7;
then
A6: |[p`1,max(N-bound (L~f),p`2)+1]|`2 >= p`2 by EUCLID:52;
|[p`1,max(N-bound (L~f),p`2)+1]|`1 = p`1 by EUCLID:52;
then |[p`1,max(N-bound (L~f),p`2)+1]| in X by A6;
then
A7: X meets UBD L~f by A3,XBOOLE_0:3;
assume not thesis;
then X c= (L~f)` by A2,SUBSET_1:23;
then X c= UBD L~f by A7,A4,GOBOARD9:4;
then p in BDD L~f /\ UBD L~f by A1,A5,XBOOLE_0:def 4;
then BDD L~f meets UBD L~f;
hence contradiction by JORDAN2C:24;
end;
theorem Th52:
p in C implies east_halfline p meets L~Cage(C,n)
proof
set f = Cage(C,n);
assume
A1: p in C;
set X = {q where q is Point of TOP-REAL 2: q`1 >= p`1 & q`2 = p`2};
A2: X = east_halfline p by TOPREAL1:32;
max(E-bound (L~f),p`1)+1 > E-bound (L~f)+0 by XREAL_1:8,XXREAL_0:25;
then
f/.1 = N-min L~f & |[max(E-bound (L~f),p`1)+1,p`2]|`1 > E-bound (L~f) by
EUCLID:52,JORDAN9:32;
then |[max(E-bound (L~f),p`1)+1,p`2]| in LeftComp f by JORDAN2C:111;
then
A3: |[max(E-bound (L~f),p`1)+1,p`2]| in UBD L~f by GOBRD14:36;
LeftComp f is_outside_component_of L~f by GOBRD14:34;
then LeftComp f is_a_component_of (L~f)` by JORDAN2C:def 3;
then
A4: UBD L~f is_a_component_of (L~f)` by GOBRD14:36;
reconsider X as connected Subset of TOP-REAL 2 by A2;
A5: C c= BDD L~f & p in X by JORDAN10:12;
max(E-bound (L~f),p`1) >= p`1 by XXREAL_0:25;
then max(E-bound (L~f),p`1)+1 >= p`1+0 by XREAL_1:7;
then
A6: |[max(E-bound (L~f),p`1)+1,p`2]|`1 >= p`1 by EUCLID:52;
|[max(E-bound (L~f),p`1)+1,p`2]|`2 = p`2 by EUCLID:52;
then |[max(E-bound (L~f),p`1)+1,p`2]| in X by A6;
then
A7: X meets UBD L~f by A3,XBOOLE_0:3;
assume not thesis;
then X c= (L~f)` by A2,SUBSET_1:23;
then X c= UBD L~f by A7,A4,GOBOARD9:4;
then p in BDD L~f /\ UBD L~f by A1,A5,XBOOLE_0:def 4;
then BDD L~f meets UBD L~f;
hence contradiction by JORDAN2C:24;
end;
theorem Th53:
p in C implies south_halfline p meets L~Cage(C,n)
proof
set f = Cage(C,n);
assume
A1: p in C;
set X = {q where q is Point of TOP-REAL 2: q`1 = p`1 & q`2 <= p`2};
A2: X = south_halfline p by TOPREAL1:34;
min(S-bound (L~f),p`2)-1 < S-bound (L~f)-0 by XREAL_1:15,XXREAL_0:17;
then
f/.1 = N-min L~f & |[p`1,min(S-bound (L~f),p`2)-1]|`2 < S-bound (L~f) by
EUCLID:52,JORDAN9:32;
then |[p`1,min(S-bound (L~f),p`2)-1]| in LeftComp f by JORDAN2C:112;
then
A3: |[p`1,min(S-bound (L~f),p`2)-1]| in UBD L~f by GOBRD14:36;
LeftComp f is_outside_component_of L~f by GOBRD14:34;
then LeftComp f is_a_component_of (L~f)` by JORDAN2C:def 3;
then
A4: UBD L~f is_a_component_of (L~f)` by GOBRD14:36;
reconsider X as connected Subset of TOP-REAL 2 by A2;
A5: C c= BDD L~f & p in X by JORDAN10:12;
min(S-bound (L~f),p`2) <= p`2 by XXREAL_0:17;
then min(S-bound (L~f),p`2)-1 <= p`2-0 by XREAL_1:13;
then
A6: |[p`1,min(S-bound (L~f),p`2)-1]|`2 <= p`2 by EUCLID:52;
|[p`1,min(S-bound (L~f),p`2)-1]|`1 = p`1 by EUCLID:52;
then |[p`1,min(S-bound (L~f),p`2)-1]| in X by A6;
then
A7: X meets UBD L~f by A3,XBOOLE_0:3;
assume not thesis;
then X c= (L~f)` by A2,SUBSET_1:23;
then X c= UBD L~f by A7,A4,GOBOARD9:4;
then p in BDD L~f /\ UBD L~f by A1,A5,XBOOLE_0:def 4;
then BDD L~f meets UBD L~f;
hence contradiction by JORDAN2C:24;
end;
theorem Th54:
p in C implies west_halfline p meets L~Cage(C,n)
proof
set f = Cage(C,n);
assume
A1: p in C;
set X = {q where q is Point of TOP-REAL 2: q`1 <= p`1 & q`2 = p`2};
A2: X = west_halfline p by TOPREAL1:36;
min(W-bound (L~f),p`1)-1 < W-bound (L~f)-0 by XREAL_1:15,XXREAL_0:17;
then
f/.1 = N-min L~f & |[min(W-bound (L~f),p`1)-1,p`2]|`1 < W-bound (L~f) by
EUCLID:52,JORDAN9:32;
then |[min(W-bound (L~f),p`1)-1,p`2]| in LeftComp f by JORDAN2C:110;
then
A3: |[min(W-bound (L~f),p`1)-1,p`2]| in UBD L~f by GOBRD14:36;
LeftComp f is_outside_component_of L~f by GOBRD14:34;
then LeftComp f is_a_component_of (L~f)` by JORDAN2C:def 3;
then
A4: UBD L~f is_a_component_of (L~f)` by GOBRD14:36;
reconsider X as connected Subset of TOP-REAL 2 by A2;
A5: C c= BDD L~f & p in X by JORDAN10:12;
min(W-bound (L~f),p`1) <= p`1 by XXREAL_0:17;
then min(W-bound (L~f),p`1)-1 <= p`1-0 by XREAL_1:13;
then
A6: |[min(W-bound (L~f),p`1)-1,p`2]|`1 <= p`1 by EUCLID:52;
|[min(W-bound (L~f),p`1)-1,p`2]|`2 = p`2 by EUCLID:52;
then |[min(W-bound (L~f),p`1)-1,p`2]| in X by A6;
then
A7: X meets UBD L~f by A3,XBOOLE_0:3;
assume not thesis;
then X c= (L~f)` by A2,SUBSET_1:23;
then X c= UBD L~f by A7,A4,GOBOARD9:4;
then p in BDD L~f /\ UBD L~f by A1,A5,XBOOLE_0:def 4;
then BDD L~f meets UBD L~f;
hence contradiction by JORDAN2C:24;
end;
Lm15: ex k,t st 1 <= k & k <= len Cage(C,n) & 1 <= t & t <= width (Gauge(C,n))
& Cage(C,n)/.k = Gauge(C,n)*(1,t)
proof
consider x being object such that
A1: x in W-most C by XBOOLE_0:def 1;
reconsider x as Point of TOP-REAL 2 by A1;
A2: x in C by A1,XBOOLE_0:def 4;
set X = {q where q is Point of TOP-REAL 2: q`1 <= x`1 & q`2 = x`2};
A3: X = west_halfline x by TOPREAL1:36;
then reconsider X as connected Subset of TOP-REAL 2;
assume
A4: for k,t being Nat st 1 <= k & k <= len Cage(C,n) & 1 <= t
& t <= width (Gauge(C,n)) holds Cage(C,n)/.k <> Gauge(C,n)*(1,t);
A5: now
west_halfline x meets L~Cage(C,n) by A2,Th54;
then consider y being object such that
A6: y in X and
A7: y in L~Cage(C,n) by A3,XBOOLE_0:3;
reconsider y as Point of TOP-REAL 2 by A6;
consider q being Point of TOP-REAL 2 such that
A8: y = q and
A9: q`1 <= x`1 and
A10: q`2 = x`2 by A6;
consider i being Nat such that
A11: 1 <= i and
A12: i+1 <= len Cage(C,n) and
A13: y in LSeg(Cage(C,n),i) by A7,SPPOL_2:13;
A14: q`1 < x`1
proof
assume q`1 >= x`1;
then q`1 = x`1 by A9,XXREAL_0:1;
then q = x by A10,TOPREAL3:6;
then x in C /\ L~Cage(C,n) by A2,A7,A8,XBOOLE_0:def 4;
then C meets L~Cage(C,n);
hence contradiction by JORDAN10:5;
end;
A15: y in LSeg(Cage(C,n)/.i,Cage(C,n)/.(i+1)) by A11,A12,A13,TOPREAL1:def 3;
now
per cases;
suppose
(Cage(C,n)/.i)`1 <= (Cage(C,n)/.(i+1))`1;
then (Cage(C,n)/.i)`1 <= q`1 by A8,A15,TOPREAL1:3;
then
A16: (Cage(C,n)/.i)`1 < x`1 by A14,XXREAL_0:2;
A17: Cage(C,n) is_sequence_on Gauge(C,n) by JORDAN9:def 1;
A18: i < len Cage(C,n) by A12,NAT_1:13;
then i in Seg len Cage(C,n) by A11,FINSEQ_1:1;
then i in dom Cage(C,n) by FINSEQ_1:def 3;
then consider i1,i2 being Nat such that
A19: [i1,i2] in Indices Gauge(C,n) and
A20: Cage(C,n)/.i = Gauge(C,n)*(i1,i2) by A17,GOBOARD1:def 9;
A21: 1 <= i2 by A19,MATRIX_0:32;
A22: i1 <= len Gauge(C,n) by A19,MATRIX_0:32;
A23: 1 <= i1 by A19,MATRIX_0:32;
A24: i2 <= width Gauge(C,n) by A19,MATRIX_0:32;
then
A25: i2 <= len Gauge(C,n) by JORDAN8:def 1;
x`1 = (W-min C)`1 by A1,PSCOMP_1:31
.= W-bound C by EUCLID:52
.= Gauge(C,n)*(2,i2)`1 by A21,A25,JORDAN8:11;
then i1 < 1+1 by A16,A20,A21,A24,A22,SPRECT_3:13;
then i1 <= 1 by NAT_1:13;
then Cage(C,n)/.i = Gauge(C,n)*(1,i2) by A20,A23,XXREAL_0:1;
hence x in UBD L~Cage(C,n) by A4,A11,A18,A21,A24;
end;
suppose
(Cage(C,n)/.i)`1 >= (Cage(C,n)/.(i+1))`1;
then q`1 >= (Cage(C,n)/.(i+1))`1 by A8,A15,TOPREAL1:3;
then
A26: (Cage(C,n)/.(i+1))`1 < x`1 by A14,XXREAL_0:2;
A27: Cage(C,n) is_sequence_on Gauge(C,n) by JORDAN9:def 1;
A28: i+1 >= 1 by NAT_1:11;
then i+1 in Seg len Cage(C,n) by A12,FINSEQ_1:1;
then i+1 in dom Cage(C,n) by FINSEQ_1:def 3;
then consider i1,i2 being Nat such that
A29: [i1,i2] in Indices Gauge(C,n) and
A30: Cage(C,n)/.(i+1) = Gauge(C,n)*(i1,i2) by A27,GOBOARD1:def 9;
A31: 1 <= i2 by A29,MATRIX_0:32;
A32: i1 <= len Gauge(C,n) by A29,MATRIX_0:32;
A33: 1 <= i1 by A29,MATRIX_0:32;
A34: i2 <= width Gauge(C,n) by A29,MATRIX_0:32;
then
A35: i2 <= len Gauge(C,n) by JORDAN8:def 1;
x`1 = (W-min C)`1 by A1,PSCOMP_1:31
.= W-bound C by EUCLID:52
.= Gauge(C,n)*(2,i2)`1 by A31,A35,JORDAN8:11;
then i1 < 1+1 by A26,A30,A31,A34,A32,SPRECT_3:13;
then i1 <= 1 by NAT_1:13;
then Cage(C,n)/.(i+1) = Gauge(C,n)*(1,i2) by A30,A33,XXREAL_0:1;
hence x in UBD L~Cage(C,n) by A4,A12,A28,A31,A34;
end;
end;
hence x in UBD L~Cage(C,n);
end;
C c= BDD L~Cage(C,n) by JORDAN10:12;
then x in BDD L~Cage(C,n) /\ UBD L~Cage(C,n) by A2,A5,XBOOLE_0:def 4;
then BDD L~Cage(C,n) meets UBD L~Cage(C,n);
hence contradiction by JORDAN2C:24;
end;
Lm16: ex k,t st 1 <= k & k <= len Cage(C,n) & 1 <= t & t <= len (Gauge(C,n)) &
Cage(C,n)/.k = Gauge(C,n)*(t,1)
proof
consider x being object such that
A1: x in S-most C by XBOOLE_0:def 1;
reconsider x as Point of TOP-REAL 2 by A1;
A2: x in C by A1,XBOOLE_0:def 4;
set X = {q where q is Point of TOP-REAL 2: q`1 = x`1 & q`2 <= x`2};
A3: X = south_halfline x by TOPREAL1:34;
then reconsider X as connected Subset of TOP-REAL 2;
assume
A4: for k,t being Nat st 1 <= k & k <= len Cage(C,n) & 1 <= t
& t <= len (Gauge(C,n)) holds Cage(C,n)/.k <> Gauge(C,n)*(t,1);
A5: now
south_halfline x meets L~Cage(C,n) by A2,Th53;
then consider y being object such that
A6: y in X and
A7: y in L~Cage(C,n) by A3,XBOOLE_0:3;
reconsider y as Point of TOP-REAL 2 by A6;
consider q being Point of TOP-REAL 2 such that
A8: y = q and
A9: q`1 = x`1 and
A10: q`2 <= x`2 by A6;
consider i being Nat such that
A11: 1 <= i and
A12: i+1 <= len Cage(C,n) and
A13: y in LSeg(Cage(C,n),i) by A7,SPPOL_2:13;
A14: q`2 < x`2
proof
assume q`2 >= x`2;
then q`2 = x`2 by A10,XXREAL_0:1;
then q = x by A9,TOPREAL3:6;
then x in C /\ L~Cage(C,n) by A2,A7,A8,XBOOLE_0:def 4;
then C meets L~Cage(C,n);
hence contradiction by JORDAN10:5;
end;
A15: y in LSeg(Cage(C,n)/.i,Cage(C,n)/.(i+1)) by A11,A12,A13,TOPREAL1:def 3;
now
per cases;
suppose
(Cage(C,n)/.i)`2 <= (Cage(C,n)/.(i+1))`2;
then (Cage(C,n)/.i)`2 <= q`2 by A8,A15,TOPREAL1:4;
then
A16: (Cage(C,n)/.i)`2 < x`2 by A14,XXREAL_0:2;
A17: Cage(C,n) is_sequence_on Gauge(C,n) by JORDAN9:def 1;
A18: i < len Cage(C,n) by A12,NAT_1:13;
then i in Seg len Cage(C,n) by A11,FINSEQ_1:1;
then i in dom Cage(C,n) by FINSEQ_1:def 3;
then consider i1,i2 being Nat such that
A19: [i1,i2] in Indices Gauge(C,n) and
A20: Cage(C,n)/.i = Gauge(C,n)*(i1,i2) by A17,GOBOARD1:def 9;
A21: 1 <= i2 by A19,MATRIX_0:32;
A22: i2 <= width Gauge(C,n) by A19,MATRIX_0:32;
A23: 1 <= i1 & i1 <= len Gauge(C,n) by A19,MATRIX_0:32;
x`2 = (S-min C)`2 by A1,PSCOMP_1:55
.= S-bound C by EUCLID:52
.= Gauge(C,n)*(i1,2)`2 by A23,JORDAN8:13;
then i2 < 1+1 by A16,A20,A22,A23,SPRECT_3:12;
then i2 <= 1 by NAT_1:13;
then Cage(C,n)/.i = Gauge(C,n)*(i1,1) by A20,A21,XXREAL_0:1;
hence x in UBD L~Cage(C,n) by A4,A11,A18,A23;
end;
suppose
(Cage(C,n)/.i)`2 >= (Cage(C,n)/.(i+1))`2;
then q`2 >= (Cage(C,n)/.(i+1))`2 by A8,A15,TOPREAL1:4;
then
A24: (Cage(C,n)/.(i+1))`2 < x`2 by A14,XXREAL_0:2;
A25: Cage(C,n) is_sequence_on Gauge(C,n) by JORDAN9:def 1;
A26: i+1 >= 1 by NAT_1:11;
then i+1 in Seg len Cage(C,n) by A12,FINSEQ_1:1;
then i+1 in dom Cage(C,n) by FINSEQ_1:def 3;
then consider i1,i2 being Nat such that
A27: [i1,i2] in Indices Gauge(C,n) and
A28: Cage(C,n)/.(i+1) = Gauge(C,n)*(i1,i2) by A25,GOBOARD1:def 9;
A29: 1 <= i2 by A27,MATRIX_0:32;
A30: i2 <= width Gauge(C,n) by A27,MATRIX_0:32;
A31: 1 <= i1 & i1 <= len Gauge(C,n) by A27,MATRIX_0:32;
x`2 = (S-min C)`2 by A1,PSCOMP_1:55
.= S-bound C by EUCLID:52
.= Gauge(C,n)*(i1,2)`2 by A31,JORDAN8:13;
then i2 < 1+1 by A24,A28,A30,A31,SPRECT_3:12;
then i2 <= 1 by NAT_1:13;
then Cage(C,n)/.(i+1) = Gauge(C,n)*(i1,1) by A28,A29,XXREAL_0:1;
hence x in UBD L~Cage(C,n) by A4,A12,A26,A31;
end;
end;
hence x in UBD L~Cage(C,n);
end;
C c= BDD L~Cage(C,n) by JORDAN10:12;
then x in BDD L~Cage(C,n) /\ UBD L~Cage(C,n) by A2,A5,XBOOLE_0:def 4;
then BDD L~Cage(C,n) meets UBD L~Cage(C,n);
hence contradiction by JORDAN2C:24;
end;
Lm17: ex k,t st 1 <= k & k <= len Cage(C,n) & 1 <= t & t <= width (Gauge(C,n))
& Cage(C,n)/.k = Gauge(C,n)*(len(Gauge(C,n)),t)
proof
consider x being object such that
A1: x in E-most C by XBOOLE_0:def 1;
reconsider x as Point of TOP-REAL 2 by A1;
A2: x in C by A1,XBOOLE_0:def 4;
set X = {q where q is Point of TOP-REAL 2: q`1 >= x`1 & q`2 = x`2};
A3: X = east_halfline x by TOPREAL1:32;
then reconsider X as connected Subset of TOP-REAL 2;
assume
A4: for k,t being Nat st 1 <= k & k <= len Cage(C,n) & 1 <= t
& t <= width (Gauge(C,n)) holds Cage(C,n)/.k <> Gauge(C,n)*(len(Gauge(C,n)),t);
A5: now
east_halfline x meets L~Cage(C,n) by A2,Th52;
then consider y being object such that
A6: y in X and
A7: y in L~Cage(C,n) by A3,XBOOLE_0:3;
reconsider y as Point of TOP-REAL 2 by A6;
consider q being Point of TOP-REAL 2 such that
A8: y = q and
A9: q`1 >= x`1 and
A10: q`2 = x`2 by A6;
consider i being Nat such that
A11: 1 <= i and
A12: i+1 <= len Cage(C,n) and
A13: y in LSeg(Cage(C,n),i) by A7,SPPOL_2:13;
A14: y in LSeg(Cage(C,n)/.i,Cage(C,n)/.(i+1)) by A11,A12,A13,TOPREAL1:def 3;
A15: q`1 > x`1
proof
assume q`1 <= x`1;
then q`1 = x`1 by A9,XXREAL_0:1;
then q = x by A10,TOPREAL3:6;
then x in C /\ L~Cage(C,n) by A2,A7,A8,XBOOLE_0:def 4;
then C meets L~Cage(C,n);
hence contradiction by JORDAN10:5;
end;
A16: Cage(C,n) is_sequence_on Gauge(C,n) by JORDAN9:def 1;
A17: Cage(C,n) is_sequence_on Gauge(C,n) by JORDAN9:def 1;
A18: 4 <= len(Gauge(C,n)) by JORDAN8:10;
A19: 1 <= i+1 by A11,NAT_1:13;
then i+1 in Seg len Cage(C,n) by A12,FINSEQ_1:1;
then i+1 in dom Cage(C,n) by FINSEQ_1:def 3;
then consider l1,l2 being Nat such that
A20: [l1,l2] in Indices Gauge(C,n) and
A21: Cage(C,n)/.(i+1) = Gauge(C,n)*(l1,l2) by A16,GOBOARD1:def 9;
A22: 1 <= l2 by A20,MATRIX_0:32;
A23: l2 <= width Gauge(C,n) by A20,MATRIX_0:32;
then
A24: l2 <= len Gauge(C,n) by JORDAN8:def 1;
A25: x`1 = (E-min C)`1 by A1,PSCOMP_1:47
.= E-bound C by EUCLID:52
.= Gauge(C,n)*(len(Gauge(C,n))-'1,l2)`1 by A22,A24,JORDAN8:12;
A26: l1 <= len Gauge(C,n) by A20,MATRIX_0:32;
A27: 1 <= l1 by A20,MATRIX_0:32;
A28: len(Gauge(C,n))-'1 <= len(Gauge(C,n)) by NAT_D:35;
A29: i < len Cage(C,n) by A12,NAT_1:13;
then i in Seg len Cage(C,n) by A11,FINSEQ_1:1;
then i in dom Cage(C,n) by FINSEQ_1:def 3;
then consider i1,i2 being Nat such that
A30: [i1,i2] in Indices Gauge(C,n) and
A31: Cage(C,n)/.i = Gauge(C,n)*(i1,i2) by A17,GOBOARD1:def 9;
A32: 1 <= i2 by A30,MATRIX_0:32;
A33: i1 <= len Gauge(C,n) by A30,MATRIX_0:32;
A34: 1 <= i1 by A30,MATRIX_0:32;
A35: i2 <= width Gauge(C,n) by A30,MATRIX_0:32;
then
A36: i2 <= len Gauge(C,n) by JORDAN8:def 1;
A37: x`1 = (E-min C)`1 by A1,PSCOMP_1:47
.= E-bound C by EUCLID:52
.= Gauge(C,n)*(len(Gauge(C,n))-'1,i2)`1 by A32,A36,JORDAN8:12;
now
per cases;
suppose
(Cage(C,n)/.i)`1 >= (Cage(C,n)/.(i+1))`1;
then (Cage(C,n)/.i)`1 >= q`1 by A8,A14,TOPREAL1:3;
then (Cage(C,n)/.i)`1 > x`1 by A15,XXREAL_0:2;
then i1 > len(Gauge(C,n))-'1 by A31,A32,A35,A34,A37,A28,SPRECT_3:13;
then i1 >= len(Gauge(C,n))-'1 + 1 by NAT_1:13;
then i1 >= len(Gauge(C,n)) by A18,XREAL_1:235,XXREAL_0:2;
then Cage(C,n)/.i = Gauge(C,n)*(len(Gauge(C,n)),i2) by A31,A33,
XXREAL_0:1;
hence contradiction by A4,A11,A29,A32,A35;
end;
suppose
(Cage(C,n)/.i)`1 <= (Cage(C,n)/.(i+1))`1;
then q`1 <= (Cage(C,n)/.(i+1))`1 by A8,A14,TOPREAL1:3;
then (Cage(C,n)/.(i+1))`1 > x`1 by A15,XXREAL_0:2;
then l1 > len(Gauge(C,n))-'1 by A21,A22,A23,A27,A25,A28,SPRECT_3:13;
then l1 >= len(Gauge(C,n))-'1 + 1 by NAT_1:13;
then l1 >= len(Gauge(C,n)) by A18,XREAL_1:235,XXREAL_0:2;
then
Cage(C,n)/.(i+1) = Gauge(C,n)*(len(Gauge(C,n)),l2) by A21,A26,XXREAL_0:1;
hence contradiction by A4,A12,A19,A22,A23;
end;
end;
hence x in UBD L~Cage(C,n);
end;
C c= BDD L~Cage(C,n) by JORDAN10:12;
then x in BDD L~Cage(C,n) /\ UBD L~Cage(C,n) by A2,A5,XBOOLE_0:def 4;
then BDD L~Cage(C,n) meets UBD L~Cage(C,n);
hence contradiction by JORDAN2C:24;
end;
theorem Th55:
ex k,t st 1 <= k & k < len Cage(C,n) & 1 <= t & t <= width (
Gauge(C,n)) & Cage(C,n)/.k = Gauge(C,n)*(1,t)
proof
consider k,t such that
A1: 1 <= k and
A2: k <= len Cage(C,n) and
A3: 1 <= t & t <= width (Gauge(C,n)) and
A4: Cage(C,n)/.k = Gauge(C,n)*(1,t) by Lm15;
per cases by A2,XXREAL_0:1;
suppose
k<len Cage(C,n);
hence thesis by A1,A3,A4;
end;
suppose
A5: k=len Cage(C,n);
take 1,t;
thus 1 <= 1 & 1 < len Cage(C,n) by GOBOARD7:34,XXREAL_0:2;
thus 1 <= t & t <= width (Gauge(C,n)) by A3;
thus thesis by A4,A5,FINSEQ_6:def 1;
end;
end;
theorem Th56:
ex k,t st 1 <= k & k < len Cage(C,n) & 1 <= t & t <= len (Gauge(
C,n)) & Cage(C,n)/.k = Gauge(C,n)*(t,1)
proof
consider k,t such that
A1: 1 <= k and
A2: k <= len Cage(C,n) and
A3: 1 <= t & t <= len (Gauge(C,n)) and
A4: Cage(C,n)/.k = Gauge(C,n)*(t,1) by Lm16;
per cases by A2,XXREAL_0:1;
suppose
k<len Cage(C,n);
hence thesis by A1,A3,A4;
end;
suppose
A5: k=len Cage(C,n);
take 1,t;
thus 1 <= 1 & 1 < len Cage(C,n) by GOBOARD7:34,XXREAL_0:2;
thus 1 <= t & t <= len (Gauge(C,n)) by A3;
thus thesis by A4,A5,FINSEQ_6:def 1;
end;
end;
theorem Th57:
ex k,t st 1 <= k & k < len Cage(C,n) & 1 <= t & t <= width (
Gauge(C,n)) & Cage(C,n)/.k = Gauge(C,n)*(len(Gauge(C,n)),t)
proof
consider k,t such that
A1: 1 <= k and
A2: k <= len Cage(C,n) and
A3: 1 <= t & t <= width (Gauge(C,n)) and
A4: Cage(C,n)/.k = Gauge(C,n)*(len(Gauge(C,n)),t) by Lm17;
per cases by A2,XXREAL_0:1;
suppose
k<len Cage(C,n);
hence thesis by A1,A3,A4;
end;
suppose
A5: k=len Cage(C,n);
take 1,t;
thus 1 <= 1 & 1 < len Cage(C,n) by GOBOARD7:34,XXREAL_0:2;
thus 1 <= t & t <= width (Gauge(C,n)) by A3;
thus thesis by A4,A5,FINSEQ_6:def 1;
end;
end;
theorem Th58:
1 <= k & k <= len Cage(C,n) & 1 <= t & t <= len (Gauge(C,n)) &
Cage(C,n)/.k = Gauge(C,n)*(t,width Gauge(C,n)) implies Cage(C,n)/.k in N-most
L~Cage(C,n)
proof
assume that
A1: 1 <= k & k <= len Cage(C,n) and
A2: 1 <= t & t <= len (Gauge(C,n)) and
A3: Cage(C,n)/.k = Gauge(C,n)*(t,width Gauge(C,n));
Cage(C,n) is_sequence_on Gauge(C,n) by JORDAN9:def 1;
then
A4: (Gauge(C,n)*(t,width Gauge(C,n)))`2 >= N-bound L~Cage(C,n) by A2,Th20;
len Cage(C,n) >= 2 by GOBOARD7:34,XXREAL_0:2;
then
A5: Cage(C,n)/.k in L~Cage(C,n) by A1,TOPREAL3:39;
then N-bound L~Cage(C,n) >= (Cage(C,n)/.k)`2 by PSCOMP_1:24;
hence thesis by A3,A5,A4,SPRECT_2:10,XXREAL_0:1;
end;
theorem Th59:
1 <= k & k <= len Cage(C,n) & 1 <= t & t <= width (Gauge(C,n)) &
Cage(C,n)/.k = Gauge(C,n)*(1,t) implies Cage(C,n)/.k in W-most L~Cage(C,n)
proof
assume that
A1: 1 <= k & k <= len Cage(C,n) and
A2: 1 <= t & t <= width (Gauge(C,n)) and
A3: Cage(C,n)/.k = Gauge(C,n)*(1,t);
Cage(C,n) is_sequence_on Gauge(C,n) by JORDAN9:def 1;
then
A4: (Gauge(C,n)*(1,t))`1 <= W-bound L~Cage(C,n) by A2,Th21;
len Cage(C,n) >= 2 by GOBOARD7:34,XXREAL_0:2;
then
A5: Cage(C,n)/.k in L~Cage(C,n) by A1,TOPREAL3:39;
then W-bound L~Cage(C,n) <= (Cage(C,n)/.k)`1 by PSCOMP_1:24;
hence thesis by A3,A5,A4,SPRECT_2:12,XXREAL_0:1;
end;
theorem Th60:
1 <= k & k <= len Cage(C,n) & 1 <= t & t <= len (Gauge(C,n)) &
Cage(C,n)/.k = Gauge(C,n)*(t,1) implies Cage(C,n)/.k in S-most L~Cage(C,n)
proof
assume that
A1: 1 <= k & k <= len Cage(C,n) and
A2: 1 <= t & t <= len (Gauge(C,n)) and
A3: Cage(C,n)/.k = Gauge(C,n)*(t,1);
Cage(C,n) is_sequence_on Gauge(C,n) by JORDAN9:def 1;
then
A4: (Gauge(C,n)*(t,1))`2 <= S-bound L~Cage(C,n) by A2,Th22;
len Cage(C,n) >= 2 by GOBOARD7:34,XXREAL_0:2;
then
A5: Cage(C,n)/.k in L~Cage(C,n) by A1,TOPREAL3:39;
then S-bound L~Cage(C,n) <= (Cage(C,n)/.k)`2 by PSCOMP_1:24;
hence thesis by A3,A5,A4,SPRECT_2:11,XXREAL_0:1;
end;
theorem Th61:
1 <= k & k <= len Cage(C,n) & 1 <= t & t <= width (Gauge(C,n)) &
Cage(C,n)/.k = Gauge(C,n)*(len Gauge(C,n),t) implies Cage(C,n)/.k in E-most L~
Cage(C,n)
proof
assume that
A1: 1 <= k & k <= len Cage(C,n) and
A2: 1 <= t & t <= width (Gauge(C,n)) and
A3: Cage(C,n)/.k = Gauge(C,n)*(len Gauge(C,n),t);
Cage(C,n) is_sequence_on Gauge(C,n) by JORDAN9:def 1;
then
A4: (Gauge(C,n)*(len Gauge(C,n),t))`1 >= E-bound L~Cage(C,n) by A2,Th23;
len Cage(C,n) >= 2 by GOBOARD7:34,XXREAL_0:2;
then
A5: Cage(C,n)/.k in L~Cage(C,n) by A1,TOPREAL3:39;
then E-bound L~Cage(C,n) >= (Cage(C,n)/.k)`1 by PSCOMP_1:24;
hence thesis by A3,A5,A4,SPRECT_2:13,XXREAL_0:1;
end;
theorem Th62:
W-bound L~Cage(C,n) = W-bound C - (E-bound C - W-bound C)/(2|^n)
proof
set a = N-bound C, s = S-bound C, w = W-bound C, e = E-bound C, f = Cage(C,n
), G = Gauge(C,n);
consider p, q being Nat such that
A1: 1 <= p & p < len f and
A2: 1 <= q & q <= width G and
A3: f/.p = G*(1,q) by Th55;
f/.p in W-most L~f by A1,A2,A3,Th59;
then
A4: (f/.p)`1 = (W-min L~f)`1 by PSCOMP_1:31;
4 <= len G by JORDAN8:10;
then 1 <= len G by XXREAL_0:2;
then
A5: [1,q] in Indices G by A2,MATRIX_0:30;
thus W-bound L~f = (W-min L~f)`1 by EUCLID:52
.= |[w+((e-w)/(2|^n))*(1-2), s+((a-s)/(2|^n))*(q-2)]|`1 by A3,A4,A5,
JORDAN8:def 1
.= w-(e-w)/(2|^n) by EUCLID:52;
end;
theorem Th63:
S-bound L~Cage(C,n) = S-bound C - (N-bound C - S-bound C)/(2|^n)
proof
set a = N-bound C, s = S-bound C, w = W-bound C, e = E-bound C, f = Cage(C,n
), G = Gauge(C,n);
consider p, q being Nat such that
A1: 1 <= p & p < len f and
A2: 1 <= q & q <= len G and
A3: f/.p = G*(q,1) by Th56;
f/.p in S-most L~f by A1,A2,A3,Th60;
then
A4: (f/.p)`2 = (S-min L~f)`2 by PSCOMP_1:55;
4 <= len G by JORDAN8:10;
then len G = width G & 1 <= len G by JORDAN8:def 1,XXREAL_0:2;
then
A5: [q,1] in Indices G by A2,MATRIX_0:30;
thus S-bound L~f = (S-min L~f)`2 by EUCLID:52
.= |[w+((e-w)/(2|^n))*(q-2), s+((a-s)/(2|^n))*(1-2)]|`2 by A3,A4,A5,
JORDAN8:def 1
.= s-(a-s)/(2|^n) by EUCLID:52;
end;
theorem Th64:
E-bound L~Cage(C,n) = E-bound C + (E-bound C - W-bound C)/(2|^n)
proof
set a = N-bound C, s = S-bound C, w = W-bound C, e = E-bound C, f = Cage(C,n
), G = Gauge(C,n);
consider p, q being Nat such that
A1: 1 <= p & p < len f and
A2: 1 <= q & q <= width G and
A3: f/.p = G*(len G,q) by Th57;
f/.p in E-most L~f by A1,A2,A3,Th61;
then
A4: (f/.p)`1 = (E-min L~f)`1 by PSCOMP_1:47;
4 <= len G by JORDAN8:10;
then 1 <= len G by XXREAL_0:2;
then
A5: [len G,q] in Indices G by A2,MATRIX_0:30;
thus E-bound L~f = (E-min L~f)`1 by EUCLID:52
.= |[w+((e-w)/(2|^n))*(len G-2), s+((a-s)/(2|^n))*(q-2)]|`1 by A3,A4,A5,
JORDAN8:def 1
.= w+((e-w)/(2|^n))*(len G-2) by EUCLID:52
.= e+(e-w)/(2|^n) by Lm10;
end;
theorem
N-bound L~Cage(C,n) + S-bound L~Cage(C,n) = N-bound L~Cage(C,m) +
S-bound L~Cage(C,m)
proof
thus N-bound L~Cage(C,n) + S-bound L~Cage(C,n) = N-bound C + (N-bound C -
S-bound C)/(2|^n) + S-bound L~Cage(C,n) by JORDAN10:6
.= N-bound C + (N-bound C - S-bound C)/(2|^n) + (S-bound C - (N-bound C
- S-bound C)/(2|^n)) by Th63
.= N-bound C + (N-bound C - S-bound C)/(2|^m) + (S-bound C - (N-bound C
- S-bound C)/(2|^m))
.= N-bound C + (N-bound C - S-bound C)/(2|^m) + S-bound L~Cage(C,m) by Th63
.= N-bound L~Cage(C,m) + S-bound L~Cage(C,m) by JORDAN10:6;
end;
theorem
E-bound L~Cage(C,n) + W-bound L~Cage(C,n) = E-bound L~Cage(C,m) +
W-bound L~Cage(C,m)
proof
thus E-bound L~Cage(C,n) + W-bound L~Cage(C,n) = E-bound C + (E-bound C -
W-bound C)/(2|^n) + W-bound L~Cage(C,n) by Th64
.= E-bound C + (E-bound C - W-bound C)/(2|^n) + (W-bound C - (E-bound C
- W-bound C)/(2|^n)) by Th62
.= E-bound C + (E-bound C - W-bound C)/(2|^m) + (W-bound C - (E-bound C
- W-bound C)/(2|^m))
.= E-bound C + (E-bound C - W-bound C)/(2|^m) + W-bound L~Cage(C,m) by Th62
.= E-bound L~Cage(C,m) + W-bound L~Cage(C,m) by Th64;
end;
theorem
i < j implies E-bound L~Cage(C,j) < E-bound L~Cage(C,i)
proof
assume
A1: i < j;
defpred P[Nat] means i < $1 implies E-bound L~Cage(C,$1) <
E-bound L~Cage(C,i);
A2: for n being Nat st P[n] holds P[n+1]
proof
let n be Nat;
assume
A3: P[n];
set j = n + 1, a = E-bound C, s = W-bound C;
A4: a+(a-s)/(2|^j) - (a+(a-s)/(2|^n)) = 0 + (a-s)/(2|^j) - (a-s)/(2|^n)
.= (a-s)/(2|^n*2) - (a-s)/(2|^n)/(2/2) by NEWTON:6
.= (a-s)/(2|^n*2) - (a-s)*2/(2|^n*2) by XCMPLX_1:84
.= (a-s - (2*a-2*s))/(2|^n*2) by XCMPLX_1:120
.= (s-a)/(2|^n*2);
2|^n > 0 by NEWTON:83;
then
A5: 2|^n*2 > 0 * 2 by XREAL_1:68;
A6: E-bound L~Cage(C,n) = a+(a-s)/(2|^n) & E-bound L~Cage(C,j) = a+(a-s)/(
2|^j) by Th64;
s - a < 0 by SPRECT_1:31,XREAL_1:49;
then 0 > a+(a-s)/(2|^j) - (a+(a-s)/(2|^n)) by A5,A4,XREAL_1:141;
then
A7: E-bound L~Cage(C,j) < E-bound L~Cage(C,n) by A6,XREAL_1:48;
assume i < n+1;
then i <= n by NAT_1:13;
hence thesis by A3,A7,XXREAL_0:1,2;
end;
A8: P[0];
for n being Nat holds P[n] from NAT_1:sch 2(A8,A2);
hence thesis by A1;
end;
theorem
i < j implies W-bound L~Cage(C,i) < W-bound L~Cage(C,j)
proof
assume
A1: i < j;
defpred P[Nat] means
i < $1 implies W-bound L~Cage(C,i) < W-bound
L~Cage(C,$1);
A2: for n being Nat st P[n] holds P[n+1]
proof
let n be Nat;
assume
A3: P[n];
set j = n + 1, a = E-bound C, s = W-bound C;
A4: s-(a-s)/(2|^j) - (s-(a-s)/(2|^n)) = s +- (a-s)/(2|^j) - s + (a-s)/(2 |^n)
.= - (a-s)/(2|^n*2) + (a-s)/(2|^n) by NEWTON:6
.= (-(a-s))/(2|^n*2) + (a-s)/(2|^n) by XCMPLX_1:187
.= (-(a-s))/(2|^n*2) + (a-s)*2/(2|^n*2) by XCMPLX_1:91
.= (-(a-s) + (a-s)*2) / (2|^n*2) by XCMPLX_1:62
.= (a-s)/(2|^n*2);
2|^n > 0 by NEWTON:83;
then
A5: 2|^n*2 > 0 * 2 by XREAL_1:68;
A6: W-bound L~Cage(C,n) = s-(a-s)/(2|^n) & W-bound L~Cage(C,j) = s-(a-s)/(
2|^j) by Th62;
a - s > 0 by SPRECT_1:31,XREAL_1:50;
then 0 < s-(a-s)/(2|^j) - (s-(a-s)/(2|^n)) by A5,A4,XREAL_1:139;
then
A7: W-bound L~Cage(C,n) < W-bound L~Cage(C,j) by A6,XREAL_1:47;
assume i < n+1;
then i <= n by NAT_1:13;
hence thesis by A3,A7,XXREAL_0:1,2;
end;
A8: P[0];
for n being Nat holds P[n] from NAT_1:sch 2(A8,A2);
hence thesis by A1;
end;
theorem
i < j implies S-bound L~Cage(C,i) < S-bound L~Cage(C,j)
proof
assume
A1: i < j;
defpred P[Nat] means
i < $1 implies S-bound L~Cage(C,i) < S-bound
L~Cage(C,$1);
A2: for n being Nat st P[n] holds P[n+1]
proof
let n be Nat;
assume
A3: P[n];
set j = n + 1, a = N-bound C, s = S-bound C;
A4: s-(a-s)/(2|^j) - (s-(a-s)/(2|^n)) = s +- (a-s)/(2|^j) - s + (a-s)/(2 |^n)
.= - (a-s)/(2|^n*2) + (a-s)/(2|^n) by NEWTON:6
.= (-(a-s))/(2|^n*2) + (a-s)/(2|^n) by XCMPLX_1:187
.= (-(a-s))/(2|^n*2) + (a-s)*2/(2|^n*2) by XCMPLX_1:91
.= (-(a-s) + (a-s)*2) / (2|^n*2) by XCMPLX_1:62
.= (a-s)/(2|^n*2);
2|^n > 0 by NEWTON:83;
then
A5: 2|^n*2 > 0 * 2 by XREAL_1:68;
A6: S-bound L~Cage(C,n) = s-(a-s)/(2|^n) & S-bound L~Cage(C,j) = s-(a-s)/(
2|^j) by Th63;
a - s > 0 by SPRECT_1:32,XREAL_1:50;
then 0 < s-(a-s)/(2|^j) - (s-(a-s)/(2|^n)) by A5,A4,XREAL_1:139;
then
A7: S-bound L~Cage(C,n) < S-bound L~Cage(C,j) by A6,XREAL_1:47;
assume i < n+1;
then i <= n by NAT_1:13;
hence thesis by A3,A7,XXREAL_0:1,2;
end;
A8: P[0];
for n being Nat holds P[n] from NAT_1:sch 2(A8,A2);
hence thesis by A1;
end;
theorem
1 <= i & i <= len Gauge(C,n) implies N-bound L~Cage(C,n) = Gauge(C,n)*
(i,len Gauge(C,n))`2
proof
set a = N-bound C, s = S-bound C, w = W-bound C, e = E-bound C, f = Cage(C,n
), G = Gauge(C,n);
A1: len G = width G by JORDAN8:def 1;
assume
A2: 1 <= i & i <= len G;
then 1 <= len G by XXREAL_0:2;
then
A3: [i,len G] in Indices G by A2,A1,MATRIX_0:30;
thus N-bound L~f = a + (a - s)/(2|^n) by JORDAN10:6
.= s+((a-s)/(2|^n))*(len G-2) by Lm10
.= |[w+((e-w)/(2|^n))*(i-2),s+((a-s)/(2|^n))*(len G-2)]|`2 by EUCLID:52
.= G*(i,len G)`2 by A3,JORDAN8:def 1;
end;
theorem
1 <= i & i <= len Gauge(C,n) implies E-bound L~Cage(C,n) = Gauge(C,n)*
(len Gauge(C,n),i)`1
proof
set a = N-bound C, s = S-bound C, w = W-bound C, e = E-bound C, f = Cage(C,n
), G = Gauge(C,n);
A1: len G = width G by JORDAN8:def 1;
assume
A2: 1 <= i & i <= len G;
then 1 <= len G by XXREAL_0:2;
then
A3: [len G,i] in Indices G by A2,A1,MATRIX_0:30;
thus E-bound L~f = e + (e - w)/(2|^n) by Th64
.= w+((e-w)/(2|^n))*(len G-2) by Lm10
.= |[w+((e-w)/(2|^n))*(len G-2),s+((a-s)/(2|^n))*(i-2)]|`1 by EUCLID:52
.= G*(len G,i)`1 by A3,JORDAN8:def 1;
end;
theorem
1 <= i & i <= len Gauge(C,n) implies S-bound L~Cage(C,n) = Gauge(C,n)*
(i,1)`2
proof
set a = N-bound C, s = S-bound C, w = W-bound C, e = E-bound C, f = Cage(C,n
), G = Gauge(C,n);
A1: len G = width G by JORDAN8:def 1;
assume
A2: 1 <= i & i <= len G;
then 1 <= len G by XXREAL_0:2;
then
A3: [i,1] in Indices G by A2,A1,MATRIX_0:30;
thus S-bound L~f = s - (a - s)/(2|^n) by Th63
.= |[w+((e-w)/(2|^n))*(i-2),s+((a-s)/(2|^n))*(1-2)]|`2 by EUCLID:52
.= G*(i,1)`2 by A3,JORDAN8:def 1;
end;
theorem
1 <= i & i <= len Gauge(C,n) implies W-bound L~Cage(C,n) = Gauge(C,n)*
(1,i)`1
proof
set a = N-bound C, s = S-bound C, w = W-bound C, e = E-bound C, f = Cage(C,n
), G = Gauge(C,n);
A1: len G = width G by JORDAN8:def 1;
assume
A2: 1 <= i & i <= len G;
then 1 <= len G by XXREAL_0:2;
then
A3: [1,i] in Indices G by A2,A1,MATRIX_0:30;
thus W-bound L~f = w - (e - w)/(2|^n) by Th62
.= |[w+((e-w)/(2|^n))*(1-2),s+((a-s)/(2|^n))*(i-2)]|`1 by EUCLID:52
.= G*(1,i)`1 by A3,JORDAN8:def 1;
end;
theorem Th74:
x in C & p in north_halfline x /\ L~Cage(C,n) implies p`2 > x`2
proof
set f = Cage(C,n);
assume
A1: x in C;
assume
A2: p in north_halfline x /\ L~f;
then
A3: p in north_halfline x by XBOOLE_0:def 4;
then
A4: p`1 = x`1 by TOPREAL1:def 10;
assume
A5: p`2 <= x`2;
p`2 >= x`2 by A3,TOPREAL1:def 10;
then p`2 = x`2 by A5,XXREAL_0:1;
then
A6: p = x by A4,TOPREAL3:6;
p in L~f by A2,XBOOLE_0:def 4;
then x in C /\ L~f by A1,A6,XBOOLE_0:def 4;
then C meets L~f;
hence contradiction by JORDAN10:5;
end;
theorem Th75:
x in C & p in east_halfline x /\ L~Cage(C,n) implies p`1 > x`1
proof
set f = Cage(C,n);
assume
A1: x in C;
assume
A2: p in east_halfline x /\ L~f;
then
A3: p in east_halfline x by XBOOLE_0:def 4;
then
A4: p`2 = x`2 by TOPREAL1:def 11;
assume
A5: p`1 <= x`1;
p`1 >= x`1 by A3,TOPREAL1:def 11;
then p`1 = x`1 by A5,XXREAL_0:1;
then
A6: p = x by A4,TOPREAL3:6;
p in L~f by A2,XBOOLE_0:def 4;
then x in C /\ L~f by A1,A6,XBOOLE_0:def 4;
then C meets L~f;
hence contradiction by JORDAN10:5;
end;
theorem Th76:
x in C & p in south_halfline x /\ L~Cage(C,n) implies p`2 < x`2
proof
set f = Cage(C,n);
assume
A1: x in C;
assume
A2: p in south_halfline x /\ L~f;
then
A3: p in south_halfline x by XBOOLE_0:def 4;
then
A4: p`1 = x`1 by TOPREAL1:def 12;
assume
A5: p`2 >= x`2;
p`2 <= x`2 by A3,TOPREAL1:def 12;
then p`2 = x`2 by A5,XXREAL_0:1;
then
A6: p = x by A4,TOPREAL3:6;
p in L~f by A2,XBOOLE_0:def 4;
then x in C /\ L~f by A1,A6,XBOOLE_0:def 4;
then C meets L~f;
hence contradiction by JORDAN10:5;
end;
theorem Th77:
x in C & p in west_halfline x /\ L~Cage(C,n) implies p`1 < x`1
proof
set f = Cage(C,n);
assume
A1: x in C;
assume
A2: p in west_halfline x /\ L~f;
then
A3: p in west_halfline x by XBOOLE_0:def 4;
then
A4: p`2 = x`2 by TOPREAL1:def 13;
assume
A5: p`1 >= x`1;
p`1 <= x`1 by A3,TOPREAL1:def 13;
then p`1 = x`1 by A5,XXREAL_0:1;
then
A6: p = x by A4,TOPREAL3:6;
p in L~f by A2,XBOOLE_0:def 4;
then x in C /\ L~f by A1,A6,XBOOLE_0:def 4;
then C meets L~f;
hence contradiction by JORDAN10:5;
end;
theorem Th78:
x in N-most C & p in north_halfline x & 1 <= i & i < len Cage(C,
n) & p in LSeg(Cage(C,n),i) implies LSeg(Cage(C,n),i) is horizontal
proof
set G = Gauge(C,n), f = Cage(C,n);
assume that
A1: x in N-most C and
A2: p in north_halfline x and
A3: 1 <= i and
A4: i < len f and
A5: p in LSeg(f,i);
assume
A6: not thesis;
A7: i+1 <= len f by A4,NAT_1:13;
then
A8: LSeg(f,i) = LSeg(f/.i,f/.(i+1)) by A3,TOPREAL1:def 3;
1 <= i+1 by A3,NAT_1:13;
then i+1 in Seg len f by A7,FINSEQ_1:1;
then
A9: i+1 in dom f by FINSEQ_1:def 3;
i in Seg len f by A3,A4,FINSEQ_1:1;
then
A10: i in dom f by FINSEQ_1:def 3;
A11: len G = width G by JORDAN8:def 1;
then
A12: len G-'1 <= width G by NAT_D:35;
A13: x in C by A1,XBOOLE_0:def 4;
p in L~f by A5,SPPOL_2:17;
then
A14: p in north_halfline x /\ L~f by A2,XBOOLE_0:def 4;
A15: f is_sequence_on G by JORDAN9:def 1;
A16: x`1 = p`1 by A2,TOPREAL1:def 10
.= (f/.i)`1 by A5,A8,A6,SPPOL_1:19,41;
A17: x`1 = p`1 by A2,TOPREAL1:def 10
.= (f/.(i+1))`1 by A5,A8,A6,SPPOL_1:19,41;
per cases;
suppose
A18: (f/.i)`2 <= (f/.(i+1))`2;
then p`2 <= (f/.(i+1))`2 by A5,A8,TOPREAL1:4;
then
A19: (f/.(i+1))`2 > x`2 by A13,A14,Th74,XXREAL_0:2;
consider i1,i2 being Nat such that
A20: [i1,i2] in Indices G and
A21: f/.(i+1) = G*(i1,i2) by A15,A9,GOBOARD1:def 9;
A22: 1 <= i2 by A20,MATRIX_0:32;
i2 <= width G by A20,MATRIX_0:32;
then
A23: i2 <= len G by JORDAN8:def 1;
A24: 1 <= i1 & i1 <= len G by A20,MATRIX_0:32;
consider j1,j2 being Nat such that
A25: [j1,j2] in Indices G and
A26: f/.i = G*(j1,j2) by A15,A10,GOBOARD1:def 9;
A27: 1 <= j1 & j1 <= len G by A25,MATRIX_0:32;
now
assume (f/.i)`2 = (f/.(i+1))`2;
then
A28: f/.i = f/.(i+1) by A17,A16,TOPREAL3:6;
then
A29: i2=j2 by A20,A21,A25,A26,GOBOARD1:5;
i1 = j1 & |.i1-j1.|+|.i2-j2.| = 1 by A15,A10,A9,A20,A21,A25,A26,A28,
GOBOARD1:5,def 9;
then 1 = 0 + |.i2-j2.| by GOBOARD7:2
.= 0 + 0 by A29,GOBOARD7:2;
hence contradiction;
end;
then
A30: (f/.i)`2 < (f/.(i+1))`2 by A18,XXREAL_0:1;
A31: 1 <= j2 by A25,MATRIX_0:32;
j2 <= width G by A25,MATRIX_0:32;
then i2 > j2 by A21,A22,A24,A26,A27,A30,Th19;
then len G > j2 by A23,XXREAL_0:2;
then
A32: len G-'1 >= j2 by NAT_D:49;
x`2 = (N-min C)`2 by A1,PSCOMP_1:39
.= N-bound C by EUCLID:52
.= G*(i1,len G-'1)`2 by A24,JORDAN8:14;
then x`2 >= (f/.i)`2 by A12,A24,A26,A31,A27,A32,Th19;
then x in L~f by A8,A17,A16,A19,GOBOARD7:7,SPPOL_2:17;
then L~f meets C by A13,XBOOLE_0:3;
hence contradiction by JORDAN10:5;
end;
suppose
A33: (f/.i)`2 >= (f/.(i+1))`2;
then p`2 <= (f/.i)`2 by A5,A8,TOPREAL1:4;
then
A34: (f/.i)`2 > x`2 by A13,A14,Th74,XXREAL_0:2;
consider i1,i2 being Nat such that
A35: [i1,i2] in Indices G and
A36: f/.i = G*(i1,i2) by A15,A10,GOBOARD1:def 9;
A37: 1 <= i2 by A35,MATRIX_0:32;
consider j1,j2 being Nat such that
A38: [j1,j2] in Indices G and
A39: f/.(i+1) = G*(j1,j2) by A15,A9,GOBOARD1:def 9;
A40: 1 <= j1 & j1 <= len G by A38,MATRIX_0:32;
now
assume (f/.i)`2 = (f/.(i+1))`2;
then
A41: f/.i = f/.(i+1) by A17,A16,TOPREAL3:6;
then
A42: i2=j2 by A35,A36,A38,A39,GOBOARD1:5;
i1 = j1 & |.j1-i1.|+|.j2-i2.| = 1 by A15,A10,A9,A35,A36,A38,A39,A41,
GOBOARD1:5,def 9;
then 1 = 0 + |.i2-j2.| by A42,GOBOARD7:2
.= 0 + 0 by A42,GOBOARD7:2;
hence contradiction;
end;
then
A43: (f/.(i+1))`2 < (f/.i)`2 by A33,XXREAL_0:1;
A44: i2 <= width G by A35,MATRIX_0:32;
A45: 1 <= i1 & i1 <= len G by A35,MATRIX_0:32;
A46: 1 <= j2 by A38,MATRIX_0:32;
j2 <= width G by A38,MATRIX_0:32;
then i2 > j2 by A36,A37,A45,A39,A40,A43,Th19;
then len G > j2 by A11,A44,XXREAL_0:2;
then
A47: len G-'1 >= j2 by NAT_D:49;
x`2 = (N-min C)`2 by A1,PSCOMP_1:39
.= N-bound C by EUCLID:52
.= G*(i1,len G-'1)`2 by A45,JORDAN8:14;
then x`2 >= (f/.(i+1))`2 by A12,A45,A39,A46,A40,A47,Th19;
then x in L~f by A8,A17,A16,A34,GOBOARD7:7,SPPOL_2:17;
then x in L~f /\ C by A13,XBOOLE_0:def 4;
then L~f meets C;
hence contradiction by JORDAN10:5;
end;
end;
theorem Th79:
x in E-most C & p in east_halfline x & 1 <= i & i < len Cage(C,
n) & p in LSeg(Cage(C,n),i) implies LSeg(Cage(C,n),i) is vertical
proof
set G = Gauge(C,n), f = Cage(C,n);
assume that
A1: x in E-most C and
A2: p in east_halfline x and
A3: 1 <= i and
A4: i < len f and
A5: p in LSeg(f,i);
assume
A6: not thesis;
A7: i+1 <= len f by A4,NAT_1:13;
then
A8: LSeg(f,i) = LSeg(f/.i,f/.(i+1)) by A3,TOPREAL1:def 3;
1 <= i+1 by A3,NAT_1:13;
then i+1 in Seg len f by A7,FINSEQ_1:1;
then
A9: i+1 in dom f by FINSEQ_1:def 3;
i in Seg len f by A3,A4,FINSEQ_1:1;
then
A10: i in dom f by FINSEQ_1:def 3;
p in L~f by A5,SPPOL_2:17;
then
A11: p in east_halfline x /\ L~f by A2,XBOOLE_0:def 4;
A12: f is_sequence_on G by JORDAN9:def 1;
A13: x`2 = p`2 by A2,TOPREAL1:def 11
.= (f/.i)`2 by A5,A8,A6,SPPOL_1:19,40;
A14: x`2 = p`2 by A2,TOPREAL1:def 11
.= (f/.(i+1))`2 by A5,A8,A6,SPPOL_1:19,40;
A15: len G = width G by JORDAN8:def 1;
then
A16: len G-'1 <= width G by NAT_D:35;
A17: x in C by A1,XBOOLE_0:def 4;
per cases;
suppose
A18: (f/.i)`1 <= (f/.(i+1))`1;
then p`1 <= (f/.(i+1))`1 by A5,A8,TOPREAL1:3;
then
A19: (f/.(i+1))`1 > x`1 by A17,A11,Th75,XXREAL_0:2;
consider i1,i2 being Nat such that
A20: [i1,i2] in Indices G and
A21: f/.(i+1) = G*(i1,i2) by A12,A9,GOBOARD1:def 9;
A22: 1 <= i2 & i2 <= width G by A20,MATRIX_0:32;
consider j1,j2 being Nat such that
A23: [j1,j2] in Indices G and
A24: f/.i = G*(j1,j2) by A12,A10,GOBOARD1:def 9;
A25: 1 <= j2 & j2 <= width G by A23,MATRIX_0:32;
A26: i1 <= len G by A20,MATRIX_0:32;
A27: 1 <= i1 by A20,MATRIX_0:32;
now
assume (f/.i)`1 = (f/.(i+1))`1;
then
A28: f/.i = f/.(i+1) by A14,A13,TOPREAL3:6;
then
A29: i2=j2 by A20,A21,A23,A24,GOBOARD1:5;
i1 = j1 & |.i1-j1.|+|.i2-j2.| = 1 by A12,A10,A9,A20,A21,A23,A24,A28,
GOBOARD1:5,def 9;
then 1 = 0 + |.i2-j2.| by GOBOARD7:2
.= 0 + 0 by A29,GOBOARD7:2;
hence contradiction;
end;
then
A30: (f/.i)`1 < (f/.(i+1))`1 by A18,XXREAL_0:1;
A31: 1 <= j1 by A23,MATRIX_0:32;
j1 <= len G by A23,MATRIX_0:32;
then i1 > j1 by A21,A22,A27,A24,A25,A30,Th18;
then len G > j1 by A26,XXREAL_0:2;
then
A32: len G-'1 >= j1 by NAT_D:49;
x`1 = (E-min C)`1 by A1,PSCOMP_1:47
.= E-bound C by EUCLID:52
.= G*(len G-'1,i2)`1 by A15,A22,JORDAN8:12;
then x`1 >= (f/.i)`1 by A15,A16,A22,A24,A25,A31,A32,Th18;
then x in L~f by A8,A14,A13,A19,GOBOARD7:8,SPPOL_2:17;
then x in L~f /\ C by A17,XBOOLE_0:def 4;
then L~f meets C;
hence contradiction by JORDAN10:5;
end;
suppose
A33: (f/.i)`1 >= (f/.(i+1))`1;
then p`1 <= (f/.i)`1 by A5,A8,TOPREAL1:3;
then
A34: (f/.i)`1 > x`1 by A17,A11,Th75,XXREAL_0:2;
consider i1,i2 being Nat such that
A35: [i1,i2] in Indices G and
A36: f/.i = G*(i1,i2) by A12,A10,GOBOARD1:def 9;
A37: 1 <= i2 & i2 <= width G by A35,MATRIX_0:32;
consider j1,j2 being Nat such that
A38: [j1,j2] in Indices G and
A39: f/.(i+1) = G*(j1,j2) by A12,A9,GOBOARD1:def 9;
A40: 1 <= j2 & j2 <= width G by A38,MATRIX_0:32;
A41: i1 <= len G by A35,MATRIX_0:32;
A42: 1 <= i1 by A35,MATRIX_0:32;
now
assume (f/.i)`1 = (f/.(i+1))`1;
then
A43: f/.i = f/.(i+1) by A14,A13,TOPREAL3:6;
then
A44: i2=j2 by A35,A36,A38,A39,GOBOARD1:5;
i1 = j1 & |.j1-i1.|+|.j2-i2.| = 1 by A12,A10,A9,A35,A36,A38,A39,A43,
GOBOARD1:5,def 9;
then 1 = 0 + |.i2-j2.| by A44,GOBOARD7:2
.= 0 + 0 by A44,GOBOARD7:2;
hence contradiction;
end;
then
A45: (f/.(i+1))`1 < (f/.i)`1 by A33,XXREAL_0:1;
A46: 1 <= j1 by A38,MATRIX_0:32;
j1 <= len G by A38,MATRIX_0:32;
then i1 > j1 by A36,A37,A42,A39,A40,A45,Th18;
then len G > j1 by A41,XXREAL_0:2;
then
A47: len G-'1 >= j1 by NAT_D:49;
x`1 = (E-min C)`1 by A1,PSCOMP_1:47
.= E-bound C by EUCLID:52
.= G*(len G-'1,i2)`1 by A15,A37,JORDAN8:12;
then x`1 >= (f/.(i+1))`1 by A15,A16,A37,A39,A40,A46,A47,Th18;
then x in L~f by A8,A14,A13,A34,GOBOARD7:8,SPPOL_2:17;
then x in L~f /\ C by A17,XBOOLE_0:def 4;
then L~f meets C;
hence contradiction by JORDAN10:5;
end;
end;
theorem Th80:
x in S-most C & p in south_halfline x & 1 <= i & i < len Cage(C
,n) & p in LSeg(Cage(C,n),i) implies LSeg(Cage(C,n),i) is horizontal
proof
set G = Gauge(C,n), f = Cage(C,n);
assume that
A1: x in S-most C and
A2: p in south_halfline x and
A3: 1 <= i and
A4: i < len f and
A5: p in LSeg(f,i);
assume
A6: not thesis;
A7: i+1 <= len f by A4,NAT_1:13;
then
A8: LSeg(f,i) = LSeg(f/.i,f/.(i+1)) by A3,TOPREAL1:def 3;
1 <= i+1 by A3,NAT_1:13;
then i+1 in Seg len f by A7,FINSEQ_1:1;
then
A9: i+1 in dom f by FINSEQ_1:def 3;
p in L~f by A5,SPPOL_2:17;
then
A10: p in south_halfline x /\ L~f by A2,XBOOLE_0:def 4;
A11: f is_sequence_on G by JORDAN9:def 1;
A12: x`1 = p`1 by A2,TOPREAL1:def 12
.= (f/.i)`1 by A5,A8,A6,SPPOL_1:19,41;
i in Seg len f by A3,A4,FINSEQ_1:1;
then
A13: i in dom f by FINSEQ_1:def 3;
A14: x`1 = p`1 by A2,TOPREAL1:def 12
.= (f/.(i+1))`1 by A5,A8,A6,SPPOL_1:19,41;
A15: x in C by A1,XBOOLE_0:def 4;
per cases;
suppose
A16: (f/.i)`2 <= (f/.(i+1))`2;
then (f/.i)`2 <= p`2 by A5,A8,TOPREAL1:4;
then
A17: (f/.i)`2 < x`2 by A15,A10,Th76,XXREAL_0:2;
consider i1,i2 being Nat such that
A18: [i1,i2] in Indices G and
A19: f/.i = G*(i1,i2) by A11,A13,GOBOARD1:def 9;
A20: i2 <= width G by A18,MATRIX_0:32;
A21: 1 <= i2 by A18,MATRIX_0:32;
A22: 1 <= i1 & i1 <= len G by A18,MATRIX_0:32;
A23: x`2 = (S-min C)`2 by A1,PSCOMP_1:55
.= S-bound C by EUCLID:52
.= G*(i1,2)`2 by A22,JORDAN8:13;
then i2 < 1+1 by A17,A19,A20,A22,SPRECT_3:12;
then
A24: i2 <= 1 by NAT_1:13;
consider j1,j2 being Nat such that
A25: [j1,j2] in Indices G and
A26: f/.(i+1) = G*(j1,j2) by A11,A9,GOBOARD1:def 9;
A27: j2 <= width G by A25,MATRIX_0:32;
now
assume (f/.i)`2 = (f/.(i+1))`2;
then
A28: f/.i = f/.(i+1) by A14,A12,TOPREAL3:6;
then
A29: i1 = j1 by A18,A19,A25,A26,GOBOARD1:5;
A30: i2=j2 by A18,A19,A25,A26,A28,GOBOARD1:5;
|.i1-j1.|+|.i2-j2.| = 1 by A11,A13,A9,A18,A19,A25,A26,GOBOARD1:def 9;
then 1 = 0 + |.i2-j2.| by A29,GOBOARD7:2
.= 0 + 0 by A30,GOBOARD7:2;
hence contradiction;
end;
then
A31: (f/.i)`2 < (f/.(i+1))`2 by A16,XXREAL_0:1;
A32: 1 <= j1 & j1 <= len G by A25,MATRIX_0:32;
1 <= j2 by A25,MATRIX_0:32;
then i2 < j2 by A19,A20,A22,A26,A32,A31,Th19;
then 1 < j2 by A21,A24,XXREAL_0:1;
then 1+1 <= j2 by NAT_1:13;
then x`2 <= (f/.(i+1))`2 by A22,A23,A26,A27,A32,Th19;
then x in L~f by A8,A14,A12,A17,GOBOARD7:7,SPPOL_2:17;
then x in L~f /\ C by A15,XBOOLE_0:def 4;
then L~f meets C;
hence contradiction by JORDAN10:5;
end;
suppose
A33: (f/.i)`2 >= (f/.(i+1))`2;
then (f/.(i+1))`2 <= p`2 by A5,A8,TOPREAL1:4;
then
A34: (f/.(i+1))`2 < x`2 by A15,A10,Th76,XXREAL_0:2;
consider i1,i2 being Nat such that
A35: [i1,i2] in Indices G and
A36: f/.(i+1) = G*(i1,i2) by A11,A9,GOBOARD1:def 9;
A37: i2 <= width G by A35,MATRIX_0:32;
A38: 1 <= i2 by A35,MATRIX_0:32;
A39: 1 <= i1 & i1 <= len G by A35,MATRIX_0:32;
A40: x`2 = (S-min C)`2 by A1,PSCOMP_1:55
.= S-bound C by EUCLID:52
.= G*(i1,2)`2 by A39,JORDAN8:13;
then i2 < 1+1 by A34,A36,A37,A39,SPRECT_3:12;
then
A41: i2 <= 1 by NAT_1:13;
consider j1,j2 being Nat such that
A42: [j1,j2] in Indices G and
A43: f/.i = G*(j1,j2) by A11,A13,GOBOARD1:def 9;
A44: j2 <= width G by A42,MATRIX_0:32;
now
assume (f/.i)`2 = (f/.(i+1))`2;
then
A45: f/.i = f/.(i+1) by A14,A12,TOPREAL3:6;
then
A46: i1 = j1 by A35,A36,A42,A43,GOBOARD1:5;
A47: i2=j2 by A35,A36,A42,A43,A45,GOBOARD1:5;
|.j1-i1.|+|.j2-i2.| = 1 by A11,A13,A9,A35,A36,A42,A43,GOBOARD1:def 9;
then 1 = 0 + |.i2-j2.| by A46,A47,GOBOARD7:2
.= 0 + 0 by A47,GOBOARD7:2;
hence contradiction;
end;
then
A48: (f/.(i+1))`2 < (f/.i)`2 by A33,XXREAL_0:1;
A49: 1 <= j1 & j1 <= len G by A42,MATRIX_0:32;
1 <= j2 by A42,MATRIX_0:32;
then i2 < j2 by A36,A37,A39,A43,A49,A48,Th19;
then 1 < j2 by A38,A41,XXREAL_0:1;
then 1+1 <= j2 by NAT_1:13;
then x`2 <= (f/.i)`2 by A39,A40,A43,A44,A49,Th19;
then x in L~f by A8,A14,A12,A34,GOBOARD7:7,SPPOL_2:17;
then x in L~f /\ C by A15,XBOOLE_0:def 4;
then L~f meets C;
hence contradiction by JORDAN10:5;
end;
end;
theorem Th81:
x in W-most C & p in west_halfline x & 1 <= i & i < len Cage(C,
n) & p in LSeg(Cage(C,n),i) implies LSeg(Cage(C,n),i) is vertical
proof
set G = Gauge(C,n), f = Cage(C,n);
assume that
A1: x in W-most C and
A2: p in west_halfline x and
A3: 1 <= i and
A4: i < len f and
A5: p in LSeg(f,i);
assume
A6: not thesis;
A7: i+1 <= len f by A4,NAT_1:13;
then
A8: LSeg(f,i) = LSeg(f/.i,f/.(i+1)) by A3,TOPREAL1:def 3;
1 <= i+1 by A3,NAT_1:13;
then i+1 in Seg len f by A7,FINSEQ_1:1;
then
A9: i+1 in dom f by FINSEQ_1:def 3;
p in L~f by A5,SPPOL_2:17;
then
A10: p in west_halfline x /\ L~f by A2,XBOOLE_0:def 4;
A11: f is_sequence_on G by JORDAN9:def 1;
A12: x`2 = p`2 by A2,TOPREAL1:def 13
.= (f/.i)`2 by A5,A8,A6,SPPOL_1:19,40;
i in Seg len f by A3,A4,FINSEQ_1:1;
then
A13: i in dom f by FINSEQ_1:def 3;
A14: x`2 = p`2 by A2,TOPREAL1:def 13
.= (f/.(i+1))`2 by A5,A8,A6,SPPOL_1:19,40;
A15: x in C by A1,XBOOLE_0:def 4;
per cases;
suppose
A16: (f/.i)`1 <= (f/.(i+1))`1;
consider i1,i2 being Nat such that
A17: [i1,i2] in Indices G and
A18: f/.i = G*(i1,i2) by A11,A13,GOBOARD1:def 9;
A19: 1 <= i2 by A17,MATRIX_0:32;
A20: i2 <= width G by A17,MATRIX_0:32;
then
A21: i2 <= len G by JORDAN8:def 1;
consider j1,j2 being Nat such that
A22: [j1,j2] in Indices G and
A23: f/.(i+1) = G*(j1,j2) by A11,A9,GOBOARD1:def 9;
A24: 1 <= j2 & j2 <= width G by A22,MATRIX_0:32;
now
assume (f/.i)`1 = (f/.(i+1))`1;
then
A25: f/.i = f/.(i+1) by A14,A12,TOPREAL3:6;
then
A26: i1 = j1 by A17,A18,A22,A23,GOBOARD1:5;
A27: i2=j2 by A17,A18,A22,A23,A25,GOBOARD1:5;
|.i1-j1.|+|.i2-j2.| = 1 by A11,A13,A9,A17,A18,A22,A23,GOBOARD1:def 9;
then 1 = 0 + |.i2-j2.| by A26,GOBOARD7:2
.= 0 + 0 by A27,GOBOARD7:2;
hence contradiction;
end;
then
A28: (f/.i)`1 < (f/.(i+1))`1 by A16,XXREAL_0:1;
(f/.i)`1 <= p`1 by A5,A8,A16,TOPREAL1:3;
then
A29: (f/.i)`1 < x`1 by A15,A10,Th77,XXREAL_0:2;
A30: 1 <= i1 by A17,MATRIX_0:32;
A31: i1 <= len G by A17,MATRIX_0:32;
A32: x`1 = (W-min C)`1 by A1,PSCOMP_1:31
.= W-bound C by EUCLID:52
.= G*(2,i2)`1 by A19,A21,JORDAN8:11;
then i1 < 1+1 by A29,A18,A19,A20,A31,SPRECT_3:13;
then
A33: i1 <= 1 by NAT_1:13;
A34: j1 <= len G by A22,MATRIX_0:32;
1 <= j1 by A22,MATRIX_0:32;
then i1 < j1 by A18,A19,A20,A31,A23,A24,A28,Th18;
then 1 < j1 by A30,A33,XXREAL_0:1;
then 1+1 <= j1 by NAT_1:13;
then x`1 <= (f/.(i+1))`1 by A19,A20,A32,A23,A24,A34,Th18;
then x in L~f by A8,A14,A12,A29,GOBOARD7:8,SPPOL_2:17;
then x in L~f /\ C by A15,XBOOLE_0:def 4;
then L~f meets C;
hence contradiction by JORDAN10:5;
end;
suppose
A35: (f/.i)`1 >= (f/.(i+1))`1;
consider i1,i2 being Nat such that
A36: [i1,i2] in Indices G and
A37: f/.(i+1) = G*(i1,i2) by A11,A9,GOBOARD1:def 9;
A38: 1 <= i2 by A36,MATRIX_0:32;
A39: i2 <= width G by A36,MATRIX_0:32;
then
A40: i2 <= len G by JORDAN8:def 1;
consider j1,j2 being Nat such that
A41: [j1,j2] in Indices G and
A42: f/.i = G*(j1,j2) by A11,A13,GOBOARD1:def 9;
A43: 1 <= j2 & j2 <= width G by A41,MATRIX_0:32;
now
assume (f/.i)`1 = (f/.(i+1))`1;
then
A44: f/.i = f/.(i+1) by A14,A12,TOPREAL3:6;
then
A45: i1 = j1 by A36,A37,A41,A42,GOBOARD1:5;
A46: i2=j2 by A36,A37,A41,A42,A44,GOBOARD1:5;
|.j1-i1.|+|.j2-i2.| = 1 by A11,A13,A9,A36,A37,A41,A42,GOBOARD1:def 9;
then 1 = 0 + |.i2-j2.| by A45,A46,GOBOARD7:2
.= 0 + 0 by A46,GOBOARD7:2;
hence contradiction;
end;
then
A47: (f/.(i+1))`1 < (f/.i)`1 by A35,XXREAL_0:1;
(f/.(i+1))`1 <= p`1 by A5,A8,A35,TOPREAL1:3;
then
A48: (f/.(i+1))`1 < x`1 by A15,A10,Th77,XXREAL_0:2;
A49: 1 <= i1 by A36,MATRIX_0:32;
A50: i1 <= len G by A36,MATRIX_0:32;
A51: x`1 = (W-min C)`1 by A1,PSCOMP_1:31
.= W-bound C by EUCLID:52
.= G*(2,i2)`1 by A38,A40,JORDAN8:11;
then i1 < 1+1 by A48,A37,A38,A39,A50,SPRECT_3:13;
then
A52: i1 <= 1 by NAT_1:13;
A53: j1 <= len G by A41,MATRIX_0:32;
1 <= j1 by A41,MATRIX_0:32;
then i1 < j1 by A37,A38,A39,A50,A42,A43,A47,Th18;
then 1 < j1 by A49,A52,XXREAL_0:1;
then 1+1 <= j1 by NAT_1:13;
then x`1 <= (f/.i)`1 by A38,A39,A51,A42,A43,A53,Th18;
then x in L~f by A8,A14,A12,A48,GOBOARD7:8,SPPOL_2:17;
then x in L~f /\ C by A15,XBOOLE_0:def 4;
then L~f meets C;
hence contradiction by JORDAN10:5;
end;
end;
theorem Th82:
x in N-most C & p in north_halfline x /\ L~Cage(C,n) implies p
`2 = N-bound L~Cage(C,n)
proof
set G = Gauge(C,n), f = Cage(C,n);
A1: f is_sequence_on G by JORDAN9:def 1;
assume
A2: x in N-most C;
then
A3: x in C by XBOOLE_0:def 4;
assume
A4: p in north_halfline x /\ L~f;
then p in L~f by XBOOLE_0:def 4;
then consider i such that
A5: 1 <= i and
A6: i+1 <= len f and
A7: p in LSeg(f,i) by SPPOL_2:13;
A8: LSeg(f,i) = LSeg(f/.i,f/.(i+1)) by A5,A6,TOPREAL1:def 3;
A9: i < len f by A6,NAT_1:13;
then i in Seg len f by A5,FINSEQ_1:1;
then i in dom f by FINSEQ_1:def 3;
then consider i1, i2 being Nat such that
A10: [i1,i2] in Indices G and
A11: f/.i = G*(i1,i2) by A1,GOBOARD1:def 9;
A12: 1 <= i2 by A10,MATRIX_0:32;
p in north_halfline x by A4,XBOOLE_0:def 4;
then LSeg(f,i) is horizontal by A2,A5,A7,A9,Th78;
then (f/.i)`2 = (f/.(i+1))`2 by A8,SPPOL_1:15;
then
A13: p`2 = (f/.i)`2 by A7,A8,GOBOARD7:6;
A14: i2 <= width G by A10,MATRIX_0:32;
A15: 1 <= i1 & i1 <= len G by A10,MATRIX_0:32;
A16: len G-'1 <= len G by NAT_D:35;
A17: len G = width G by JORDAN8:def 1;
x`2 = (N-min C)`2 by A2,PSCOMP_1:39
.= N-bound C by EUCLID:52
.= G*(i1,len G-'1)`2 by A15,JORDAN8:14;
then i2 > len G-'1 by A3,A4,A11,A17,A12,A15,A13,A16,Th74,SPRECT_3:12;
then i2 >= len G-'1+1 by NAT_1:13;
then i2 >= len G by A12,XREAL_1:235,XXREAL_0:2;
then i2 = len G by A17,A14,XXREAL_0:1;
then f/.i in N-most L~f by A5,A9,A11,A17,A15,Th58;
hence thesis by A13,Th3;
end;
theorem Th83:
x in E-most C & p in east_halfline x /\ L~Cage(C,n) implies p`1
= E-bound L~Cage(C,n)
proof
set G = Gauge(C,n), f = Cage(C,n);
A1: f is_sequence_on G by JORDAN9:def 1;
assume
A2: x in E-most C;
then
A3: x in C by XBOOLE_0:def 4;
A4: len G-'1 <= len G by NAT_D:35;
A5: len G = width G by JORDAN8:def 1;
assume
A6: p in east_halfline x /\ L~f;
then p in L~f by XBOOLE_0:def 4;
then consider i such that
A7: 1 <= i and
A8: i+1 <= len f and
A9: p in LSeg(f,i) by SPPOL_2:13;
A10: LSeg(f,i) = LSeg(f/.i,f/.(i+1)) by A7,A8,TOPREAL1:def 3;
A11: i < len f by A8,NAT_1:13;
then i in Seg len f by A7,FINSEQ_1:1;
then i in dom f by FINSEQ_1:def 3;
then consider i1, i2 being Nat such that
A12: [i1,i2] in Indices G and
A13: f/.i = G*(i1,i2) by A1,GOBOARD1:def 9;
A14: 1 <= i2 & i2 <= width G by A12,MATRIX_0:32;
p in east_halfline x by A6,XBOOLE_0:def 4;
then LSeg(f,i) is vertical by A2,A7,A9,A11,Th79;
then (f/.i)`1 = (f/.(i+1))`1 by A10,SPPOL_1:16;
then
A15: p`1 = (f/.i)`1 by A9,A10,GOBOARD7:5;
A16: i1 <= len G by A12,MATRIX_0:32;
A17: 1 <= i1 by A12,MATRIX_0:32;
x`1 = (E-min C)`1 by A2,PSCOMP_1:47
.= E-bound C by EUCLID:52
.= G*(len G-'1,i2)`1 by A5,A14,JORDAN8:12;
then i1 > len G-'1 by A3,A6,A13,A14,A17,A15,A4,Th75,SPRECT_3:13;
then i1 >= len G-'1+1 by NAT_1:13;
then i1 >= len G by A17,XREAL_1:235,XXREAL_0:2;
then i1 = len G by A16,XXREAL_0:1;
then f/.i in E-most L~f by A7,A11,A13,A14,Th61;
hence thesis by A15,Th4;
end;
theorem Th84:
x in S-most C & p in south_halfline x /\ L~Cage(C,n) implies p
`2 = S-bound L~Cage(C,n)
proof
set G = Gauge(C,n), f = Cage(C,n);
A1: f is_sequence_on G by JORDAN9:def 1;
assume
A2: x in S-most C;
then
A3: x in C by XBOOLE_0:def 4;
assume
A4: p in south_halfline x /\ L~f;
then p in L~f by XBOOLE_0:def 4;
then consider i such that
A5: 1 <= i and
A6: i+1 <= len f and
A7: p in LSeg(f,i) by SPPOL_2:13;
A8: LSeg(f,i) = LSeg(f/.i,f/.(i+1)) by A5,A6,TOPREAL1:def 3;
A9: i < len f by A6,NAT_1:13;
then i in Seg len f by A5,FINSEQ_1:1;
then i in dom f by FINSEQ_1:def 3;
then consider i1, i2 being Nat such that
A10: [i1,i2] in Indices G and
A11: f/.i = G*(i1,i2) by A1,GOBOARD1:def 9;
A12: 1 <= i2 by A10,MATRIX_0:32;
p in south_halfline x by A4,XBOOLE_0:def 4;
then LSeg(f,i) is horizontal by A2,A5,A7,A9,Th80;
then (f/.i)`2 = (f/.(i+1))`2 by A8,SPPOL_1:15;
then
A13: p`2 = (f/.i)`2 by A7,A8,GOBOARD7:6;
A14: i2 <= width G by A10,MATRIX_0:32;
A15: 1 <= i1 & i1 <= len G by A10,MATRIX_0:32;
x`2 = (S-min C)`2 by A2,PSCOMP_1:55
.= S-bound C by EUCLID:52
.= G*(i1,2)`2 by A15,JORDAN8:13;
then i2 < 1+1 by A3,A4,A11,A14,A15,A13,Th76,SPRECT_3:12;
then i2 <= 1 by NAT_1:13;
then i2 = 1 by A12,XXREAL_0:1;
then f/.i in S-most L~f by A5,A9,A11,A15,Th60;
hence thesis by A13,Th5;
end;
theorem Th85:
x in W-most C & p in west_halfline x /\ L~Cage(C,n) implies p`1
= W-bound L~Cage(C,n)
proof
set G = Gauge(C,n), f = Cage(C,n);
A1: f is_sequence_on G by JORDAN9:def 1;
assume
A2: x in W-most C;
then
A3: x in C by XBOOLE_0:def 4;
A4: len G = width G by JORDAN8:def 1;
assume
A5: p in west_halfline x /\ L~f;
then p in L~f by XBOOLE_0:def 4;
then consider i such that
A6: 1 <= i and
A7: i+1 <= len f and
A8: p in LSeg(f,i) by SPPOL_2:13;
A9: LSeg(f,i) = LSeg(f/.i,f/.(i+1)) by A6,A7,TOPREAL1:def 3;
A10: i < len f by A7,NAT_1:13;
then i in Seg len f by A6,FINSEQ_1:1;
then i in dom f by FINSEQ_1:def 3;
then consider i1, i2 being Nat such that
A11: [i1,i2] in Indices G and
A12: f/.i = G*(i1,i2) by A1,GOBOARD1:def 9;
A13: 1 <= i2 & i2 <= width G by A11,MATRIX_0:32;
p in west_halfline x by A5,XBOOLE_0:def 4;
then LSeg(f,i) is vertical by A2,A6,A8,A10,Th81;
then (f/.i)`1 = (f/.(i+1))`1 by A9,SPPOL_1:16;
then
A14: p`1 = (f/.i)`1 by A8,A9,GOBOARD7:5;
A15: i1 <= len G by A11,MATRIX_0:32;
A16: 1 <= i1 by A11,MATRIX_0:32;
x`1 = (W-min C)`1 by A2,PSCOMP_1:31
.= W-bound C by EUCLID:52
.= G*(2,i2)`1 by A4,A13,JORDAN8:11;
then i1 < 1+1 by A3,A5,A12,A13,A15,A14,Th77,SPRECT_3:13;
then i1 <= 1 by NAT_1:13;
then i1 = 1 by A16,XXREAL_0:1;
then f/.i in W-most L~f by A6,A10,A12,A13,Th59;
hence thesis by A14,Th6;
end;
theorem
x in N-most C implies ex p being Point of TOP-REAL 2 st north_halfline
x /\ L~Cage(C,n) = {p}
proof
set f = Cage(C,n);
assume
A1: x in N-most C;
then x in C by XBOOLE_0:def 4;
then north_halfline x meets L~f by Th51;
then consider p being object such that
A2: p in north_halfline x and
A3: p in L~f by XBOOLE_0:3;
A4: p in north_halfline x /\ L~f by A2,A3,XBOOLE_0:def 4;
reconsider p as Point of TOP-REAL 2 by A2;
take p;
hereby
let a be object;
assume
A5: a in north_halfline x /\ L~f;
then reconsider y = a as Point of TOP-REAL 2;
y in north_halfline x by A5,XBOOLE_0:def 4;
then
A6: y`1 = x`1 by TOPREAL1:def 10
.= p`1 by A2,TOPREAL1:def 10;
p`2 = N-bound L~f by A1,A4,Th82
.= y`2 by A1,A5,Th82;
then y = p by A6,TOPREAL3:6;
hence a in {p} by TARSKI:def 1;
end;
thus thesis by A4,ZFMISC_1:31;
end;
theorem
x in E-most C implies ex p being Point of TOP-REAL 2 st east_halfline
x /\ L~Cage(C,n) = {p}
proof
set f = Cage(C,n);
assume
A1: x in E-most C;
then x in C by XBOOLE_0:def 4;
then east_halfline x meets L~f by Th52;
then consider p being object such that
A2: p in east_halfline x and
A3: p in L~f by XBOOLE_0:3;
A4: p in east_halfline x /\ L~f by A2,A3,XBOOLE_0:def 4;
reconsider p as Point of TOP-REAL 2 by A2;
take p;
hereby
let a be object;
assume
A5: a in east_halfline x /\ L~f;
then reconsider y = a as Point of TOP-REAL 2;
y in east_halfline x by A5,XBOOLE_0:def 4;
then
A6: y`2 = x`2 by TOPREAL1:def 11
.= p`2 by A2,TOPREAL1:def 11;
p`1 = E-bound L~f by A1,A4,Th83
.= y`1 by A1,A5,Th83;
then y = p by A6,TOPREAL3:6;
hence a in {p} by TARSKI:def 1;
end;
thus thesis by A4,ZFMISC_1:31;
end;
theorem
x in S-most C implies ex p being Point of TOP-REAL 2 st south_halfline
x /\ L~Cage(C,n) = {p}
proof
set f = Cage(C,n);
assume
A1: x in S-most C;
then x in C by XBOOLE_0:def 4;
then south_halfline x meets L~f by Th53;
then consider p being object such that
A2: p in south_halfline x and
A3: p in L~f by XBOOLE_0:3;
A4: p in south_halfline x /\ L~f by A2,A3,XBOOLE_0:def 4;
reconsider p as Point of TOP-REAL 2 by A2;
take p;
hereby
let a be object;
assume
A5: a in south_halfline x /\ L~f;
then reconsider y = a as Point of TOP-REAL 2;
y in south_halfline x by A5,XBOOLE_0:def 4;
then
A6: y`1 = x`1 by TOPREAL1:def 12
.= p`1 by A2,TOPREAL1:def 12;
p`2 = S-bound L~f by A1,A4,Th84
.= y`2 by A1,A5,Th84;
then y = p by A6,TOPREAL3:6;
hence a in {p} by TARSKI:def 1;
end;
thus thesis by A4,ZFMISC_1:31;
end;
theorem
x in W-most C implies ex p being Point of TOP-REAL 2 st west_halfline
x /\ L~Cage(C,n) = {p}
proof
set f = Cage(C,n);
assume
A1: x in W-most C;
then x in C by XBOOLE_0:def 4;
then west_halfline x meets L~f by Th54;
then consider p being object such that
A2: p in west_halfline x and
A3: p in L~f by XBOOLE_0:3;
A4: p in west_halfline x /\ L~f by A2,A3,XBOOLE_0:def 4;
reconsider p as Point of TOP-REAL 2 by A2;
take p;
hereby
let a be object;
assume
A5: a in west_halfline x /\ L~f;
then reconsider y = a as Point of TOP-REAL 2;
y in west_halfline x by A5,XBOOLE_0:def 4;
then
A6: y`2 = x`2 by TOPREAL1:def 13
.= p`2 by A2,TOPREAL1:def 13;
p`1 = W-bound L~f by A1,A4,Th85
.= y`1 by A1,A5,Th85;
then y = p by A6,TOPREAL3:6;
hence a in {p} by TARSKI:def 1;
end;
thus thesis by A4,ZFMISC_1:31;
end;