:: Introduction to Go-Board - Part II.
:: Go-Board Determined by Finite Sequence of point from ${\calE}^2_{\rm T}$
:: by Jaros{\l}aw Kotowicz and Yatsuka Nakamura
::
:: Received August 24, 1992
:: Copyright (c) 1992-2017 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, PRE_TOPC, EUCLID, FINSEQ_1, REAL_1, SUBSET_1, GOBOARD1,
NAT_1, XBOOLE_0, CARD_1, ARYTM_3, XXREAL_0, TARSKI, ARYTM_1, RELAT_1,
ORDINAL4, PARTFUN1, FUNCT_1, RLTOPSP1, TOPREAL1, MCART_1, MATRIX_1,
INCSP_1, ZFMISC_1, TREES_1, ORDINAL2, COMPLEX1, STRUCT_0, GOBOARD2;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, CARD_1, NUMBERS,
XCMPLX_0, XREAL_0, COMPLEX1, REAL_1, NAT_1, RELAT_1, FUNCT_1, PARTFUN1,
FINSEQ_1, VALUED_0, STRUCT_0, PRE_TOPC, SEQ_4, MATRIX_0, MATRIX_1,
RLTOPSP1, EUCLID, TOPREAL1, GOBOARD1, XXREAL_0;
constructors PARTFUN1, SQUARE_1, NAT_1, COMPLEX1, SEQ_4, TOPREAL1, GOBOARD1,
XXREAL_2, SEQM_3, RELSET_1, DOMAIN_1, BINOP_2, RVSUM_1, REAL_1;
registrations RELSET_1, XXREAL_0, XREAL_0, NAT_1, FINSEQ_1, STRUCT_0, EUCLID,
VALUED_0, CARD_1, SEQM_3, SEQ_4, INT_1, ORDINAL1;
requirements NUMERALS, REAL, BOOLE, SUBSET, ARITHM;
definitions TARSKI, TOPREAL1, GOBOARD1, XBOOLE_0;
equalities TOPREAL1, XBOOLE_0;
expansions TOPREAL1, GOBOARD1, XBOOLE_0;
theorems TARSKI, NAT_1, ZFMISC_1, FUNCT_1, FINSEQ_1, ABSVALUE, SEQ_4,
FINSEQ_2, MATRIX_0, EUCLID, TOPREAL1, TOPREAL3, GOBOARD1, FINSEQ_4,
FINSEQ_3, PARTFUN2, INT_1, XBOOLE_0, XBOOLE_1, XREAL_1, COMPLEX1,
XXREAL_0, ORDINAL1, PARTFUN1, SEQM_3, RLTOPSP1;
schemes NAT_1, MATRIX_0, FINSEQ_4;
begin
reserve p,p1,p2,q for Point of TOP-REAL 2,
f,f1,f2,g,g1,g2 for FinSequence of TOP-REAL 2,
r,s for Real,
n,m,i,j,k for Nat,
G for Go-board,
x for set;
theorem
(for n,m st m>n+1 & n in dom f & n+1 in dom f & m in dom f & m+1 in
dom f holds LSeg(f,n) misses LSeg(f,m)) implies f is s.n.c.
proof
assume
A1: for n,m st m>n+1 & n in dom f & n+1 in dom f & m in dom f & m+1 in
dom f holds LSeg(f,n) misses LSeg(f,m);
let n,m be Nat such that
A2: m>n+1;
A3: n <= n+1 & m <= m+1 by NAT_1:11;
per cases;
suppose
n in dom f & n+1 in dom f & m in dom f & m+1 in dom f;
hence thesis by A1,A2;
end;
suppose
not(n in dom f & n+1 in dom f & m in dom f & m+1 in dom f);
then
not(1 <= n & n <= len f & 1 <= n+1 & n+1<= len f & 1 <= m & m <= len f
& 1 <= m+1 & m+1<= len f) by FINSEQ_3:25;
then not(1 <= n & n+1 <= len f & 1 <= m & m+1 <= len f) by A3,XXREAL_0:2;
then LSeg(f,m)={} or LSeg(f,n)={} by TOPREAL1:def 3;
hence thesis;
end;
end;
theorem
f is unfolded s.n.c. one-to-one & f/.len f in LSeg(f,i) & i in dom f &
i+1 in dom f implies i+1=len f
proof
assume that
A1: f is unfolded and
A2: f is s.n.c. and
A3: f is one-to-one and
A4: f/.len f in LSeg(f,i) and
A5: i in dom f and
A6: i+1 in dom f and
A7: i+1<>len f;
A8: 1<=i by A5,FINSEQ_3:25;
A9: i<=len f by A5,FINSEQ_3:25;
then reconsider l=len f - 1 as Element of NAT by A8,INT_1:5,XXREAL_0:2;
1<=len f by A8,A9,XXREAL_0:2;
then
A10: l+1 in dom f by FINSEQ_3:25;
A11: i+1<=len f by A6,FINSEQ_3:25;
then i+1l+1;
then
A18: f/.l<>f/.(l+1) by A3,A17,A10,PARTFUN2:10;
i+1+1=i+(1+1);
then
A19: LSeg(f,i)/\ LSeg(f,i+1)={f/.(i+1)} by A1,A8,A12;
now
per cases;
suppose
A20: l=i+1;
then f/.len f in LSeg(f,i) /\ LSeg(f,i+1) by A4,A16,XBOOLE_0:def 4;
hence contradiction by A18,A19,A20,TARSKI:def 1;
end;
suppose
l<>i+1;
then i+10 & len f = k+1 implies L~f = L~(f|k) \/ LSeg(f,k)
proof
assume that
A1: k<>0 and
A2: len f = k+1;
A3: 0+1<=k by A1,NAT_1:13;
set f1 = f|k, lf = {LSeg(f,i): 1<=i & i+1 <= len f}, l1 = {LSeg(f1,j): 1<=j
& j+1 <= len f1};
k<=len f by A2,NAT_1:13;
then
A4: len(f|k)=k by FINSEQ_1:59;
thus L~f c= L~(f|k) \/ LSeg(f,k)
proof
let x be object;
assume x in L~f;
then consider X be set such that
A5: x in X and
A6: X in lf by TARSKI:def 4;
consider n such that
A7: X=LSeg(f,n) and
A8: 1<=n and
A9: n+1 <= len f by A6;
now
per cases;
suppose
n+1 = len f;
hence thesis by A2,A5,A7,XBOOLE_0:def 3;
end;
suppose
A10: n+1 <> len f;
A11: 1<=n+1 by A8,NAT_1:13;
n<=k by A2,A9,XREAL_1:6;
then
A12: n in dom f1 by A4,A8,FINSEQ_3:25;
A13: n+1 < len f by A9,A10,XXREAL_0:1;
then n+1 <= k by A2,NAT_1:13;
then n+1 in dom f1 by A4,A11,FINSEQ_3:25;
then
A14: X=LSeg(f1,n) by A7,A12,TOPREAL3:17;
n+1<=k by A2,A13,NAT_1:13;
then X in l1 by A4,A8,A14;
then x in union l1 by A5,TARSKI:def 4;
hence thesis by XBOOLE_0:def 3;
end;
end;
hence thesis;
end;
A15: k<=k+1 by NAT_1:11;
let x be object such that
A16: x in L~f1 \/ LSeg(f,k);
now
per cases by A16,XBOOLE_0:def 3;
suppose
x in L~f1;
then consider X be set such that
A17: x in X and
A18: X in l1 by TARSKI:def 4;
consider n such that
A19: X=LSeg(f1,n) and
A20: 1<=n and
A21: n+1 <= len f1 by A18;
n<=n+1 by NAT_1:11;
then n<=len f1 by A21,XXREAL_0:2;
then
A22: n in dom f1 by A20,FINSEQ_3:25;
1<=n+1 by NAT_1:11;
then n+1 in dom f1 by A21,FINSEQ_3:25;
then
A23: X=LSeg(f,n) by A19,A22,TOPREAL3:17;
n+1<=len f by A2,A15,A4,A21,XXREAL_0:2;
then X in lf by A20,A23;
hence thesis by A17,TARSKI:def 4;
end;
suppose
A24: x in LSeg(f,k);
LSeg(f,k) in lf by A2,A3;
hence thesis by A24,TARSKI:def 4;
end;
end;
hence thesis;
end;
theorem
1 < k & len f = k+1 & f is unfolded s.n.c. implies L~(f|k) /\ LSeg(f,k
) = {f/.k}
proof
assume that
A1: 1n+1;
then LSeg(f,n) misses LSeg(f,m) by A1;
then
A2: LSeg(f,n) /\ LSeg(f,m) = {};
now
A3: m <= m+1 by NAT_1:11;
A4: n <= n+1 by NAT_1:11;
now
per cases;
suppose
A5: n in dom f1;
now
per cases;
suppose
n+1 in dom f1;
then
A6: LSeg(f,n)=LSeg(f1,n) by A5,TOPREAL3:17;
now
per cases;
suppose
A7: m in dom f1;
now
per cases;
suppose
m+1 in dom f1;
hence LSeg(f1,n) /\ LSeg(f1,m) = {} by A2,A6,A7,
TOPREAL3:17;
end;
suppose
not m+1 in dom f1;
then not(1 <= m+1 & m+1<= len f1) by FINSEQ_3:25;
then LSeg(f1,m)={} by NAT_1:11,TOPREAL1:def 3;
hence LSeg(f1,n) /\ LSeg(f1,m) = {};
end;
end;
hence thesis;
end;
suppose
not m in dom f1;
then not(1 <= m & m <= len f1) by FINSEQ_3:25;
then not(1 <= m & m+1 <= len f1) by A3,XXREAL_0:2;
then LSeg(f1,m)={} by TOPREAL1:def 3;
hence thesis;
end;
end;
hence thesis;
end;
suppose
not n+1 in dom f1;
then not(1 <= n+1 & n+1<= len f1) by FINSEQ_3:25;
then LSeg(f1,n)={} by NAT_1:11,TOPREAL1:def 3;
hence thesis;
end;
end;
hence thesis;
end;
suppose
not n in dom f1;
then not(1 <= n & n <= len f1) by FINSEQ_3:25;
then not(1 <= n & n+1 <= len f1) by A4,XXREAL_0:2;
then LSeg(f1,n)={} by TOPREAL1:def 3;
hence thesis;
end;
end;
hence thesis;
end;
hence thesis;
end;
theorem
f1 is special & f2 is special & ((f1/.len f1)`1=(f2/.1)`1 or (f1/.len
f1)`2=(f2/.1)`2) implies f1^f2 is special
proof
assume that
A1: f1 is special and
A2: f2 is special and
A3: (f1/.len f1)`1=(f2/.1)`1 or (f1/.len f1)`2=(f2/.1)`2;
let n be Nat;
set f = f1^f2;
assume that
A4: 1 <= n and
A5: n+1 <= len f;
reconsider n as Element of NAT by ORDINAL1:def 12;
set p =f/.n, q =f/.(n+1);
A6: len f=len f1+len f2 by FINSEQ_1:22;
per cases;
suppose
A7: n+1 <= len f1;
then n+1 in dom f1 by A4,SEQ_4:134;
then
A8: f1/.(n+1)=q by FINSEQ_4:68;
n in dom f1 by A4,A7,SEQ_4:134;
then f1/.n=p by FINSEQ_4:68;
hence thesis by A1,A4,A7,A8;
end;
suppose
len f1 < n+1;
then
A9: len f1<=n by NAT_1:13;
then reconsider n1=n-len f1 as Element of NAT by INT_1:5;
now
per cases;
suppose
A10: n=len f1;
then n in dom f1 by A4,FINSEQ_3:25;
then
A11: p=f1/.n by FINSEQ_4:68;
len f2 >= 1 by A5,A6,A10,XREAL_1:6;
hence p`1=q`1 or p`2=q`2 by A3,A10,A11,SEQ_4:136;
end;
suppose
n<>len f1;
then len f1= n1 by NAT_1:11;
then n = n1 + len f1 & n1 <= len f2 by A14,XXREAL_0:2;
then f2/.n1=p by A12,SEQ_4:136;
hence p`1=q`1 or p`2=q`2 by A2,A12,A14,A15;
end;
end;
hence thesis;
end;
end;
theorem Th9:
f <> {} implies X_axis(f) <> {}
proof
A1: len X_axis(f) = len f by GOBOARD1:def 1;
assume f <> {} & X_axis(f) = {};
hence contradiction by A1;
end;
theorem Th10:
f <> {} implies Y_axis(f) <> {}
proof
A1: len Y_axis(f) = len f by GOBOARD1:def 2;
assume f <> {} & Y_axis(f) = {};
hence contradiction by A1;
end;
registration
let f be non empty FinSequence of TOP-REAL 2;
cluster X_axis f -> non empty;
coherence by Th9;
cluster Y_axis f -> non empty;
coherence by Th10;
end;
theorem Th11:
f is special implies
for n being Nat st n in dom f & n+1 in dom f
for i,j,m,k being Nat
st [i,j] in Indices G & [m,k] in Indices G & f/.n=G*(i,j) & f/.(n+1
)=G*(m,k) holds i=m or k=j
proof
assume
A1: f is special;
let n be Nat;
assume n in dom f & n+1 in dom f;
then
A2: 1 <= n & n +1 <= len f by FINSEQ_3:25;
let i,j,m,k be Nat such that
A3: [i,j] in Indices G and
A4: [m,k] in Indices G and
A5: f/.n=G*(i,j) & f/.(n+1)=G*(m,k);
reconsider cj = Col(G,j), lm = Line(G,m) as FinSequence of TOP-REAL 2;
set xj = X_axis(cj), yj = Y_axis(cj), xm = X_axis(lm), ym = Y_axis(lm);
len cj=len G by MATRIX_0:def 8;
then
A6: dom cj = dom G by FINSEQ_3:29;
assume that
A7: i<>m and
A8: k<>j;
A9: len xm=len lm & dom xm=Seg len xm by FINSEQ_1:def 3,GOBOARD1:def 1;
A10: len xj=len cj by GOBOARD1:def 1;
then
A11: dom xj = dom cj by FINSEQ_3:29;
A12: Indices G = [:dom G,Seg width G:] by MATRIX_0:def 4;
then
A13: i in dom G by A3,ZFMISC_1:87;
then cj/.i = cj.i by A6,PARTFUN1:def 6;
then
A14: G*(i,j)=cj/.i by A13,MATRIX_0:def 8;
then
A15: xj.i=G*(i,j)`1 by A13,A6,A11,GOBOARD1:def 1;
A16: m in dom G by A4,A12,ZFMISC_1:87;
then cj/.m = cj.m by A6,PARTFUN1:def 6;
then
A17: G*(m,j)=cj/.m by A16,MATRIX_0:def 8;
then
A18: xj.m=G*(m,j)`1 by A16,A6,A11,GOBOARD1:def 1;
A19: ym is increasing by A16,GOBOARD1:def 6;
A20: xm is constant by A16,GOBOARD1:def 4;
A21: dom yj=Seg len yj by FINSEQ_1:def 3;
A22: dom xj=Seg len xj & len yj=len cj by FINSEQ_1:def 3,GOBOARD1:def 2;
then
A23: yj.m=G*(m,j)`2 by A16,A10,A21,A6,A11,A17,GOBOARD1:def 2;
A24: j in Seg width G by A3,A12,ZFMISC_1:87;
then
A25: xj is increasing by GOBOARD1:def 7;
A26: len lm=width G by MATRIX_0:def 7;
then
A27: dom lm = Seg width G by FINSEQ_1:def 3;
then lm/.j = lm.j by A24,PARTFUN1:def 6;
then
A28: G*(m,j)=lm/.j by A24,MATRIX_0:def 7;
then
A29: xm.j=G*(m,j)`1 by A24,A26,A9,GOBOARD1:def 1;
A30: k in Seg width G by A4,A12,ZFMISC_1:87;
then lm/.k = lm.k by A27,PARTFUN1:def 6;
then
A31: G*(m,k)=lm/.k by A30,MATRIX_0:def 7;
then
A32: xm.k=G*(m,k)`1 by A30,A26,A9,GOBOARD1:def 1;
A33: yj is constant by A24,GOBOARD1:def 5;
A34: len ym=len lm & dom ym=Seg len ym by FINSEQ_1:def 3,GOBOARD1:def 2;
then
A35: ym.j=G*(m,j)`2 by A24,A26,A28,GOBOARD1:def 2;
A36: ym.k=G*(m,k)`2 by A30,A26,A34,A31,GOBOARD1:def 2;
A37: yj.i=G*(i,j)`2 by A13,A10,A22,A21,A6,A11,A14,GOBOARD1:def 2;
now
per cases by A1,A5,A2;
suppose
A38: G*(i,j)`1=G*(m,k)`1;
now
per cases by A7,XXREAL_0:1;
suppose
i>m;
then G*(m,j)`1G*(i,j)`1 by A13,A16,A6,A11,A25,A15,A18,SEQM_3:def 1;
hence contradiction by A24,A30,A26,A9,A20,A29,A32,A38,SEQM_3:def 10;
end;
end;
hence contradiction;
end;
suppose
A39: G*(i,j)`2=G*(m,k)`2;
now
per cases by A8,XXREAL_0:1;
suppose
k>j;
then G*(m,j)`2G*(m,k)`2 by A24,A30,A26,A34,A19,A35,A36,SEQM_3:def 1;
hence contradiction by A13,A16,A10,A22,A21,A6,A11,A33,A37,A23,A39,
SEQM_3:def 10;
end;
end;
hence contradiction;
end;
end;
hence contradiction;
end;
theorem
(for n being Nat st n in dom f
ex i,j being Nat st [i,j] in Indices G & f/.n=G*(i,j)) & f
is special &
(for n being Nat st n in dom f & n+1 in dom f holds f/.n <> f/.(n+1))
implies ex g st g is_sequence_on G & L~f = L~g & g/.1=f/.1 & g/.len g=f/.len f
& len f<=len g
proof
defpred P[Nat] means for f st len f=$1 &
(for n being Nat st n in dom f
ex i,j being Nat st [i,j] in Indices G & f/.n=G*(i,j)) & f is special &
(for n being Nat st n in dom f & n+1 in dom f holds f/.n <> f/.(n+1))
ex g st g is_sequence_on G & L~f = L~g &
g/.1=f/.1 & g/.len g=f/.len f & len f<=len g;
A1: for k being Nat st P[k] holds P[k+1]
proof
let k be Nat such that
A2: P[k];
let f such that
A3: len f=k+1 and
A4: for n being Nat st n in dom f
ex i,j being Nat st [i,j] in Indices G & f/.n=G*(i,j)
and
A5: f is special and
A6: for n being Nat st n in dom f & n+1 in dom f holds f/.n <> f/.(n+1);
A7: dom f = Seg len f by FINSEQ_1:def 3;
now
per cases;
suppose
A8: k=0;
take g=f;
A9: dom f = {1} by A3,A8,FINSEQ_1:2,def 3;
now
let n be Nat;
assume that
A10: n in dom g and
A11: n+1 in dom g;
n=1 by A9,A10,TARSKI:def 1;
hence
for i1,i2,j1,j2 be Nat st [i1,i2] in Indices G & [j1
,j2] in Indices G & g/.n=G*(i1,i2) & g/.(n+1)=G*(j1,j2)
holds |.i1-j1.|+|.i2-j2.|=1 by A9,A11,TARSKI:def 1;
end;
hence g is_sequence_on G by A4;
thus L~f=L~g & g/.1=f/.1 & g/.len g=f/.len f & len f<=len g;
end;
suppose
A12: k<>0;
then
A13: 0+1<=k by NAT_1:13;
then
A14: k in Seg k by FINSEQ_1:1;
A15: 1 in Seg k by A13,FINSEQ_1:1;
A16: k<=k+1 by NAT_1:11;
then
A17: k in dom f by A3,A7,A13,FINSEQ_1:1;
then consider i1,i2 be Nat such that
A18: [i1,i2] in Indices G and
A19: f/.k=G*(i1,i2) by A4;
reconsider l1 = Line(G,i1), c1 = Col(G,i2) as FinSequence of TOP-REAL
2;
set x1 = X_axis(l1), y1 = Y_axis(l1), x2 = X_axis(c1), y2 = Y_axis(c1);
A20: dom y1=Seg len y1 & len y1=len l1 by FINSEQ_1:def 3,GOBOARD1:def 2;
len y2=len c1 by GOBOARD1:def 2;
then
A21: dom y2 = dom c1 by FINSEQ_3:29;
len x2=len c1 by GOBOARD1:def 1;
then
A22: dom x2 = dom c1 by FINSEQ_3:29;
set f1=f|k;
A23: len (f|k)=k by A3,FINSEQ_1:59,NAT_1:11;
A24: dom(f|k)=Seg len(f|k) by FINSEQ_1:def 3;
A25: now
let n be Nat;
assume
A26: n in dom f1;
then n in dom f by A17,A23,A24,FINSEQ_4:71;
then consider i,j being Nat such that
A27: [i,j] in Indices G & f/.n=G*(i,j) by A4;
take i,j;
thus [i,j] in Indices G & f1/.n=G*(i,j) by A17,A23,A24,A26,A27,
FINSEQ_4:71;
end;
A28: f1 is special
proof
let n be Nat;
assume that
A29: 1 <= n and
A30: n+1 <= len f1;
n <= n+1 by NAT_1:11;
then n <= len f1 by A30,XXREAL_0:2;
then n in dom f1 by A29,FINSEQ_3:25;
then
A31: f1/.n=f/.n by A17,A23,A24,FINSEQ_4:71;
1 <= n+1 by NAT_1:11;
then n+1 in dom f1 by A30,FINSEQ_3:25;
then
A32: f1/.(n+1)=f/.(n+1) by A17,A23,A24,FINSEQ_4:71;
n+1 <= len f by A3,A16,A23,A30,XXREAL_0:2;
hence thesis by A5,A29,A31,A32;
end;
now
let n be Nat;
assume
A33: n in dom f1 & n+1 in dom f1;
then
A34: f1/.n=f/.n & f1/.(n+1)=f/.(n+1) by A17,A23,A24,FINSEQ_4:71;
n in dom f & n+1 in dom f by A17,A23,A24,A33,FINSEQ_4:71;
hence f1/.n <> f1/.(n+1) by A6,A34;
end;
then consider g1 such that
A35: g1 is_sequence_on G and
A36: L~g1=L~f1 and
A37: g1/.1=f1/.1 and
A38: g1/.len g1=f1/.len f1 and
A39: len f1<=len g1 by A2,A23,A25,A28;
A40: for n being Nat st n in dom g1
ex m,k being Nat st [m,k] in Indices G & g1/.n=G*(m,k)
by A35;
A41: for n being Nat st n in dom g1 & n+1 in dom g1
for m,k,i,j being Nat st [m,k]
in Indices G & [i,j] in Indices G & g1/.n = G*(m,k) & g1/.(n+1) = G*(i,j) holds
|.m-i.|+|.k-j.| = 1 by A35;
A42: dom x1=Seg len x1 & len x1=len l1 by FINSEQ_1:def 3,GOBOARD1:def 1;
len c1 = len G by MATRIX_0:def 8;
then
A43: dom c1 = dom G by FINSEQ_3:29;
1<=len f by A3,NAT_1:11;
then
A44: k+1 in dom f by A3,FINSEQ_3:25;
then consider j1,j2 be Nat such that
A45: [j1,j2] in Indices G and
A46: f/.(k+1)=G*(j1,j2) by A4;
A47: Indices G = [:dom G,Seg width G:] by MATRIX_0:def 4;
then
A48: j1 in dom G by A45,ZFMISC_1:87;
A49: i1 in dom G by A18,A47,ZFMISC_1:87;
then
A50: x1 is constant by GOBOARD1:def 4;
A51: i2 in Seg width G by A18,A47,ZFMISC_1:87;
then
A52: x2 is increasing by GOBOARD1:def 7;
A53: y2 is constant by A51,GOBOARD1:def 5;
A54: y1 is increasing by A49,GOBOARD1:def 6;
A55: len l1=width G by MATRIX_0:def 7;
A56: j2 in Seg width G by A45,A47,ZFMISC_1:87;
A57: dom g1 = Seg len g1 by FINSEQ_1:def 3;
now
per cases by A5,A17,A18,A19,A44,A45,A46,Th11;
suppose
A58: i1=j1;
set ppi = G*(i1,i2), pj = G*(i1,j2);
now
per cases by XXREAL_0:1;
case
A59: i2>j2;
j2 in dom l1 by A56,A55,FINSEQ_1:def 3;
then l1/.j2 = l1.j2 by PARTFUN1:def 6;
then
A60: l1/.j2=pj by A56,MATRIX_0:def 7;
then
A61: y1.j2=pj`2 by A56,A20,A55,GOBOARD1:def 2;
i2 in dom l1 by A51,A55,FINSEQ_1:def 3;
then l1/.i2 = l1.i2 by PARTFUN1:def 6;
then
A62: l1/.i2=ppi by A51,MATRIX_0:def 7;
then
A63: y1.i2=ppi`2 by A51,A20,A55,GOBOARD1:def 2;
then
A64: pj`2len g1;
A102: w + len g1 = j;
then
A103: w <= len g2 by A93,A96,XREAL_1:6;
A104: j - len g1 <> 0 by A101;
then
A105: w >= 1 by NAT_1:14;
then
A106: w in dom g2 by A103,FINSEQ_3:25;
then reconsider u=i2-w as Element of NAT by A68,A74;
A107: g/.j=g2/.w by A105,A102,A103,SEQ_4:136;
A108: x1.i2=ppi`1 by A51,A42,A55,A62,GOBOARD1:def 1;
A109: uj2;
i2-len g2<=u by A103,XREAL_1:13;
then j2__ len g1;
reconsider q1=g/.i, q2=g/.(i+1) as Point of TOP-REAL 2;
A125: i<=len g by A120,NAT_1:13;
A126: len g1<=i by A124,NAT_1:13;
then
A127: q1 `1=ppi`1 by A94,A125;
A128: q1`2<=ppi`2 by A94,A126,A125;
A129: pj`2<=q1`2 by A94,A126,A125;
q2`1=ppi`1 by A94,A120,A124;
then
A130: q2=|[q1 `1,q2`2]| by A127,EUCLID:53;
A131: q2`2<=ppi`2 by A94,A120,A124;
A132: q1=|[q1`1,q1`2]| & LSeg(g,i)=LSeg(q2,q1) by A119,A120,
EUCLID:53,TOPREAL1:def 3;
A133: pj`2<= q2`2 by A94,A120,A124;
now
per cases by XXREAL_0:1;
suppose
q1`2>q2`2;
then LSeg(g,i)={p2: p2`1=q1`1 & q2`2<=p2`2 & p2`2
<=q1`2} by A130,A132,TOPREAL3:9;
then consider p2 such that
A134: p2 =x & p2`1=q1`1 and
A135: q2`2<=p2`2 & p2`2<=q1`2 by A116,A118;
pj`2<=p2`2 & p2`2<=ppi`2 by A128,A133,A135,
XXREAL_0:2;
then
A136: x in LSeg(f,k) by A92,A127,A134;
LSeg(f,k) in lf by A3,A13;
hence thesis by A136,TARSKI:def 4;
end;
suppose
q1`2=q2`2;
then LSeg(g,i)={q1} by A130,A132,RLTOPSP1:70;
then x=q1 by A116,A118,TARSKI:def 1;
then
A137: x in LSeg(f,k) by A92,A127,A129,A128;
LSeg(f,k) in lf by A3,A13;
hence thesis by A137,TARSKI:def 4;
end;
suppose
q1`2=p1`2;
A147: now
reconsider n=len g1 as Nat;
take n;
thus P2[n]
proof
thus len g1<=n & n<=len g by A93,XREAL_1:31;
1<=len g1 by A13,A23,A39,XXREAL_0:2;
then
A148: len g1 in dom g1 by FINSEQ_3:25;
let q;
assume q=g/.n;
then q=f1/.len f1 by A38,A148,FINSEQ_4:68
.=G*(i1,i2) by A17,A23,A14,A19,FINSEQ_4:71;
hence thesis by A146;
end;
end;
A149: for n be Nat holds P2[n] implies n<=len g;
consider ma be Nat such that
A150: P2[ma] & for n be Nat st P2[n] holds n<=ma
from NAT_1:sch 6(A149,A147);
reconsider ma as Element of NAT by ORDINAL1:def 12;
now
per cases;
suppose
A151: ma=len g;
j2+1<=i2 by A59,NAT_1:13;
then
A152: 1<=l by XREAL_1:19;
then 0+1<=ma by A73,A93,A151,XREAL_1:7;
then reconsider m1=ma-1 as Element of NAT by INT_1:5;
A153: m1 + 1 = ma;
len g1+1<=ma by A73,A93,A151,A152,XREAL_1:7;
then
A154: m1 >= len g1 by A153,XREAL_1:6;
reconsider q=g/.m1 as Point of TOP-REAL 2;
set lq={e where e is Point of TOP-REAL 2: e`1=ppi`1
& pj`2<=e`2 & e`2<=q`2};
A155: i2-l=j2;
A156: l in dom g2 by A74,A152,FINSEQ_1:1;
then
A157: g/.ma=g2/.l by A73,A93,A151,FINSEQ_4:69
.= pj by A73,A74,A156,A155;
then p1`2<=pj`2 by A150;
then
A158: p1`2=pj`2 by A145,XXREAL_0:1;
A159: m1 <= len g by A151,A153,NAT_1:11;
then
A160: q`1=ppi`1 by A94,A154;
A161: pj`2<=q`2 by A94,A154,A159;
1<=len g1 by A13,A23,A39,XXREAL_0:2;
then
A162: 1<=m1 by A154,XXREAL_0:2;
then q=|[q`1,q`2]| & LSeg (g,m1)=LSeg(pj,q) by A151
,A157,A153,EUCLID:53,TOPREAL1:def 3;
then LSeg(g,m1)=lq by A66,A91,A160,A161,TOPREAL3:9;
then
A163: p1 in LSeg(g,m1) by A144,A158,A161;
LSeg(g,m1) in lg by A151,A153,A162;
hence thesis by A143,A163,TARSKI:def 4;
end;
suppose
ma<>len g;
then malen g1;
A220: w + len g1 = j;
then
A221: w <= len g2 by A211,A214,XREAL_1:6;
A222: x1 .i2=ppi`1 by A51,A42,A55,A204,GOBOARD1:def 1;
A223: j - len g1 <> 0 by A219;
then
A224: w >= 1 by NAT_1:14;
then
A225: g/.j=g2/.w by A220,A221,SEQ_4:136;
A226: i2____j2;
u<=i2+l by A178,A221,XREAL_1:7;
then u len g1;
reconsider q1=g/.i, q2=g/.(i+1) as Point of TOP-REAL 2;
A243: i<=len g by A238,NAT_1:13;
A244: len g1<=i by A242,NAT_1:13;
then
A245: q1 `1=ppi`1 by A212,A243;
A246: q1`2<=pj`2 by A212,A244,A243;
A247: ppi`2<=q1`2 by A212,A244,A243;
q2`1=ppi`1 by A212,A238,A242;
then
A248: q2=|[q1 `1,q2`2]| by A245,EUCLID:53;
A249: q2`2<=pj`2 by A212,A238,A242;
A250: q1=|[q1`1,q1`2]| & LSeg(g,i)=LSeg(q2,q1) by A237,A238,
EUCLID:53,TOPREAL1:def 3;
A251: ppi`2<= q2`2 by A212,A238,A242;
now
per cases by XXREAL_0:1;
suppose
q1`2>q2`2;
then LSeg(g,i)={p2: p2`1=q1`1 & q2`2<=p2`2 & p2`2
<=q1`2} by A248,A250,TOPREAL3:9;
then consider p2 such that
A252: p2 =x & p2`1=q1`1 and
A253: q2`2<=p2`2 & p2`2<=q1`2 by A234,A236;
ppi`2<=p2`2 & p2`2<=pj`2 by A246,A251,A253,
XXREAL_0:2;
then
A254: x in LSeg(f,k) by A209,A245,A252;
LSeg(f,k) in lf by A3,A13;
hence thesis by A254,TARSKI:def 4;
end;
suppose
q1`2=q2`2;
then LSeg(g,i)={q1} by A248,A250,RLTOPSP1:70;
then x=q1 by A234,A236,TARSKI:def 1;
then
A255: x in LSeg(f,k) by A209,A245,A247,A246;
LSeg(f,k) in lf by A3,A13;
hence thesis by A255,TARSKI:def 4;
end;
suppose
q1`2= len g1 by A271,XREAL_1:6;
reconsider q=g/.m1 as Point of TOP-REAL 2;
set lq={e where e is Point of TOP-REAL 2: e`1=ppi`1
& q`2<=e`2 & e`2<=pj`2};
A273: i2+l=j2;
A274: l in dom g2 by A178,A270,FINSEQ_3:25;
then
A275: g/.ma=g2/.l by A178,A211,A269,FINSEQ_4:69
.= pj by A178,A274,A273;
then pj`2<=p1`2 by A268;
then
A276: p1`2=pj`2 by A264,XXREAL_0:1;
A277: m1 <= len g by A269,A271,NAT_1:11;
then
A278: q`1=ppi`1 by A212,A272;
A279: q`2<=pj`2 by A212,A272,A277;
1<=len g1 by A13,A23,A39,XXREAL_0:2;
then
A280: 1<=m1 by A272,XXREAL_0:2;
then q=|[q`1,q`2]| & LSeg (g,m1)=LSeg(pj,q) by A269
,A275,A271,EUCLID:53,TOPREAL1:def 3;
then LSeg(g,m1)=lq by A208,A201,A278,A279,TOPREAL3:9;
then
A281: p1 in LSeg(g,m1) by A262,A276,A279;
LSeg(g,m1) in lg by A269,A271,A280;
hence thesis by A261,A281,TARSKI:def 4;
end;
suppose
ma<>len g;
then maj1;
c1/.j1 = c1.j1 by A48,A43,PARTFUN1:def 6;
then
A296: c1/.j1=pj by A48,MATRIX_0:def 8;
then
A297: x2.j1=pj`1 by A48,A43,A22,GOBOARD1:def 1;
c1/.i1 = c1.i1 by A49,A43,PARTFUN1:def 6;
then
A298: c1/.i1=ppi by A49,MATRIX_0:def 8;
then
A299: x2.i1=ppi`1 by A49,A43,A22,GOBOARD1:def 1;
then
A300: pj `1len g1;
A337: w + len g1 = j;
then
A338: w <= len g2 by A329,A332,XREAL_1:6;
A339: j - len g1 <> 0 by A336;
then
A340: w >= 1 by NAT_1:14;
then
A341: w in dom g2 by A338,FINSEQ_3:25;
then reconsider u=i1-w as Element of NAT by A304,A310;
A342: g/.j=g2/.w by A340,A337,A338,SEQ_4:136;
A343: uj1;
i1-len g2<=u by A338,XREAL_1:13;
then j1____ len g1;
reconsider q1=g/.i, q2=g/.(i+1) as Point of TOP-REAL 2;
A360: i<=len g by A355,NAT_1:13;
A361: len g1<=i by A359,NAT_1:13;
then
A362: q1 `2=ppi`2 by A330,A360;
A363: q1`1<=ppi`1 by A330,A361,A360;
A364: pj`1<=q1`1 by A330,A361,A360;
q2`2=ppi`2 by A330,A355,A359;
then
A365: q2=|[q2 `1,q1`2]| by A362,EUCLID:53;
A366: q2`1<=ppi`1 by A330,A355,A359;
A367: q1=|[q1`1,q1`2]| & LSeg(g,i)=LSeg(q2,q1) by A354,A355,
EUCLID:53,TOPREAL1:def 3;
A368: pj`1<= q2`1 by A330,A355,A359;
now
per cases by XXREAL_0:1;
suppose
q1`1>q2`1;
then LSeg(g,i)={p2: p2`2=q1`2 & q2`1<=p2`1 & p2`1
<=q1`1} by A365,A367,TOPREAL3:10;
then consider p2 such that
A369: p2 =x & p2`2=q1`2 and
A370: q2`1<=p2`1 & p2`1<=q1`1 by A351,A353;
pj`1<=p2`1 & p2`1<=ppi`1 by A363,A368,A370,
XXREAL_0:2;
then
A371: x in LSeg(f,k) by A328,A362,A369;
LSeg(f,k) in lf by A3,A13;
hence thesis by A371,TARSKI:def 4;
end;
suppose
q1`1=q2`1;
then LSeg(g,i)={q1} by A365,A367,RLTOPSP1:70;
then x=q1 by A351,A353,TARSKI:def 1;
then
A372: x in LSeg(f,k) by A328,A362,A364,A363;
LSeg(f,k) in lf by A3,A13;
hence thesis by A372,TARSKI:def 4;
end;
suppose
q1`1=p1`1;
A382: now
reconsider n=len g1 as Nat;
take n;
thus P2[n]
proof
thus len g1<=n & n<=len g by A329,XREAL_1:31;
1<=len g1 by A13,A23,A39,XXREAL_0:2;
then
A383: len g1 in dom g1 by FINSEQ_3:25;
let q;
assume q=g/.n;
then q=f1/.len f1 by A38,A383,FINSEQ_4:68
.=G*(i1,i2) by A17,A23,A14,A19,FINSEQ_4:71;
hence thesis by A381;
end;
end;
A384: for n be Nat holds P2[n] implies n<=len g;
consider ma be Nat such that
A385: P2 [ma] & for n be Nat st P2[n] holds n<=ma
from NAT_1:sch 6 (A384,A382);
reconsider ma as Element of NAT by ORDINAL1:def 12;
now
per cases;
suppose
A386: ma=len g;
j1+1<=i1 by A295,NAT_1:13;
then
A387: 1<=l by XREAL_1:19;
then 0+1<=ma by A309,A329,A386,XREAL_1:7;
then reconsider m1=ma-1 as Element of NAT by INT_1:5;
A388: m1 + 1 = ma;
len g1+1<=ma by A309,A329,A386,A387,XREAL_1:7;
then
A389: m1 >= len g1 by A388,XREAL_1:6;
reconsider q=g/.m1 as Point of TOP-REAL 2;
set lq={e where e is Point of TOP-REAL 2: e`2=ppi`2
& pj`1<=e`1 & e`1<=q`1};
A390: i1-l=j1;
A391: l in dom g2 by A310,A387,FINSEQ_1:1;
then
A392: g/.ma=g2/.l by A309,A329,A386,FINSEQ_4:69
.= pj by A309,A310,A391,A390;
then p1`1<=pj`1 by A385;
then
A393: p1`1=pj`1 by A380,XXREAL_0:1;
A394: m1 <= len g by A386,A388,NAT_1:11;
then
A395: q`2=ppi`2 by A330,A389;
A396: pj`1<=q`1 by A330,A389,A394;
1<=len g1 by A13,A23,A39,XXREAL_0:2;
then
A397: 1<=m1 by A389,XXREAL_0:2;
then q=|[q`1,q`2]| & LSeg (g,m1)=LSeg(pj,q) by A386
,A392,A388,EUCLID:53,TOPREAL1:def 3;
then LSeg(g,m1)=lq by A302,A327,A395,A396,TOPREAL3:10
;
then
A398: p1 in LSeg(g,m1) by A379,A393,A396;
LSeg(g,m1) in lg by A386,A388,A397;
hence thesis by A378,A398,TARSKI:def 4;
end;
suppose
ma<>len g;
then malen g1;
A454: w + len g1 = j;
then
A455: w <= len g2 by A446,A449,XREAL_1:6;
A456: y2.i1=G*(i1,i2)`2 by A49,A43,A21,A439,GOBOARD1:def 2;
A457: j - len g1 <> 0 by A453;
then
A458: w >= 1 by NAT_1:14;
then
A459: g/.j=g2/.w by A454,A455,SEQ_4:136;
A460: i1____j1;
u<=i1+l by A413,A455,XREAL_1:7;
then u len g1;
reconsider q1=g/.i, q2=g/.(i+1) as Point of TOP-REAL 2;
A477: i<=len g by A472,NAT_1:13;
A478: len g1<=i by A476,NAT_1:13;
then
A479: q1 `2=ppi`2 by A447,A477;
A480: q1`1<=pj`1 by A447,A478,A477;
A481: ppi`1<=q1`1 by A447,A478,A477;
q2`2=ppi`2 by A447,A472,A476;
then
A482: q2=|[q2 `1,q1`2]| by A479,EUCLID:53;
A483: q2`1<=pj`1 by A447,A472,A476;
A484: q1=|[q1`1,q1`2]| & LSeg(g,i)=LSeg(q2,q1) by A471,A472,
EUCLID:53,TOPREAL1:def 3;
A485: ppi`1<= q2`1 by A447,A472,A476;
now
per cases by XXREAL_0:1;
suppose
q1`1>q2`1;
then LSeg(g,i)={p2: p2`2=q1`2 & q2`1<=p2`1 & p2`1
<=q1`1} by A482,A484,TOPREAL3:10;
then consider p2 such that
A486: p2 =x & p2`2=q1`2 and
A487: q2`1<=p2`1 & p2`1<=q1`1 by A468,A470;
ppi`1<=p2`1 & p2`1<=pj`1 by A480,A485,A487,
XXREAL_0:2;
then
A488: x in LSeg(f,k) by A444,A479,A486;
LSeg(f,k) in lf by A3,A13;
hence thesis by A488,TARSKI:def 4;
end;
suppose
q1`1=q2`1;
then LSeg(g,i)={q1} by A482,A484,RLTOPSP1:70;
then x=q1 by A468,A470,TARSKI:def 1;
then
A489: x in LSeg(f,k) by A444,A479,A481,A480;
LSeg(f,k) in lf by A3,A13;
hence thesis by A489,TARSKI:def 4;
end;
suppose
q1`1= len g1 by A505,XREAL_1:6;
reconsider q=g/.m1 as Point of TOP-REAL 2;
set lq={e where e is Point of TOP-REAL 2: e`2=ppi`2
& q`1<=e`1 & e`1<=pj`1};
A507: i1+l=j1;
A508: l in dom g2 by A413,A504,FINSEQ_3:25;
then
A509: g/.ma=g2/.l by A413,A446,A503,FINSEQ_4:69
.= pj by A413,A508,A507;
then pj`1<=p1`1 by A502;
then
A510: p1`1=pj`1 by A498,XXREAL_0:1;
A511: m1 <= len g by A503,A505,NAT_1:11;
then
A512: q`2=ppi`2 by A447,A506;
A513: q`1<=pj`1 by A447,A506,A511;
1<=len g1 by A13,A23,A39,XXREAL_0:2;
then
A514: 1<=m1 by A506,XXREAL_0:2;
then q=|[q`1,q`2]| & LSeg(g,m1)=LSeg(pj,q) by A503
,A509,A505,EUCLID:53,TOPREAL1:def 3;
then LSeg(g,m1)=lq by A443,A436,A512,A513,TOPREAL3:10
;
then
A515: p1 in LSeg(g,m1) by A496,A510,A513;
LSeg(g,m1) in lg by A503,A505,A514;
hence thesis by A495,A515,TARSKI:def 4;
end;
suppose
ma<>len g;
then ma f/.(n+1);
take g=f;
f={} by A529;
then
for n being Nat holds n in dom g & n+1 in dom g implies
for m,k,i,j being Nat st [m,k] in
Indices G & [i,j] in Indices G & g/.n=G*(m,k) & g/.(n+1)=G*(i,j) holds |.m-i.|
+|.k-j.|=1;
hence thesis by A530;
end;
for n being Nat holds P[n] from NAT_1:sch 2(A528,A1);
hence thesis;
end;
definition
let v1,v2 be FinSequence of REAL;
assume
A1: v1 <> {};
func GoB(v1,v2) -> Matrix of TOP-REAL 2 means
:Def1:
len it = len v1 & width
it = len v2 &
for n,m being Nat st [n,m] in Indices it holds it*(n,m) = |[v1.n,v2.m]|;
existence
proof
defpred P[Nat,Nat,Point of TOP-REAL 2] means [$1,$2] in [:dom v1,dom v2:]
& for r,s st v1.$1=r & v2.$2=s holds $3=|[r,s]|;
A2: dom v1 = Seg len v1 by FINSEQ_1:def 3;
A3: for i,j being Nat st [i,j] in [:Seg len v1,Seg len v2:] ex p st P[i,j, p]
proof
let i,j be Nat;
assume
A4: [i,j] in [:Seg len v1,Seg len v2:];
reconsider i9=i, j9=j as Element of NAT by ORDINAL1:def 12;
reconsider s1=v1.i9, s2=v2.j9 as Real;
take |[s1,s2]|;
thus [i,j] in [:dom v1,dom v2:] by A2,A4,FINSEQ_1:def 3;
let r,s;
assume r=v1.i & s=v2.j;
hence thesis;
end;
consider M be Matrix of len v1,len v2,the carrier of TOP-REAL 2 such that
A5: for i,j being Nat st [i,j] in Indices M holds P[i,j,M*(i,j)] from
MATRIX_0:sch 2(A3);
reconsider M as Matrix of the carrier of TOP-REAL 2;
take M;
thus len M=len v1 & width M=len v2 by A1,MATRIX_0:23;
let n,m be Nat;
assume [n,m] in Indices M;
hence thesis by A5;
end;
uniqueness
proof
let G1,G2 be Matrix of TOP-REAL 2;
assume that
A6: len G1 = len v1 & width G1 = len v2 and
A7: for n,m being Nat st [n,m] in Indices G1 holds G1*(n,m) = |[v1.n,v2.m]| and
A8: len G2 = len v1 & width G2 = len v2 and
A9: for n,m being Nat st [n,m] in Indices G2 holds G2*(n,m) = |[v1.n,v2.m]|;
A10: Indices G1 = [:dom G1,Seg width G1:] & Indices G2 = [:dom G2,Seg
width G2:] by MATRIX_0:def 4;
now
let n,m be Nat;
reconsider m9=m, n9=n as Element of NAT by ORDINAL1:def 12;
A11: dom G1 = Seg len G1 & dom G2 = Seg len G2 by FINSEQ_1:def 3;
reconsider r=v1.n9, s=v2.m9 as Real;
assume
A12: [n,m] in Indices G1;
then G1*(n,m)=|[r,s]| by A7;
hence G1*(n,m)=G2*(n,m) by A6,A8,A9,A10,A12,A11;
end;
hence thesis by A6,A8,MATRIX_0:21;
end;
end;
registration
let v1,v2 be non empty FinSequence of REAL;
cluster GoB(v1,v2) -> non empty-yielding X_equal-in-line Y_equal-in-column;
coherence
proof
set M = GoB(v1,v2);
A1: len M=len v1 by Def1;
then
A2: dom M = dom v1 by FINSEQ_3:29;
A3: width M=len v2 by Def1;
hence M is non empty-yielding by A1,MATRIX_0:def 10;
A4: Indices M=[:dom v1,Seg len v2:] by A3,A2,MATRIX_0:def 4;
thus M is X_equal-in-line
proof
let n be Nat;
reconsider l = Line(M,n) as FinSequence of TOP-REAL 2;
set x = X_axis(l);
assume
A5: n in dom M;
A6: len l = width M & dom x = Seg len x by FINSEQ_1:def 3,MATRIX_0:def 7;
A7: len x = len l by GOBOARD1:def 1;
then
A8: dom x = dom l by FINSEQ_3:29;
now
let i,j be Nat;
assume that
A9: i in dom x and
A10: j in dom x;
reconsider r=v1.n, s1=v2.i, s2=v2.j as Real;
[n,i] in Indices M by A3,A2,A4,A5,A7,A6,A9,ZFMISC_1:87;
then M*(n,i)=|[r,s1]| by Def1;
then
A11: M*(n,i)`1 = r by EUCLID:52;
l/.i = l.i by A8,A9,PARTFUN1:def 6;
then l/.i=M*(n,i) by A7,A6,A9,MATRIX_0:def 7;
then
A12: x.i=r by A9,A11,GOBOARD1:def 1;
[n,j] in Indices M by A3,A2,A4,A5,A7,A6,A10,ZFMISC_1:87;
then M*(n,j)=|[r,s2]| by Def1;
then
A13: M*(n,j)`1 = r by EUCLID:52;
l/.j = l.j by A8,A10,PARTFUN1:def 6;
then l/.j=M*(n,j) by A7,A6,A10,MATRIX_0:def 7;
hence x.i=x.j by A10,A13,A12,GOBOARD1:def 1;
end;
hence thesis by SEQM_3:def 10;
end;
thus M is Y_equal-in-column
proof
let n be Nat;
reconsider c = Col(M,n) as FinSequence of TOP-REAL 2;
set y = Y_axis(c);
len y = len c by GOBOARD1:def 2;
then
A14: dom y = dom c by FINSEQ_3:29;
len c = len M by MATRIX_0:def 8;
then
A15: dom c = dom M by FINSEQ_3:29;
assume
A16: n in Seg width M;
now
let i,j be Nat;
assume that
A17: i in dom y and
A18: j in dom y;
reconsider r=v2.n, s1=v1.i, s2=v1.j as Real;
[i,n] in Indices M by A3,A2,A4,A16,A14,A15,A17,ZFMISC_1:87;
then M*(i,n)=|[s1,r]| by Def1;
then
A19: M*(i,n)`2 = r by EUCLID:52;
c/.i = c.i by A14,A17,PARTFUN1:def 6;
then c/.i=M*(i,n) by A14,A15,A17,MATRIX_0:def 8;
then
A20: y.i=r by A17,A19,GOBOARD1:def 2;
[j,n] in Indices M by A3,A2,A4,A16,A14,A15,A18,ZFMISC_1:87;
then M*(j,n)=|[s2,r]| by Def1;
then
A21: M*(j,n)`2 = r by EUCLID:52;
c/.j = c.j by A14,A18,PARTFUN1:def 6;
then c/.j=M*(j,n) by A14,A15,A18,MATRIX_0:def 8;
hence y.i=y.j by A18,A21,A20,GOBOARD1:def 2;
end;
hence thesis by SEQM_3:def 10;
end;
end;
end;
registration
let v1,v2 be non empty increasing FinSequence of REAL;
cluster GoB(v1,v2) -> Y_increasing-in-line X_increasing-in-column;
coherence
proof
set M = GoB(v1,v2);
A1: width M=len v2 by Def1;
A2: len M=len v1 by Def1;
then
A3: dom M = dom v1 by FINSEQ_3:29;
then
A4: Indices M=[:dom v1,Seg len v2:] by A1,MATRIX_0:def 4;
A5: dom v2=Seg len v2 by FINSEQ_1:def 3;
thus M is Y_increasing-in-line
proof
let n be Nat;
reconsider l = Line(M,n) as FinSequence of TOP-REAL 2;
set y = Y_axis(l);
assume
A6: n in dom M;
A7: len l = width M & dom y = Seg len y by FINSEQ_1:def 3,MATRIX_0:def 7;
A8: len y = len l by GOBOARD1:def 2;
then
A9: dom y = dom l by FINSEQ_3:29;
now
let i,j be Nat;
assume that
A10: i in dom y and
A11: j in dom y and
A12: i Matrix of TOP-REAL 2 equals
GoB(Incr(X_axis(f)),Incr(Y_axis(f)));
correctness;
end;
registration
let f be non empty FinSequence of TOP-REAL 2;
cluster GoB(f) -> non empty-yielding X_equal-in-line Y_equal-in-column
Y_increasing-in-line X_increasing-in-column;
coherence;
end;
reserve f for non empty FinSequence of TOP-REAL 2;
theorem Th13:
len GoB(f) = card rng X_axis(f) & width GoB(f) = card rng Y_axis (f)
proof
set x = X_axis(f), y = Y_axis(f);
len Incr(x)=card rng x & len Incr(y)=card rng y by SEQ_4:def 21;
hence thesis by Def1;
end;
theorem
for n st n in dom f holds ex i,j st [i,j] in Indices GoB(f) & f/.n =
GoB(f)*(i,j)
proof
set x = X_axis(f), y = Y_axis(f);
let n such that
A1: n in dom f;
A2: rng Incr(y) = rng y by SEQ_4:def 21;
reconsider p=f/.n as Point of TOP-REAL 2;
A3: dom f = Seg len f by FINSEQ_1:def 3;
dom y = Seg len y & len y = len f by FINSEQ_1:def 3,GOBOARD1:def 2;
then y.n=p`2 & y.n in rng y by A1,A3,FUNCT_1:def 3,GOBOARD1:def 2;
then consider j being Nat such that
A4: j in dom Incr(y) and
A5: Incr(y).j=p`2 by A2,FINSEQ_2:10;
A6: rng Incr(x) = rng x by SEQ_4:def 21;
dom x = Seg len x & len x = len f by FINSEQ_1:def 3,GOBOARD1:def 1;
then x.n=p`1 & x.n in rng x by A1,A3,FUNCT_1:def 3,GOBOARD1:def 1;
then consider i being Nat such that
A7: i in dom Incr(x) and
A8: Incr(x).i=p`1 by A6,FINSEQ_2:10;
width GoB(f)=card rng y & len Incr(y) = card rng y by Th13,SEQ_4:def 21;
then
A9: Seg width GoB(f) = dom Incr(y) by FINSEQ_1:def 3;
reconsider i,j as Element of NAT by ORDINAL1:def 12;
take i,j;
len GoB(f)=card rng x & len Incr(x) = card rng x by Th13,SEQ_4:def 21;
then Indices GoB(f) = [:dom GoB(f), Seg width GoB(f):] & dom GoB(f) = dom
Incr(x) by FINSEQ_3:29,MATRIX_0:def 4;
hence [i,j] in Indices GoB(f) by A7,A4,A9,ZFMISC_1:87;
then GoB(f)*(i,j) = |[p`1,p`2]| by A8,A5,Def1;
hence thesis by EUCLID:53;
end;
theorem
n in dom f & (for m st m in dom f holds (X_axis(f)).n <= (X_axis(f)).m
) implies f/.n in rng Line(GoB(f),1)
proof
set x = X_axis(f), y = Y_axis(f), r = x.n;
assume that
A1: n in dom f and
A2: for m st m in dom f holds r <= x.m;
reconsider p=f/.n as Point of TOP-REAL 2;
A3: dom f = Seg len f by FINSEQ_1:def 3;
A4: dom x = Seg len x & len x = len f by FINSEQ_1:def 3,GOBOARD1:def 1;
then
A5: x.n=p`1 by A1,A3,GOBOARD1:def 1;
A6: rng Incr(x) = rng x by SEQ_4:def 21;
x.n in rng x by A1,A3,A4,FUNCT_1:def 3;
then consider i being Nat such that
A7: i in dom Incr(x) and
A8: Incr(x).i=p`1 by A5,A6,FINSEQ_2:10;
reconsider i as Element of NAT by ORDINAL1:def 12;
A9: 1<=i by A7,FINSEQ_3:25;
then reconsider i1=i-1 as Element of NAT by INT_1:5;
A10: i<=len Incr(x) by A7,FINSEQ_3:25;
A11: now
reconsider s=Incr(x).i1 as Real;
assume i <> 1;
then 1__* len Incr(x);
then i 1;
then 1 len Incr(y);
then j*