:: Gauges
:: by Czes\law Byli\'nski
::
:: Received January 22, 1999
:: Copyright (c) 1999-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, REAL_1, FINSEQ_1, MATRIX_1, GOBOARD1, RELAT_1,
PARTFUN1, ARYTM_3, COMPLEX1, ARYTM_1, XBOOLE_0, RFINSEQ, XXREAL_0,
PRE_TOPC, EUCLID, GOBOARD5, TOPREAL1, GOBOARD2, TREES_1, MCART_1, CARD_1,
NAT_1, FUNCT_1, ORDINAL4, RCOMP_1, SPPOL_1, PSCOMP_1, NEWTON, STRUCT_0,
ZFMISC_1, INCSP_1, JORDAN8, ORDINAL1;
notations TARSKI, XBOOLE_0, SUBSET_1, ZFMISC_1, ORDINAL1, NUMBERS, XCMPLX_0,
XREAL_0, REAL_1, COMPLEX1, NAT_1, NAT_D, FUNCT_1, PARTFUN1, FINSEQ_1,
NEWTON, RFINSEQ, STRUCT_0, MATRIX_0, MATRIX_1, PRE_TOPC, COMPTS_1,
EUCLID, TOPREAL1, GOBOARD1, GOBOARD2, SPPOL_1, PSCOMP_1, GOBOARD5,
XXREAL_0;
constructors NEWTON, RFINSEQ, NAT_D, COMPTS_1, GOBOARD2, SPPOL_1, GOBOARD5,
PSCOMP_1, GOBOARD1, RELSET_1, REAL_1;
registrations RELAT_1, XREAL_0, NAT_1, FINSEQ_1, STRUCT_0, EUCLID, GOBOARD2,
SPRECT_1, NEWTON, VALUED_0, ORDINAL1;
requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM;
definitions GOBOARD1, GOBOARD5, TOPREAL1, XBOOLE_0, SEQM_3;
expansions GOBOARD1, XBOOLE_0;
theorems ZFMISC_1, NAT_1, FINSEQ_1, MATRIX_0, GOBOARD1, FINSEQ_4, EUCLID,
FINSEQ_3, PSCOMP_1, SPRECT_1, FINSEQ_5, GOBOARD5, SPRECT_2, ABSVALUE,
UNIFORM1, SUBSET_1, GOBRD11, GOBOARD2, SPRECT_3, JORDAN5D, XBOOLE_0,
XCMPLX_1, XREAL_1, NEWTON, XXREAL_0, PARTFUN1, NAT_D, SEQM_3;
schemes MATRIX_0;
begin
reserve i,i1,i2,i9,i19,j,j1,j2,j9,j19,k,l,m,n for Nat;
reserve r,s,r9,s9 for Real;
reserve D for set,
f for FinSequence of D,
G for Matrix of D;
theorem
<*>D is_sequence_on G;
theorem
for D being non empty set, f being FinSequence of D, G being Matrix of D
st f is_sequence_on G holds f/^m is_sequence_on G
proof
let D be non empty set, f be FinSequence of D, G be Matrix of D such that
A1: for n st n in dom f ex i,j st [i,j] in Indices G & f/.n = G*(i,j) and
A2: for n st n in dom f & n+1 in dom f for m,k,i,j
st [m,k] in Indices G & [i,j] in Indices G & f/.n=G*(m,k) & f/.(n+1)=G*(i,j)
holds |.m-i.|+|.k-j.| = 1;
set g = f/^m;
hereby
let n;
assume
A3: n in dom g;
then consider i,j such that
A4: [i,j] in Indices G and
A5: f/.(n+m) = G*(i,j) by A1,FINSEQ_5:26;
take i,j;
thus [i,j] in Indices G by A4;
thus g/.n = G*(i,j) by A3,A5,FINSEQ_5:27;
end;
let n such that
A6: n in dom g and
A7: n+1 in dom g;
let i1,j1,i2,j2 such that
A8: [i1,j1] in Indices G and
A9: [i2,j2] in Indices G and
A10: g/.n = G*(i1,j1) and
A11: g/.(n+1) = G*(i2,j2);
A12: n+m in dom f by A6,FINSEQ_5:26;
A13: n+1+m = n+m+1;
then
A14: n+m+1 in dom f by A7,FINSEQ_5:26;
A15: f/.(n+m) = g/.n by A6,FINSEQ_5:27;
f/.(n+m+1) = g/.(n+1) by A7,A13,FINSEQ_5:27;
hence thesis by A2,A8,A9,A10,A11,A12,A14,A15;
end;
theorem Th3:
1 <= k & k+1 <= len f & f is_sequence_on G
implies ex i1,j1,i2,j2 being Nat st
[i1,j1] in Indices G & f/.k = G*(i1,j1) &
[i2,j2] in Indices G & f/.(k+1) = G*(i2,j2) &
(i1 = i2 & j1+1 = j2 or i1+1 = i2 & j1 = j2 or
i1 = i2+1 & j1 = j2 or i1 = i2 & j1 = j2+1)
proof
assume that
A1: 1 <= k and
A2: k+1 <= len f and
A3: f is_sequence_on G;
k <= k+1 by NAT_1:11;
then k <= len f by A2,XXREAL_0:2;
then
A4: k in dom f by A1,FINSEQ_3:25;
then consider i1,j1 being Nat such that
A5: [i1,j1] in Indices G and
A6: f/.k = G*(i1,j1) by A3;
k+1 >= 1 by NAT_1:11;
then
A7: k+1 in dom f by A2,FINSEQ_3:25;
then consider i2,j2 being Nat such that
A8: [i2,j2] in Indices G and
A9: f/.(k+1) = G*(i2,j2) by A3;
A10: |.i1-i2.|+|.j1-j2.| = 1 by A3,A4,A5,A6,A7,A8,A9;
now per cases by A10,SEQM_3:42;
case that
A11: |.i1-i2.| = 1 and
A12: j1 = j2;
i1-i2 = 1 or -(i1-i2) = 1 by A11,ABSVALUE:def 1;
hence i1 = i2+1 or i1+1 = i2;
thus j1 = j2 by A12;
end;
case that
A13: i1 = i2 and
A14: |.j1-j2.| = 1;
j1-j2 = 1 or -(j1-j2) = 1 by A14,ABSVALUE:def 1;
hence j1 = j2+1 or j1+1 = j2;
thus i1 = i2 by A13;
end;
end;
hence thesis by A5,A6,A8,A9;
end;
reserve G for Go-board,
p for Point of TOP-REAL 2;
theorem
for f being non empty FinSequence of TOP-REAL 2 st f is_sequence_on G
holds f is standard special
proof
let f be non empty FinSequence of TOP-REAL 2 such that
A1: f is_sequence_on G;
thus f is_sequence_on GoB f
proof
set F = GoB f;
thus for n st n in dom f
ex i,j st [i,j] in Indices GoB f & f/.n = (GoB f)*(i,j) by GOBOARD2:14;
let n such that
A2: n in dom f and
A3: n+1 in dom f;
let m,k,i,j such that
A4: [m,k] in Indices GoB f and
A5: [i,j] in Indices GoB f and
A6: f/.n = (GoB f)*(m,k) and
A7: f/.(n+1) = (GoB f)*(i,j);
A8: 1 <= m by A4,MATRIX_0:32;
A9: m <= len F by A4,MATRIX_0:32;
A10: 1 <= k by A4,MATRIX_0:32;
A11: k <= width F by A4,MATRIX_0:32;
A12: 1 <= i by A5,MATRIX_0:32;
A13: i <= len F by A5,MATRIX_0:32;
A14: 1 <= j by A5,MATRIX_0:32;
A15: j <= width F by A5,MATRIX_0:32;
then
A16: F*(i,j)`1 = F*(i,1)`1 by A12,A13,A14,GOBOARD5:2;
A17: F*(i,k)`1 = F*(i,1)`1 by A10,A11,A12,A13,GOBOARD5:2;
A18: F*(i,j)`2 = F*(1,j)`2 by A12,A13,A14,A15,GOBOARD5:1;
A19: F*(m,j)`2 = F*(1,j)`2 by A8,A9,A14,A15,GOBOARD5:1;
A20: 1 <= n by A2,FINSEQ_3:25;
n+1 <= len f by A3,FINSEQ_3:25;
then consider i1,j1,i2,j2 such that
A21: [i1,j1] in Indices G and
A22: f/.n = G*(i1,j1) and
A23: [i2,j2] in Indices G and
A24: f/.(n+1) = G*(i2,j2) and
A25: i1 = i2 & j1+1 = j2 or i1+1 = i2 & j1 = j2 or
i1 = i2+1 & j1 = j2 or i1 = i2 & j1 = j2+1 by A1,A20,Th3;
A26: 1 <= i1 by A21,MATRIX_0:32;
A27: i1 <= len G by A21,MATRIX_0:32;
A28: 1 <= j1 by A21,MATRIX_0:32;
A29: j1 <= width G by A21,MATRIX_0:32;
A30: 1 <= i2 by A23,MATRIX_0:32;
A31: i2 <= len G by A23,MATRIX_0:32;
A32: 1 <= j2 by A23,MATRIX_0:32;
A33: j2 <= width G by A23,MATRIX_0:32;
A34: G*(i1,j1)`1 = G*(i1,1)`1 by A26,A27,A28,A29,GOBOARD5:2;
A35: G*(i2,j2)`1 = G*(i2,1)`1 by A30,A31,A32,A33,GOBOARD5:2;
A36: G*(i1,j1)`2 = G*(1,j1)`2 by A26,A27,A28,A29,GOBOARD5:1;
A37: G*(i2,j1)`2 = G*(1,j1)`2 by A28,A29,A30,A31,GOBOARD5:1;
A38: k+1 >= 1 by NAT_1:12;
A39: j+1 >= 1 by NAT_1:12;
A40: m+1 >= 1 by NAT_1:12;
A41: i+1 >= 1 by NAT_1:12;
A42: k+1 > k by NAT_1:13;
A43: j+1 > j by NAT_1:13;
A44: m+1 > m by NAT_1:13;
A45: i+1 > i by NAT_1:13;
per cases by A25;
suppose
A46: i1 = i2 & j1+1 = j2;
now
assume m <> i;
then m < i or m > i by XXREAL_0:1;
hence contradiction by A6,A7,A8,A9,A10,A11,A12,A13,A16,A17,A22,A24,A34
,A35,A46,GOBOARD5:3;
end;
then
A47: |.m-i.| = 0 by ABSVALUE:2;
now
assume j <= k;
then
A48: F*(i,j)`2 <= F*(m,k)`2 by A8,A9,A11,A14,A18,A19,SPRECT_3:12;
j1 < j2 by A46,NAT_1:13;
hence contradiction by A6,A7,A22,A24,A28,A30,A31,A33,A36,A37,A48,
GOBOARD5:4;
end;
then
A49: k+1 <= j by NAT_1:13;
now
assume
A50: k+1 < j;
then
A51: k+1 < width F by A15,XXREAL_0:2;
then consider l,i9 such that
A52: l in dom f and
A53: [i9,k+1] in Indices F and
A54: f/.l = F*(i9,k+1) by JORDAN5D:8,NAT_1:12;
A55: 1 <= i9 by A53,MATRIX_0:32;
i9 <= len F by A53,MATRIX_0:32;
then
A56: F*(i9,k+1)`2 = F*(1,k+1)`2 by A38,A51,A55,GOBOARD5:1;
A57: F*(m,k+1)`2 = F*(1,k+1)`2 by A8,A9,A38,A51,GOBOARD5:1;
consider i19,j19 such that
A58: [i19,j19] in Indices G and
A59: f/.l = G*(i19,j19) by A1,A52;
A60: 1 <= i19 by A58,MATRIX_0:32;
A61: i19 <= len G by A58,MATRIX_0:32;
A62: 1 <= j19 by A58,MATRIX_0:32;
A63: j19 <= width G by A58,MATRIX_0:32;
A64: G*(i19,j1)`2 = G*(1,j1)`2 by A28,A29,A60,A61,GOBOARD5:1;
A65: G*(i2,j2)`2 = G*(1,j2)`2 by A30,A31,A32,A33,GOBOARD5:1;
A66: G*(i19,j2)`2 = G*(1,j2)`2 by A32,A33,A60,A61,GOBOARD5:1;
A67: now
assume j1 >= j19;
then G*(i19,j19)`2 <= G*(i1,j1)`2 by A29,A36,A60,A61,A62,A64,
SPRECT_3:12;
hence contradiction by A6,A8,A9,A10,A22,A42,A51,A54,A56,A57,A59,
GOBOARD5:4;
end;
now
assume j2 <= j19;
then G*(i2,j2)`2 <= G*(i19,j19)`2 by A32,A60,A61,A63,A65,A66,
SPRECT_3:12;
hence contradiction by A7,A8,A9,A15,A18,A19,A24,A38,A50,A54,A56,A57,A59,
GOBOARD5:4;
end;
hence contradiction by A46,A67,NAT_1:13;
end;
then k+1 = j by A49,XXREAL_0:1;
then |.j-k.| = 1 by ABSVALUE:def 1;
hence thesis by A47,UNIFORM1:11;
end;
suppose
A68: i1+1 = i2 & j1 = j2;
now
assume k <> j;
then k < j or k > j by XXREAL_0:1;
hence contradiction by A6,A7,A8,A9,A10,A11,A14,A15,A18,A19,A22,A24,A36
,A37,A68,GOBOARD5:4;
end;
then
A69: |.k-j.| = 0 by ABSVALUE:2;
now
assume i <= m;
then
A70: F*(i,j)`1 <= F*(m,k)`1 by A9,A10,A11,A12,A16,A17,SPRECT_3:13;
i1 < i2 by A68,NAT_1:13;
hence contradiction by A6,A7,A22,A24,A26,A28,A29,A31,A68,A70,GOBOARD5:3
;
end;
then
A71: m+1 <= i by NAT_1:13;
now
assume
A72: m+1 < i;
then
A73: m+1 < len F by A13,XXREAL_0:2;
then consider l,j9 such that
A74: l in dom f and
A75: [m+1,j9] in Indices F and
A76: f/.l = F*(m+1,j9) by JORDAN5D:7,NAT_1:12;
A77: 1 <= j9 by A75,MATRIX_0:32;
j9 <= width F by A75,MATRIX_0:32;
then
A78: F*(m+1,j9)`1 = F*(m+1,1)`1 by A40,A73,A77,GOBOARD5:2;
A79: F*(m+1,k)`1 = F*(m+1,1)`1 by A10,A11,A40,A73,GOBOARD5:2;
consider i19,j19 such that
A80: [i19,j19] in Indices G and
A81: f/.l = G*(i19,j19) by A1,A74;
A82: 1 <= i19 by A80,MATRIX_0:32;
A83: i19 <= len G by A80,MATRIX_0:32;
A84: 1 <= j19 by A80,MATRIX_0:32;
A85: j19 <= width G by A80,MATRIX_0:32;
then
A86: G*(i1,j19)`1 = G*(i1,1)`1 by A26,A27,A84,GOBOARD5:2;
A87: G*(i2,j2)`1 = G*(i2,1)`1 by A30,A31,A32,A33,GOBOARD5:2;
A88: G*(i2,j19)`1 = G*(i2,1)`1 by A30,A31,A84,A85,GOBOARD5:2;
A89: now
assume i1 >= i19;
then G*(i19,j19)`1 <= G*(i1,j1)`1 by A27,A34,A82,A84,A85,A86,
SPRECT_3:13;
hence contradiction by A6,A8,A10,A11,A22,A44,A73,A76,A78,A79,A81,
GOBOARD5:3;
end;
now
assume i2 <= i19;
then G*(i2,j2)`1 <= G*(i19,j19)`1 by A30,A83,A84,A85,A87,A88,
SPRECT_3:13;
hence contradiction by A7,A10,A11,A13,A16,A17,A24,A40,A72,A76,A78,A79
,A81,GOBOARD5:3;
end;
hence contradiction by A68,A89,NAT_1:13;
end;
then m+1 = i by A71,XXREAL_0:1;
then |.i-m.| = 1 by ABSVALUE:def 1;
hence thesis by A69,UNIFORM1:11;
end;
suppose
A90: i1 = i2+1 & j1 = j2;
now
assume k <> j;
then k < j or k > j by XXREAL_0:1;
hence contradiction by A6,A7,A8,A9,A10,A11,A14,A15,A18,A19,A22,A24,A36
,A37,A90,GOBOARD5:4;
end;
then
A91: |.k-j.| = 0 by ABSVALUE:2;
now
assume m <= i;
then
A92: F*(i,j)`1 >= F*(m,k)`1 by A8,A10,A11,A13,A16,A17,SPRECT_3:13;
i1 > i2 by A90,NAT_1:13;
hence contradiction by A6,A7,A22,A24,A27,A28,A29,A30,A90,A92,GOBOARD5:3
;
end;
then
A93: i+1 <= m by NAT_1:13;
now
assume
A94: i+1 < m;
then
A95: i+1 < len F by A9,XXREAL_0:2;
then consider l,j9 such that
A96: l in dom f and
A97: [i+1,j9] in Indices F and
A98: f/.l = F*(i+1,j9) by JORDAN5D:7,NAT_1:12;
A99: 1 <= j9 by A97,MATRIX_0:32;
j9 <= width F by A97,MATRIX_0:32;
then
A100: F*(i+1,j9)`1 = F*(i+1,1)`1 by A41,A95,A99,GOBOARD5:2;
A101: F*(i+1,k)`1 = F*(i+1,1)`1 by A10,A11,A41,A95,GOBOARD5:2;
A102: F*(i+1,j)`1 = F*(i+1,1)`1 by A14,A15,A41,A95,GOBOARD5:2;
consider i19,j19 such that
A103: [i19,j19] in Indices G and
A104: f/.l = G*(i19,j19) by A1,A96;
A105: 1 <= i19 by A103,MATRIX_0:32;
A106: i19 <= len G by A103,MATRIX_0:32;
A107: 1 <= j19 by A103,MATRIX_0:32;
A108: j19 <= width G by A103,MATRIX_0:32;
then
A109: G*(i1,j19)`1 = G*(i1,1)`1 by A26,A27,A107,GOBOARD5:2;
A110: G*(i2,j2)`1 = G*(i2,1)`1 by A30,A31,A32,A33,GOBOARD5:2;
A111: G*(i2,j19)`1 = G*(i2,1)`1 by A30,A31,A107,A108,GOBOARD5:2;
A112: now
assume i2 >= i19;
then G*(i19,j19)`1 <= G*(i2,j2)`1 by A31,A105,A107,A108,A110,A111,
SPRECT_3:13;
hence contradiction by A7,A12,A14,A15,A24,A45,A95,A98,A100,A102,A104,
GOBOARD5:3;
end;
now
assume i1 <= i19;
then G*(i1,j1)`1 <= G*(i19,j19)`1 by A26,A34,A106,A107,A108,A109,
SPRECT_3:13;
hence contradiction by A6,A9,A10,A11,A22,A41,A94,A98,A100,A101,A104,
GOBOARD5:3;
end;
hence contradiction by A90,A112,NAT_1:13;
end;
then i+1 = m by A93,XXREAL_0:1;
hence thesis by A91,ABSVALUE:def 1;
end;
suppose
A113: i1 = i2 & j1 = j2+1;
now
assume m <> i;
then m < i or m > i by XXREAL_0:1;
hence contradiction by A6,A7,A8,A9,A10,A11,A12,A13,A16,A17,A22,A24,A34
,A35,A113,GOBOARD5:3;
end;
then
A114: |.m-i.| = 0 by ABSVALUE:2;
now
assume j >= k;
then
A115: F*(i,j)`2 >= F*(m,k)`2 by A8,A9,A10,A15,A18,A19,SPRECT_3:12;
j1 > j2 by A113,NAT_1:13;
hence contradiction by A6,A7,A22,A24,A29,A30,A31,A32,A36,A37,A115,
GOBOARD5:4;
end;
then
A116: j+1 <= k by NAT_1:13;
now
assume
A117: j+1 < k;
then
A118: j+1 < width F by A11,XXREAL_0:2;
then consider l,i9 such that
A119: l in dom f and
A120: [i9,j+1] in Indices F and
A121: f/.l = F*(i9,j+1) by JORDAN5D:8,NAT_1:12;
A122: 1 <= i9 by A120,MATRIX_0:32;
i9 <= len F by A120,MATRIX_0:32;
then
A123: F*(i9,j+1)`2 = F*(1,j+1)`2 by A39,A118,A122,GOBOARD5:1;
A124: F*(i,j+1)`2 = F*(1,j+1)`2 by A12,A13,A39,A118,GOBOARD5:1;
A125: F*(m,j+1)`2 = F*(1,j+1)`2 by A8,A9,A39,A118,GOBOARD5:1;
consider i19,j19 such that
A126: [i19,j19] in Indices G and
A127: f/.l = G*(i19,j19) by A1,A119;
A128: 1 <= i19 by A126,MATRIX_0:32;
A129: i19 <= len G by A126,MATRIX_0:32;
A130: 1 <= j19 by A126,MATRIX_0:32;
A131: j19 <= width G by A126,MATRIX_0:32;
A132: G*(i19,j1)`2 = G*(1,j1)`2 by A28,A29,A128,A129,GOBOARD5:1;
A133: G*(i2,j2)`2 = G*(1,j2)`2 by A30,A31,A32,A33,GOBOARD5:1;
A134: G*(i19,j2)`2 = G*(1,j2)`2 by A32,A33,A128,A129,GOBOARD5:1;
A135: now
assume j2 >= j19;
then G*(i19,j19)`2 <= G*(i2,j2)`2 by A33,A128,A129,A130,A133,A134,
SPRECT_3:12;
hence contradiction by A7,A12,A13,A14,A24,A43,A118,A121,A123,A124
,A127,GOBOARD5:4;
end;
now
assume j1 <= j19;
then G*(i1,j1)`2 <= G*(i19,j19)`2 by A28,A36,A128,A129,A131,A132,
SPRECT_3:12;
hence contradiction by A6,A8,A9,A11,A22,A39,A117,A121,A123,A125,A127,
GOBOARD5:4;
end;
hence contradiction by A113,A135,NAT_1:13;
end;
then j+1 = k by A116,XXREAL_0:1;
hence thesis by A114,ABSVALUE:def 1;
end;
end;
thus f is special
proof
let i be Nat;
assume that
A136: 1 <= i and
A137: i+1 <= len f;
consider i1,j1,i2,j2 such that
A138: [i1,j1] in Indices G and
A139: f/.i = G*(i1,j1) and
A140: [i2,j2] in Indices G and
A141: f/.(i+1) = G*(i2,j2) and
A142: i1 = i2 & j1+1 = j2 or i1+1 = i2 & j1 = j2 or
i1 = i2+1 & j1 = j2 or i1 = i2 & j1 = j2+1 by A1,A136,A137,Th3;
A143: 1 <= i1 by A138,MATRIX_0:32;
A144: i1 <= len G by A138,MATRIX_0:32;
A145: 1 <= j1 by A138,MATRIX_0:32;
A146: j1 <= width G by A138,MATRIX_0:32;
A147: 1 <= i2 by A140,MATRIX_0:32;
A148: i2 <= len G by A140,MATRIX_0:32;
A149: 1 <= j2 by A140,MATRIX_0:32;
A150: j2 <= width G by A140,MATRIX_0:32;
A151: G*(i1,j1)`2 = G*(1,j1)`2 by A143,A144,A145,A146,GOBOARD5:1;
G*(i1,j1)`1 = G*(i1,1)`1 by A143,A144,A145,A146,GOBOARD5:2;
hence thesis by A139,A141,A142,A147,A148,A149,A150,A151,GOBOARD5:1,2;
end;
end;
theorem
for f being non empty FinSequence of TOP-REAL 2 st
len f >= 2 & f is_sequence_on G holds f is non constant
proof
let f be non empty FinSequence of TOP-REAL 2 such that
A1: len f >= 2 and
A2: f is_sequence_on G;
assume
A3: for n,m st n in dom f & m in dom f holds f.n = f.m;
1 <= len f by A1,XXREAL_0:2;
then
A4: 1 in dom f by FINSEQ_3:25;
then consider i1,j1 such that
A5: [i1,j1] in Indices G and
A6: f/.1 = G*(i1,j1) by A2;
A7: 1+1 in dom f by A1,FINSEQ_3:25;
then consider i2,j2 such that
A8: [i2,j2] in Indices G and
A9: f/.2 = G*(i2,j2) by A2;
A10: f/.1 = f.1 by A4,PARTFUN1:def 6
.= f.2 by A3,A4,A7
.= f/.2 by A7,PARTFUN1:def 6;
then
A11: i1 = i2 by A5,A6,A8,A9,GOBOARD1:5;
A12: j1 = j2 by A5,A6,A8,A9,A10,GOBOARD1:5;
A13: |.i1-i2.| = 0 by A11,ABSVALUE:2;
|.i1-i2.| + |.j1-j2.| = 1 by A2,A4,A5,A6,A7,A8,A9;
hence contradiction by A12,A13;
end;
theorem
for f being non empty FinSequence of TOP-REAL 2 st f is_sequence_on G &
(ex i,j being Nat st [i,j] in Indices G & p = G*(i,j)) &
(for i1,j1,i2,j2 st [i1,j1] in Indices G & [i2,j2] in Indices G &
f/.len f = G*(i1,j1) & p = G*(i2,j2) holds |.i2-i1.|+|.j2-j1.| = 1)
holds f^<*p*> is_sequence_on G
proof
let f be non empty FinSequence of TOP-REAL 2 such that
A1: f is_sequence_on G and
A2: ex i,j st [i,j] in Indices G & p = G*(i,j) and
A3: for i1,j1,i2,j2 st [i1,j1] in Indices G & [i2,j2] in Indices G &
f/.len f = G*(i1,j1) & p = G*(i2,j2) holds |.i2-i1.|+|.j2-j1.| = 1;
A4: for n st n in dom f & n+1 in dom f holds
for m,k,i,j st [m,k] in Indices G & [i,j] in Indices G & f/.n=G*(m,k) &
f/.(n+1)=G*(i,j) holds |.m-i.|+|.k-j.|=1 by A1;
A5: now
let n;
assume that
A6: n in dom <*p*> and
A7: n+1 in dom <*p*>;
A8: 1 <= n by A6,FINSEQ_3:25;
A9: n+1 <= len <*p*> by A7,FINSEQ_3:25;
A10: 1+1 <= n+1 by A8,XREAL_1:6;
n+1 <= 1 by A9,FINSEQ_1:39;
hence for m,k,i,j st [m,k] in Indices G & [i,j] in Indices G &
<*p*>/.n=G*(m,k) & <*p*>/.(n+1)=G*(i,j)
holds |.m-i.|+|.k-j.|=1 by A10,XXREAL_0:2;
end;
now
let m,k,i,j such that
A11: [m,k] in Indices G and
A12: [i,j] in Indices G and
A13: f/.len f=G*(m,k) and
A14: <*p*>/.1=G*(i,j) and len f in dom f
and 1 in dom <*p*>;
<*p*>/.1 = p by FINSEQ_4:16;
then |.i-m.|+|.j-k.|=1 by A3,A11,A12,A13,A14;
hence 1 = |.m-i.|+|.j-k.| by UNIFORM1:11
.= |.m-i.|+|.k-j.| by UNIFORM1:11;
end;
then
A15: for n st n in dom(f^<*p*>) & n+1 in dom(f^<*p*>) holds
for m,k,i,j st [m,k] in Indices G & [i,j] in Indices G &
(f^<*p*>)/.n =G*(m,k) & (f^<*p*>)/.(n+1)=G*(i,j)
holds |.m-i.|+|.k-j.|=1 by A4,A5,GOBOARD1:24;
now
let n such that
A16: n in dom(f^<*p*>);
per cases by A16,FINSEQ_1:25;
suppose
A17: n in dom f;
then consider i,j such that
A18: [i,j] in Indices G and
A19: f/.n = G*(i,j) by A1;
take i,j;
thus [i,j] in Indices G by A18;
thus (f^<*p*>)/.n = G*(i,j) by A17,A19,FINSEQ_4:68;
end;
suppose ex l be Nat st l in dom <*p*> & n = (len f) + l;
then consider l be Nat such that
A20: l in dom <*p*> and
A21: n = (len f) + l;
consider i,j such that
A22: [i,j] in Indices G and
A23: p = G*(i,j) by A2;
take i,j;
thus [i,j] in Indices G by A22;
A24: l <= len <*p*> by A20,FINSEQ_3:25;
A25: 1 <= l by A20,FINSEQ_3:25;
l <= 1 by A24,FINSEQ_1:39;
then l = 1 by A25,XXREAL_0:1;
then <*p*>/.l = p by FINSEQ_4:16;
hence (f^<*p*>)/.n = G*(i,j) by A20,A21,A23,FINSEQ_4:69;
end;
end;
hence thesis by A15;
end;
theorem
i+k < len G & 1 <= j & j < width G & cell(G,i,j) meets cell(G,i+k,j)
implies k <= 1
proof
assume that
A1: i+k < len G and
A2: 1 <= j and
A3: j < width G and
A4: cell(G,i,j) meets cell(G,i+k,j) and
A5: k > 1;
cell(G,i,j) /\ cell(G,i+k,j) <> {} by A4;
then consider p such that
A6: p in cell(G,i,j) /\ cell(G,i+k,j) by SUBSET_1:4;
A7: p in cell(G,i,j) by A6,XBOOLE_0:def 4;
A8: p in cell(G,i+k,j) by A6,XBOOLE_0:def 4;
i+k >= 1 by A5,NAT_1:12;
then cell(G,i+k,j) = { |[r9,s9]| : G*(i+k,1)`1 <= r9 & r9 <= G*(i+k+1,1)`1 &
G*(1,j)`2 <= s9 & s9 <= G*(1,j+1)`2 } by A1,A2,A3,GOBRD11:32;
then consider r9,s9 such that
A9: p = |[r9,s9]| and
A10: G*(i+k,1)`1 <= r9 and r9 <= G*(i+k+1,1)`1
and G*(1,j)`2 <= s9
and s9 <= G*(1,j+1)`2 by A8;
A11: 1 < width G by A2,A3,XXREAL_0:2;
A12: i = 0 or i >= 1+0 by NAT_1:9;
per cases by A12;
suppose
A13: i = 0;
then cell(G,i,j) = {|[r,s]| : r <= G*(1,1)`1 & G*(1,j)`2 <= s & s <= G*
(1,j+1)`2} by A2,A3,GOBRD11:26;
then consider r,s such that
A14: p = |[r,s]| and
A15: r <= G*(1,1)`1 and G*(1,j)`2 <= s
and s <= G*(1,j+1)`2 by A7;
A16: k <= len G by A1,NAT_1:12;
A17: p`1 = r by A14,EUCLID:52;
p`1 = r9 by A9,EUCLID:52;
then G*(k,1)`1 <= G*(1,1)`1 by A10,A13,A15,A17,XXREAL_0:2;
hence contradiction by A5,A11,A16,GOBOARD5:3;
end;
suppose
A18: i >= 1;
i < len G by A1,NAT_1:12;
then cell(G,i,j) =
{|[r,s]|: G*(i,1)`1 <= r & r <= G*(i+1,1)`1 & G*(1,j)`2 <= s & s <=
G*(1,j+1)`2} by A2,A3,A18,GOBRD11:32;
then consider r,s such that
A19: p = |[r,s]| and G*(i,1)`1 <= r and
A20: r <= G*(i+1,1)`1 and G*(1,j)`2 <= s
and s <= G*(1,j+1)`2 by A7;
A21: 1 <= i+1 by NAT_1:12;
A22: i+1 < k+i by A5,XREAL_1:6;
A23: p`1 = r by A19,EUCLID:52;
p`1 = r9 by A9,EUCLID:52;
then G*(i+k,1)`1 <= G*(i+1,1)`1 by A10,A20,A23,XXREAL_0:2;
hence contradiction by A1,A11,A21,A22,GOBOARD5:3;
end;
end;
theorem Th8:
for C being non empty compact Subset of TOP-REAL 2
holds C is vertical iff E-bound C <= W-bound C
proof
let C be non empty compact Subset of TOP-REAL 2;
A1: E-bound C >= W-bound C by SPRECT_1:21;
C is vertical iff W-bound C = E-bound C by SPRECT_1:15;
hence thesis by A1,XXREAL_0:1;
end;
theorem Th9:
for C being non empty compact Subset of TOP-REAL 2
holds C is horizontal iff N-bound C <= S-bound C
proof
let C be non empty compact Subset of TOP-REAL 2;
A1: N-bound C >= S-bound C by SPRECT_1:22;
C is horizontal iff N-bound C = S-bound C by SPRECT_1:16;
hence thesis by A1,XXREAL_0:1;
end;
definition
let C be Subset of TOP-REAL 2, n be natural Number;
deffunc f(natural Number,natural Number) =
|[(W-bound C)+(((E-bound C)-(W-bound C))/(2|^n))*($1-2),
(S-bound C)+(((N-bound C)-(S-bound C))/(2|^n))*($2-2)]|;
func Gauge (C,n) -> Matrix of TOP-REAL 2 means
:Def1:
len it = 2|^n + 3 & len it = width it &
for i,j being Nat st [i,j] in Indices it holds
it*(i,j) = |[(W-bound C)+(((E-bound C)-(W-bound C))/(2|^n))*(i-2),
(S-bound C)+(((N-bound C)-(S-bound C))/(2|^n))*(j-2)]|;
existence
proof
consider M being Matrix of (2|^n + 3) ,(2|^n + 3), the carrier of TOP-REAL 2
such that
A1: for i,j being Nat st [i,j] in Indices M holds M*(i,j) = f(i,j)
from MATRIX_0:sch 1;
take M;
thus len M = 2|^n + 3 by MATRIX_0:def 2;
hence len M = width M by MATRIX_0:23;
thus thesis by A1;
end;
uniqueness
proof
let M1,M2 be Matrix of TOP-REAL 2 such that
A2: len M1 = 2|^n + 3 and
A3: len M1 = width M1 and
A4: for i,j being Nat st [i,j] in Indices M1 holds M1*(i,j) = f(i,j) and
A5: len M2 = 2|^n + 3 and
A6: len M2 = width M2 and
A7: for i,j being Nat st [i,j] in Indices M2 holds M2*(i,j) = f(i,j);
now
let i,j be Nat;
assume
A8: [i,j] in Indices M1;
A9: M1 is Matrix of (2|^n + 3) ,(2|^n + 3), the carrier of TOP-REAL 2 by A2,
A3,MATRIX_0:20;
M2 is Matrix of (2|^n + 3) ,(2|^n + 3), the carrier of TOP-REAL 2 by A5,
A6,MATRIX_0:20;
then
A10: [i,j] in Indices M2 by A8,A9,MATRIX_0:26;
thus M1*(i,j) = f(i,j) by A4,A8
.= M2*(i,j) by A7,A10;
end;
hence thesis by A2,A3,A5,A6,MATRIX_0:21;
end;
end;
registration
let C be non empty Subset of TOP-REAL 2, n be Nat;
cluster Gauge (C,n) -> non empty-yielding X_equal-in-line Y_equal-in-column;
coherence
proof
set M = Gauge (C,n);
A1: len M = 2|^n + 3 by Def1;
len M = width M by Def1;
hence M is non empty-yielding by A1,MATRIX_0:def 10;
A2: Indices M = [:dom M,Seg width M:] by MATRIX_0:def 4;
thus M is X_equal-in-line
proof
let i;
assume
A3: i in dom M;
set l= Line(M,i), f = X_axis(l);
let j1,j2 such that
A4: j1 in dom f and
A5: j2 in dom f;
len l = width M by MATRIX_0:def 7;
then
A6: dom l = Seg width M by FINSEQ_1:def 3;
A7: dom f = dom l by SPRECT_2:15;
then
A8: l/.j1 = l.j1 by A4,PARTFUN1:def 6
.= M*(i,j1) by A4,A6,A7,MATRIX_0:def 7;
A9: [i,j1] in Indices M by A2,A3,A4,A6,A7,ZFMISC_1:87;
A10: l/.j2 = l.j2 by A5,A7,PARTFUN1:def 6
.= M*(i,j2) by A5,A6,A7,MATRIX_0:def 7;
A11: [i,j2] in Indices M by A2,A3,A5,A6,A7,ZFMISC_1:87;
set x = (W-bound C)+(((E-bound C)-(W-bound C))/(2|^n))*(i-2);
set d = ((N-bound C)-(S-bound C))/(2|^n);
thus f.j1 = (l/.j1)`1 by A4,GOBOARD1:def 1
.= |[x,(S-bound C)+d*(j1-2)]|`1 by A8,A9,Def1
.= x by EUCLID:52
.= |[x,(S-bound C)+d*(j2-2)]|`1 by EUCLID:52
.= (l/.j2)`1 by A10,A11,Def1
.= f.j2 by A5,GOBOARD1:def 1;
end;
thus M is Y_equal-in-column
proof
let j;
assume
A12: j in Seg width M;
set c = Col(M,j), f = Y_axis(c);
let i1,i2 such that
A13: i1 in dom f and
A14: i2 in dom f;
len c = len M by MATRIX_0:def 8;
then
A15: dom c = dom M by FINSEQ_3:29;
A16: dom f = dom c by SPRECT_2:16;
then
A17: c/.i1 = c.i1 by A13,PARTFUN1:def 6
.= M*(i1,j) by A13,A15,A16,MATRIX_0:def 8;
A18: [i1,j] in Indices M by A2,A12,A13,A15,A16,ZFMISC_1:87;
A19: c/.i2 = c.i2 by A14,A16,PARTFUN1:def 6
.= M*(i2,j) by A14,A15,A16,MATRIX_0:def 8;
A20: [i2,j] in Indices M by A2,A12,A14,A15,A16,ZFMISC_1:87;
set y = (S-bound C)+(((N-bound C)-(S-bound C))/(2|^n))*(j-2);
set d = ((E-bound C)-(W-bound C))/(2|^n);
thus f.i1 = (c/.i1)`2 by A13,GOBOARD1:def 2
.= |[(W-bound C)+d*(i1-2),y]|`2 by A17,A18,Def1
.= y by EUCLID:52
.= |[(W-bound C)+d*(i2-2),y]|`2 by EUCLID:52
.= (c/.i2)`2 by A19,A20,Def1
.= f.i2 by A14,GOBOARD1:def 2;
end;
end;
end;
registration
let C be compact non vertical non horizontal non empty Subset of TOP-REAL 2,
n be Nat;
cluster Gauge (C,n) -> Y_increasing-in-line X_increasing-in-column;
coherence
proof
set M = Gauge (C,n);
A1: Indices M = [:dom M,Seg width M:] by MATRIX_0:def 4;
thus M is Y_increasing-in-line
proof
let i;
assume
A2: i in dom M;
set l = Line(M,i), f = Y_axis(l);
let j1,j2 be Nat such that
A3: j1 in dom f and
A4: j2 in dom f and
A5: j1 < j2;
len l = width M by MATRIX_0:def 7;
then
A6: dom l = Seg width M by FINSEQ_1:def 3;
A7: dom f = dom l by SPRECT_2:16;
then
A8: l/.j1 = l.j1 by A3,PARTFUN1:def 6
.= M*(i,j1) by A3,A6,A7,MATRIX_0:def 7;
A9: [i,j1] in Indices M by A1,A2,A3,A6,A7,ZFMISC_1:87;
A10: l/.j2 = l.j2 by A4,A7,PARTFUN1:def 6
.= M*(i,j2) by A4,A6,A7,MATRIX_0:def 7;
A11: [i,j2] in Indices M by A1,A2,A4,A6,A7,ZFMISC_1:87;
set x = (W-bound C)+(((E-bound C)-(W-bound C))/(2|^n))*(i-2);
set d = ((N-bound C)-(S-bound C))/(2|^n);
A12: f.j1 = (l/.j1)`2 by A3,GOBOARD1:def 2
.= |[x,(S-bound C)+d*(j1-2)]|`2 by A8,A9,Def1
.= (S-bound C)+d*(j1-2) by EUCLID:52;
A13: f.j2 = (l/.j2)`2 by A4,GOBOARD1:def 2
.= |[x,(S-bound C)+d*(j2-2)]|`2 by A10,A11,Def1
.= (S-bound C)+d*(j2-2) by EUCLID:52;
N-bound C > S-bound C by Th9;
then
A14: (N-bound C)-(S-bound C) > 0 by XREAL_1:50;
(2|^n) > 0 by NEWTON:83;
then
A15: d > 0 by A14,XREAL_1:139;
j1-2 < j2 -2 by A5,XREAL_1:9;
then d*(j1-2) < d*(j2-2) by A15,XREAL_1:68;
hence f.j1 < f.j2 by A12,A13,XREAL_1:8;
end;
let j;
assume
A16: j in Seg width M;
set c = Col(M,j), f = X_axis(c);
let i1,i2 such that
A17: i1 in dom f and
A18: i2 in dom f and
A19: i1 < i2;
len c = len M by MATRIX_0:def 8;
then
A20: dom c = dom M by FINSEQ_3:29;
A21: dom f = dom c by SPRECT_2:15;
then
A22: c/.i1 = c.i1 by A17,PARTFUN1:def 6
.= M*(i1,j) by A17,A20,A21,MATRIX_0:def 8;
A23: [i1,j] in Indices M by A1,A16,A17,A20,A21,ZFMISC_1:87;
A24: c/.i2 = c.i2 by A18,A21,PARTFUN1:def 6
.= M*(i2,j) by A18,A20,A21,MATRIX_0:def 8;
A25: [i2,j] in Indices M by A1,A16,A18,A20,A21,ZFMISC_1:87;
set y = (S-bound C)+(((N-bound C)-(S-bound C))/(2|^n))*(j-2);
set d = ((E-bound C)-(W-bound C))/(2|^n);
A26: f.i1 = (c/.i1)`1 by A17,GOBOARD1:def 1
.= |[(W-bound C)+d*(i1-2),y]|`1 by A22,A23,Def1
.= (W-bound C)+d*(i1-2) by EUCLID:52;
A27: f.i2 = (c/.i2)`1 by A18,GOBOARD1:def 1
.= |[(W-bound C)+d*(i2-2),y]|`1 by A24,A25,Def1
.= (W-bound C)+d*(i2-2) by EUCLID:52;
E-bound C > W-bound C by Th8;
then
A28: (E-bound C)-(W-bound C) > 0 by XREAL_1:50;
(2|^n) > 0 by NEWTON:83;
then
A29: d > 0 by A28,XREAL_1:139;
i1-2 < i2 -2 by A19,XREAL_1:9;
then d*(i1-2) < d*(i2-2) by A29,XREAL_1:68;
hence f.i1 < f.i2 by A26,A27,XREAL_1:8;
end;
end;
reserve T for non empty Subset of TOP-REAL 2;
theorem Th10:
for n being Nat holds len Gauge(T,n) >= 4
proof
let n be Nat;
set G = Gauge(T,n);
A1: len G = 2|^n + 3 by Def1;
2|^n >= n + 1 by NEWTON:85;
then
A2: len G >= n + 1 + 3 by A1,XREAL_1:6;
n+4 >= 4 by NAT_1:12;
hence thesis by A2,XXREAL_0:2;
end;
theorem
1 <= j & j <= len Gauge(T,n) implies Gauge(T,n)*(2,j)`1 = W-bound T
proof
set G = Gauge(T,n);
set W = W-bound T, S = S-bound T, E = E-bound T, N = N-bound T;
assume that
A1: 1 <= j and
A2: j <= len Gauge(T,n);
A3: len G = width G by Def1;
len G >= 4 by Th10;
then 2 <= len G by XXREAL_0:2;
then [2,j] in Indices G by A1,A2,A3,MATRIX_0:30;
then G*(2,j) = |[W+((E-W)/(2|^n))*(2-2), S+(N-S)/(2|^n)*(j-2)]| by Def1;
hence thesis by EUCLID:52;
end;
theorem
1 <= j & j <= len Gauge(T,n) implies
Gauge(T,n)*(len Gauge(T,n)-'1,j)`1 = E-bound T
proof
set G = Gauge(T,n);
set W = W-bound T, S = S-bound T, E = E-bound T, N = N-bound T;
assume that
A1: 1 <= j and
A2: j <= len Gauge(T,n);
A3: len G = 2|^n + 3 by Def1;
A4: len G = width G by Def1;
A5: len G >= 4 by Th10;
then 1 < len G by XXREAL_0:2;
then
A6: 1 <= (len G)-'1 by NAT_D:49;
A7: (len G)-'1-2 = (len G)-1-2 by A5,XREAL_1:233,XXREAL_0:2
.= 2|^n by A3;
A8: 2|^n > 0 by NEWTON:83;
(len G)-'1 <= len G by NAT_D:35;
then [(len G)-'1,j] in Indices G by A1,A2,A4,A6,MATRIX_0:30;
then G*((len G)-'1,j)
= |[W+((E-W)/(2|^n))*((len G)-'1-2), S+((N-S)/(2|^n))*(j-2)]| by Def1;
hence G*((len G)-'1,j)`1 = W+((E-W)/(2|^n))*(2|^n) by A7,EUCLID:52
.= W+(E-W) by A8,XCMPLX_1:87
.= E-bound T;
end;
theorem
1 <= i & i <= len Gauge(T,n) implies Gauge(T,n)*(i,2)`2 = S-bound T
proof
set G = Gauge(T,n);
set W = W-bound T, S = S-bound T, E = E-bound T, N = N-bound T;
assume that
A1: 1 <= i and
A2: i <= len Gauge(T,n);
A3: len G = width G by Def1;
len G >= 4 by Th10;
then 2 <= len G by XXREAL_0:2;
then [i,2] in Indices G by A1,A2,A3,MATRIX_0:30;
then G*(i,2) = |[W+((E-W)/(2|^n))*(i-2), S+((N-S)/(2|^n))*(2-2)]| by Def1;
hence thesis by EUCLID:52;
end;
theorem
1 <= i & i <= len Gauge(T,n) implies
Gauge(T,n)*(i,len Gauge(T,n)-'1)`2 = N-bound T
proof
set G = Gauge(T,n);
set W = W-bound T, S = S-bound T, E = E-bound T, N = N-bound T;
assume that
A1: 1 <= i and
A2: i <= len Gauge(T,n);
A3: len G = 2|^n + 3 by Def1;
A4: len G = width G by Def1;
A5: len G >= 4 by Th10;
then 1 < len G by XXREAL_0:2;
then
A6: 1 <= (len G)-'1 by NAT_D:49;
A7: (len G)-'1-2 = (len G)-1-2 by A5,XREAL_1:233,XXREAL_0:2
.= 2|^n by A3;
A8: 2|^n > 0 by NEWTON:83;
(len G)-'1 <= len G by NAT_D:35;
then [i,(len G)-'1] in Indices G by A1,A2,A4,A6,MATRIX_0:30;
then G*(i,(len G)-'1)
= |[W+((E-W)/(2|^n))*(i-2), S+((N-S)/(2|^n))*((len G)-'1-2)]| by Def1;
hence G*(i,(len G)-'1)`2 = S+((N-S)/(2|^n))*(2|^n) by A7,EUCLID:52
.= S+(N-S) by A8,XCMPLX_1:87
.= N-bound T;
end;
reserve C for
compact non vertical non horizontal non empty Subset of TOP-REAL 2;
reserve i, j, n for Nat;
theorem
i <= len Gauge(C,n) implies cell(Gauge(C,n),i,len Gauge(C,n)) misses C
proof
set G = Gauge(C,n);
assume
A1: i <= len G;
A2: len G = 2|^n + (1+2) by Def1;
A3: len G = width G by Def1;
assume cell(G,i,len G) /\ C <> {};
then consider p such that
A4: p in cell(G,i,len G) /\ C by SUBSET_1:4;
A5: p in cell(G,i,len G) by A4,XBOOLE_0:def 4;
A6: p in C by A4,XBOOLE_0:def 4;
4 <= len G by Th10;
then
A7: 1 <= len G by XXREAL_0:2;
set W = W-bound C, S = S-bound C, E = E-bound C, N = N-bound C;
set NS = (N-S)/(2|^n);
[1,width G] in Indices G by A3,A7,MATRIX_0:30;
then
A8: G*(1,width G) = |[W+((E-W)/(2|^n))*(1-2), S+NS*((width G)-2)]| by Def1;
A9: 2|^n > 0 by NEWTON:83;
N > S by Th9;
then
A10: N-S > 0 by XREAL_1:50;
NS*((width G)-2) =NS*(2|^n) + NS*1 by A2,A3
.= N-S+NS by A9,XCMPLX_1:87;
then G*(1,width G)`2 = N + NS by A8,EUCLID:52;
then
A11: G*(1,width G)`2 > N by A9,A10,XREAL_1:29,139;
A12: i = 0 or i >= 1+0 by NAT_1:9;
per cases by A1,A12,XXREAL_0:1;
suppose i = 0;
then cell(G,i,width G) = { |[r,s]| : r <= G*(1,1)`1 & G*(1,width G)`2 <= s }
by GOBRD11:25;
then consider r,s such that
A13: p = |[r,s]| and
r <= G*(1,1)`1 and
A14: G*(1,width G)`2 <= s by A3,A5;
p`2 = s by A13,EUCLID:52;
then N < p`2 by A11,A14,XXREAL_0:2;
hence contradiction by A6,PSCOMP_1:24;
end;
suppose i = len G;
then cell(G,i,width G)={|[r,s]| : G*(len G,1)`1 <= r & G*(1,width G)`2 <=
s } by GOBRD11:28;
then consider r,s such that
A15: p = |[r,s]| and
G*(len G,1)`1 <= r and
A16: G*(1,width G)`2 <= s by A3,A5;
p`2 = s by A15,EUCLID:52;
then N < p`2 by A11,A16,XXREAL_0:2;
hence contradiction by A6,PSCOMP_1:24;
end;
suppose 1 <= i & i < len G;
then cell(G,i,width G) = {|[r,s]|: G*(i,1)`1 <= r & r <= G*(i+1,1)`1 & G*
(1,width G)`2 <= s} by GOBRD11:31;
then consider r,s such that
A17: p = |[r,s]| and
G*(i,1)`1 <= r and r <= G*(i+1,1)`1 and
A18: G*(1,width G)`2 <= s by A3,A5;
p`2 = s by A17,EUCLID:52;
then N < p`2 by A11,A18,XXREAL_0:2;
hence contradiction by A6,PSCOMP_1:24;
end;
end;
theorem
j <= len Gauge(C,n) implies cell(Gauge(C,n),len Gauge(C,n),j) misses C
proof
set G = Gauge(C,n);
assume
A1: j <= len G;
A2: len G = 2|^n + (1+2) by Def1;
A3: len G = width G by Def1;
assume cell(G,len G,j) /\ C <> {};
then consider p such that
A4: p in cell(G,len G,j) /\ C by SUBSET_1:4;
A5: p in cell(G,len G,j) by A4,XBOOLE_0:def 4;
A6: p in C by A4,XBOOLE_0:def 4;
4 <= len G by Th10;
then
A7: 1 <= len G by XXREAL_0:2;
set W = W-bound C, S = S-bound C, E = E-bound C, N = N-bound C;
set EW = (E-W)/(2|^n);
[len G,1] in Indices G by A3,A7,MATRIX_0:30;
then
A8: G*(len G,1) = |[W+EW*((len G)-2), S+((N-S)/(2|^n))*(1-2)]| by Def1;
A9: 2|^n > 0 by NEWTON:83;
E > W by Th8;
then
A10: E-W > 0 by XREAL_1:50;
EW*((len G)-2) = EW*(2|^n) + EW*1 by A2
.= E-W+EW by A9,XCMPLX_1:87;
then G*(len G,1)`1 = E + EW by A8,EUCLID:52;
then
A11: G*(len G,1)`1 > E by A9,A10,XREAL_1:29,139;
A12: j = 0 or j >= 1+0 by NAT_1:9;
per cases by A1,A12,XXREAL_0:1;
suppose j = 0;
then cell(G,len G,j) = {|[r,s]| : G*(len G,1)`1 <= r & s <= G*(1,1)`2}
by GOBRD11:27;
then consider r,s such that
A13: p = |[r,s]| and
A14: G*(len G,1)`1 <= r and s <= G*(1,1)`2 by A5;
p`1 = r by A13,EUCLID:52;
then E < p`1 by A11,A14,XXREAL_0:2;
hence contradiction by A6,PSCOMP_1:24;
end;
suppose j = len G;
then cell(G,len G,j)={|[r,s]| : G*(len G,1)`1 <= r & G*(1,width G)`2 <= s}
by A3,GOBRD11:28;
then consider r,s such that
A15: p = |[r,s]| and
A16: G*(len G,1)`1 <= r and G*(1,width G)`2 <= s by A5;
p`1 = r by A15,EUCLID:52;
then E < p`1 by A11,A16,XXREAL_0:2;
hence contradiction by A6,PSCOMP_1:24;
end;
suppose 1 <= j & j < len G;
then cell(G,len G,j)
= { |[r,s]| : G*(len G,1)`1 <= r & G*(1,j)`2 <= s & s <= G*(1,j+1)`2 }
by A3,GOBRD11:29;
then consider r,s such that
A17: p = |[r,s]| and
A18: G*(len G,1)`1 <= r and G*(1,j)`2 <= s
and s <= G*(1,j+1)`2 by A5;
p`1 = r by A17,EUCLID:52;
then E < p`1 by A11,A18,XXREAL_0:2;
hence contradiction by A6,PSCOMP_1:24;
end;
end;
theorem
i <= len Gauge(C,n) implies cell(Gauge(C,n),i,0) misses C
proof
set G = Gauge(C,n);
assume
A1: i <= len G;
A2: len G = width G by Def1;
assume cell(G,i,0) /\ C <> {};
then consider p such that
A3: p in cell(G,i,0) /\ C by SUBSET_1:4;
A4: p in cell(G,i,0) by A3,XBOOLE_0:def 4;
A5: p in C by A3,XBOOLE_0:def 4;
4 <= len G by Th10;
then
A6: 1 <= len G by XXREAL_0:2;
set W = W-bound C, S = S-bound C, E = E-bound C, N = N-bound C;
set NS = (N-S)/(2|^n);
[1,1] in Indices G by A2,A6,MATRIX_0:30;
then G*(1,1) = |[W+((E-W)/(2|^n))*(1-2), S+NS*(1-2)]| by Def1;
then
A7: G*(1,1)`2 = S+NS*(-1) by EUCLID:52;
A8: 2|^n > 0 by NEWTON:83;
N > S by Th9;
then N-S > 0 by XREAL_1:50;
then NS > 0 by A8,XREAL_1:139;
then NS*(-1) < 0 * (-1) by XREAL_1:69;
then
A9: G*(1,1)`2 < S+0 by A7,XREAL_1:6;
A10: i = 0 or i >= 1+0 by NAT_1:9;
per cases by A1,A10,XXREAL_0:1;
suppose i = 0;
then cell(G,i,0) ={ |[r,s]| : r <= G*(1,1)`1 & s <= G*(1,1)`2 }
by GOBRD11:24;
then consider r,s such that
A11: p = |[r,s]| and
r <= G*(1,1)`1 and
A12: s <= G*(1,1)`2 by A4;
p`2 = s by A11,EUCLID:52;
then S > p`2 by A9,A12,XXREAL_0:2;
hence contradiction by A5,PSCOMP_1:24;
end;
suppose i = len G;
then cell(G,i,0)={ |[r,s]| : G*(len G,1)`1 <= r & s <= G*(1,1)`2 }
by GOBRD11:27;
then consider r,s such that
A13: p = |[r,s]| and
G*(len G,1)`1 <= r and
A14: s <= G*(1,1)`2 by A4;
p`2 = s by A13,EUCLID:52;
then S > p`2 by A9,A14,XXREAL_0:2;
hence contradiction by A5,PSCOMP_1:24;
end;
suppose 1 <= i & i < len G;
then cell(G,i,0) = { |[r,s]|: G*(i,1)`1 <= r & r <= G*(i+1,1)`1 & s <= G*
(1,1)`2 } by GOBRD11:30;
then consider r,s such that
A15: p = |[r,s]| and
G*(i,1)`1 <= r and r <= G*(i+1,1)`1 and
A16: s <= G*(1,1)`2 by A4;
p`2 = s by A15,EUCLID:52;
then S > p`2 by A9,A16,XXREAL_0:2;
hence contradiction by A5,PSCOMP_1:24;
end;
end;
theorem
j <= len Gauge(C,n) implies cell(Gauge(C,n),0,j) misses C
proof
set G = Gauge(C,n);
assume
A1: j <= len G;
A2: len G = width G by Def1;
assume cell(G,0,j) /\ C <> {};
then consider p such that
A3: p in cell(G,0,j) /\ C by SUBSET_1:4;
A4: p in cell(G,0,j) by A3,XBOOLE_0:def 4;
A5: p in C by A3,XBOOLE_0:def 4;
4 <= len G by Th10;
then
A6: 1 <= len G by XXREAL_0:2;
set W = W-bound C, S = S-bound C, E = E-bound C, N = N-bound C;
set EW = (E-W)/(2|^n);
[1,1] in Indices G by A2,A6,MATRIX_0:30;
then G*(1,1) = |[W+EW*(1-2), S+((N-S)/(2|^n))*(1-2)]| by Def1;
then
A7: G*(1,1)`1 = W+EW*(-1) by EUCLID:52;
A8: 2|^n > 0 by NEWTON:83;
E > W by Th8;
then E-W > 0 by XREAL_1:50;
then EW > 0 by A8,XREAL_1:139;
then EW*(-1) < 0 * (-1) by XREAL_1:69;
then
A9: G*(1,1)`1 < W+0 by A7,XREAL_1:6;
A10: j = 0 or j >= 1+0 by NAT_1:9;
per cases by A1,A10,XXREAL_0:1;
suppose j = 0;
then cell(G,0,j) = { |[r,s]| : r <= G*(1,1)`1 & s <= G*(1,1)`2 }
by GOBRD11:24;
then consider r,s such that
A11: p = |[r,s]| and
A12: r <= G*(1,1)`1 and s <= G*(1,1)`2 by A4;
p`1 = r by A11,EUCLID:52;
then W > p`1 by A9,A12,XXREAL_0:2;
hence contradiction by A5,PSCOMP_1:24;
end;
suppose j = len G;
then cell(G,0,j)={ |[r,s]| : r <= G*(1,1)`1 & G*(1,width G)`2 <= s }
by A2,GOBRD11:25;
then consider r,s such that
A13: p = |[r,s]| and
A14: r <= G*(1,1)`1 and G*(1,width G)`2 <= s by A4;
p`1 = r by A13,EUCLID:52;
then W > p`1 by A9,A14,XXREAL_0:2;
hence contradiction by A5,PSCOMP_1:24;
end;
suppose 1 <= j & j < len G;
then cell(G,0,j) = { |[r,s]| : r <= G*(1,1)`1 & G*(1,j)`2 <= s & s <=
G*(1,j+1)`2 } by A2,GOBRD11:26;
then consider r,s such that
A15: p = |[r,s]| and
A16: r <= G*(1,1)`1 and G*(1,j)`2 <= s
and s <= G*(1,j+1)`2 by A4;
p`1 = r by A15,EUCLID:52;
then W > p`1 by A9,A16,XXREAL_0:2;
hence contradiction by A5,PSCOMP_1:24;
end;
end;