Copyright (c) 2001 Association of Mizar Users
environ
vocabulary COMPTS_1, SPPOL_1, EUCLID, FINSEQ_1, GOBOARD1, PRE_TOPC, BOOLE,
ARYTM_3, RELAT_1, RELAT_2, TRIANG_1, ZF_REFLE, AMI_1, PRALG_1, FUNCT_1,
FUNCT_6, ORDINAL2, TOPREAL1, JORDAN1, PCOMPS_1, METRIC_1, SQUARE_1,
ARYTM_1, FINSEQ_2, COMPLEX1, ABSVALUE, ORDERS_1, ORDERS_2, FINSET_1,
FINSEQ_4, GOBOARD2, CARD_1, FUNCT_5, MCART_1, GOBRD13, TARSKI, PROB_1,
MATRIX_1, TREES_1, INCSP_1, GOBOARD5, SEQM_3, CONNSP_1, SUBSET_1,
GOBOARD9, TOPS_1, JORDAN3, RFINSEQ, FINSEQ_5, JORDAN8, INT_1, GROUP_1,
PSCOMP_1, JORDAN2C, FINSEQ_6, SPRECT_2, JORDAN9, JORDAN1A, JORDAN1H,
ARYTM, PARTFUN1;
notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, FINSEQ_6, RVSUM_1, GOBOARD5,
STRUCT_0, ORDINAL1, NUMBERS, XCMPLX_0, XREAL_0, REAL_1, SQUARE_1, NAT_1,
INT_1, BINARITH, ABSVALUE, RELAT_1, RELAT_2, RELSET_1, FUNCT_1, PARTFUN1,
FUNCT_2, CARD_1, CARD_4, FINSET_1, FINSEQ_1, FUNCT_6, PROB_1, PRALG_1,
FINSEQ_2, FINSEQ_4, FINSEQ_5, RFINSEQ, MATRIX_1, METRIC_1, ORDERS_1,
ORDERS_2, TRIANG_1, PRE_TOPC, TOPS_1, COMPTS_1, CONNSP_1, PCOMPS_1,
EUCLID, JORDAN1, SPRECT_2, TOPREAL1, GOBOARD1, GOBOARD2, JORDAN3,
JORDAN2C, SPPOL_1, PSCOMP_1, GOBOARD9, JORDAN8, GOBRD13, JORDAN9,
JORDAN1A;
constructors REAL_1, CARD_4, RFINSEQ, BINARITH, TOPS_1, CONNSP_1, PSCOMP_1,
GOBOARD9, JORDAN8, GOBRD13, GROUP_1, JORDAN9, GOBOARD2, TRIANG_1,
ORDERS_2, AMI_1, JORDAN1, PRALG_1, MATRLIN, JORDAN3, JORDAN2C, SQUARE_1,
WSIERP_1, JORDAN1A, TOPREAL4, SPRECT_1, PROB_1;
clusters PSCOMP_1, RELSET_1, FINSEQ_1, FINSEQ_5, REVROT_1, XREAL_0, GOBOARD9,
JORDAN8, GOBRD13, EUCLID, FINSET_1, POLYNOM1, WAYBEL_2, GOBOARD1,
PRELAMB, TRIANG_1, PUA2MSS1, MSAFREE1, FUNCT_7, PRALG_1, GENEALG1,
GOBOARD2, SPRECT_3, TOPREAL6, INT_1, BORSUK_2, SPRECT_4, SPRECT_1,
MEMBERED, RELAT_1;
requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
definitions GOBOARD1, TARSKI, RELSET_1, RELAT_2, ORDERS_2, FUNCT_1, JORDAN1,
RELAT_1, XBOOLE_0;
theorems JORDAN9, GOBOARD5, TOPREAL1, GOBOARD7, AXIOMS, GOBOARD1, SPRECT_2,
GOBOARD2, FINSEQ_4, TRIANG_1, ORDERS_2, CARD_2, PRE_CIRC, CARD_1,
FINSEQ_3, FUNCT_2, GOBRD13, PSCOMP_1, FINSEQ_1, FUNCT_1, MATRIX_1,
RELAT_1, RLVECT_1, EUCLID, NAT_1, SUBSET_1, GOBRD11, JORDAN1D, ZFMISC_1,
RELSET_1, FUNCT_7, TARSKI, UNIALG_1, PROB_1, EXTENS_1, FUNCT_6, JORDAN3,
JORDAN4, JORDAN8, TOPREAL3, GOBRD14, GOBOARD9, SPRECT_4, GOBRD12,
SPPOL_2, REAL_1, PRE_TOPC, AMI_5, TOPS_1, SPRECT_3, JORDAN1A, TSEP_1,
INT_1, REAL_2, HEINE, NEWTON, JORDAN5B, JORDAN2C, JORDAN1, TOPMETR,
SUB_METR, SQUARE_1, RVSUM_1, ABSVALUE, METRIC_1, JORDAN1B, CQC_THE1,
BINARITH, SCMFSA_7, POLYNOM4, SPRECT_1, FINSEQ_2, JORDAN10, SPPOL_1,
CONNSP_1, REVROT_1, PCOMPS_2, XBOOLE_0, XBOOLE_1, XREAL_0, PARTIT_2,
XCMPLX_0, XCMPLX_1, PARTFUN1, RELAT_2;
schemes FINSEQ_1, FINSEQ_2, NAT_1;
begin :: Preliminaries
reserve m,k,j,j1,i,i1,i2,n for Nat,
r,s for Real,
C for compact non vertical non horizontal Subset of TOP-REAL 2,
G for Go-board,
p for Point of TOP-REAL 2;
definition
cluster with_non-empty_element set;
existence
proof consider X being with_non-empty_element set;
take X; thus thesis;
end;
end;
definition let D be non empty with_non-empty_element set;
cluster non empty non-empty FinSequence of D*;
existence
proof
consider X being non empty set such that
A1: X in D by TRIANG_1:def 1;
A2: rng<*<*X*>*> = {<*X*>} by FINSEQ_1:56;
<*X*> in D* by A1,FUNCT_7:20;
then rng<*<*X*>*> c= D* by A2,ZFMISC_1:37;
then reconsider F = <*<*X*>*> as FinSequence of D* by FINSEQ_1:def 4;
take F;
thus F is non empty;
assume {} in rng F;
hence thesis by A2,TARSKI:def 1;
end;
end;
definition let D be non empty with_non-empty_elements set;
cluster non empty non-empty FinSequence of D*;
existence
proof consider X being Element of D;
A1: rng<*<*X*>*> = {<*X*>} by FINSEQ_1:56;
<*X*> in D* by FUNCT_7:20;
then rng<*<*X*>*> c= D* by A1,ZFMISC_1:37;
then reconsider F = <*<*X*>*> as FinSequence of D* by FINSEQ_1:def 4;
take F;
thus F is non empty;
assume {} in rng F;
hence thesis by A1,TARSKI:def 1;
end;
end;
definition let F be non-empty Function-yielding Function;
cluster rngs F -> non-empty;
coherence
proof
now let n be set;
assume n in dom rngs F;
then A1: n in dom F by EXTENS_1:4;
then A2: (rngs F).n = rng(F.n) by FUNCT_6:31;
F.n is non empty by A1,UNIALG_1:def 6;
hence (rngs F).n is non empty by A2,RELAT_1:64;
end;
hence thesis by UNIALG_1:def 6;
end;
end;
definition
cluster increasing -> one-to-one FinSequence of REAL;
coherence
proof let f be FinSequence of REAL such that
A1: f is increasing;
let x1,x2 be set;
assume
A2: x1 in dom f & x2 in dom f;
then reconsider n1=x1, n2=x2 as Nat;
assume
A3: f.x1 = f.x2;
assume
A4: not thesis;
per cases by A4,AXIOMS:21;
suppose n1 < n2;
hence contradiction by A1,A2,A3,GOBOARD1:def 1;
suppose n1 > n2;
hence contradiction by A1,A2,A3,GOBOARD1:def 1;
end;
end;
canceled 3;
theorem Th4:
for p,q being Point of TOP-REAL 2
holds LSeg(p,q) \ {p,q} is convex
proof let p,q,w1,w2 be Point of TOP-REAL 2;
set P = LSeg(p,q) \ {p,q};
assume
A1: w1 in P & w2 in P;
then w1 in LSeg(p,q) & w2 in LSeg(p,q) by XBOOLE_0:def 4;
then A2: LSeg(w1,w2) c= LSeg(p,q) by TOPREAL1:12;
not w1 in {p,q} & not w2 in {p,q} by A1,XBOOLE_0:def 4;
then w1 <> p & w2 <> p & w1 <> q & w2 <> q by TARSKI:def 2;
then not p in LSeg(w1,w2) & not q in LSeg(w1,w2) by A2,SPPOL_1:24;
then LSeg(w1,w2) misses {p,q} by ZFMISC_1:57;
hence LSeg(w1,w2) c= P by A2,XBOOLE_1:86;
end;
theorem
for p,q being Point of TOP-REAL 2
holds LSeg(p,q) \ {p,q} is connected
proof let p,q be Point of TOP-REAL 2;
LSeg(p,q) \ {p,q} is convex by Th4;
hence thesis by JORDAN1:9;
end;
theorem Th6:
for p,q being Point of TOP-REAL 2 st p <> q
holds p in Cl(LSeg(p,q) \ {p,q})
proof let p,q be Point of TOP-REAL 2 such that
A1: p <> q;
for G being Subset of TOP-REAL 2 st G is open
holds p in G implies (LSeg(p,q) \ {p,q}) meets G
proof let G be Subset of TOP-REAL 2 such that
A2: G is open and
A3: p in G;
reconsider P = G as Subset of TopSpaceMetr Euclid 2 by EUCLID:def 8;
reconsider x = p, y = q as Point of Euclid 2 by TOPREAL3:13;
TOP-REAL 2 = TopSpaceMetr Euclid 2 by EUCLID:def 8;
then consider r being real number such that
A4: r>0 and
A5: Ball(x,r) c= P by A2,A3,TOPMETR:22;
reconsider r as Real by XREAL_0:def 1;
set t = min(r/2,dist(x,y)/2),
s = t/dist(x,y);
A6: r/2 > 0 by A4,REAL_2:127;
A7: 0 < dist(x,y) by A1,SUB_METR:2;
then 0 < dist(x,y)/2 by REAL_2:127;
then A8: 0 < t by A6,SPPOL_1:13;
then A9: 0 < s by A7,REAL_2:127;
A10: t <= dist(x,y)/2 by SQUARE_1:35;
dist(x,y)/2 < dist(x,y)/1 by A7,REAL_2:200;
then t < dist(x,y) by A10,AXIOMS:22;
then A11: s < 1 by A8,REAL_2:142;
set pp = (1-s)*p+s*q;
reconsider z = pp as Point of Euclid 2 by TOPREAL3:13;
A12: pp in LSeg(p,q) by A9,A11,SPPOL_1:22;
A13: (1-s)*p+s*p = (1-s+s)*p by EUCLID:37
.= 1 * p by XCMPLX_1:27
.= p by EUCLID:33;
A14: now assume pp = p;
then s*p = pp - (1-s)*p by A13,EUCLID:52
.= s*q by EUCLID:52;
hence contradiction by A1,A9,EUCLID:38;
end;
A15: (1-s)*q+s*q = (1-s+s)*q by EUCLID:37
.= 1 *q by XCMPLX_1:27
.= q by EUCLID:33;
A16: 1-s <> 0 by A11,XCMPLX_1:15;
now assume pp = q;
then (1-s)*q = pp - s*q by A15,EUCLID:52
.= (1-s)*p by EUCLID:52;
hence contradiction by A1,A16,EUCLID:38;
end;
then not pp in {p,q} by A14,TARSKI:def 2;
then A17: pp in LSeg(p,q) \ {p,q} by A12,XBOOLE_0:def 4;
reconsider x' = x, y' = y, z' = z as Element of REAL 2 by EUCLID:25;
reconsider a = x', b = y' as Element of 2-tuples_on REAL by EUCLID:def 1;
reconsider u = a-b, v = s*b, w = (1-s)*a as Element of REAL 2
by EUCLID:def 1;
A18: (1-s)*p = (1-s)*x' by EUCLID:def 11;
s*q = s*y' by EUCLID:def 11;
then A19: (1-s)*p+s*q = w+v by A18,EUCLID:def 10;
dist(x,z) = |.x'-z'.| by SPPOL_1:20
.= |.a-(1-s)*a-s*b.| by A19,RVSUM_1:60
.= |.1 *a-(1-s)*a-s*b.| by RVSUM_1:74
.= |.1 *a +-(1-s)*a-s*b.| by RVSUM_1:52
.= |.1 *a +(-1)*((1-s)*a)-s*b.| by RVSUM_1:76
.= |.1 *a +(-1)*(1-s)*a-s*b.| by RVSUM_1:71
.= |.1 *a + (-(1-s))*a-s*b.| by XCMPLX_1:180
.= |.(1+ (-(1-s)))*a-s*b.| by RVSUM_1:72
.= |.(1-(1-s))*a-s*b.| by XCMPLX_0:def 8
.= |.s*a-s*b.| by XCMPLX_1:18
.= |.s*a+ -s*b.| by RVSUM_1:52
.= |.s*a+ (-1)*(s*b).| by RVSUM_1:76
.= |.s*a+ (-1)*s*b.| by RVSUM_1:71
.= |.s*a+ s*((-1)*b).| by RVSUM_1:71
.= |.s*(a+ (-1)*b).| by RVSUM_1:73
.= |.s*(a+ -b).| by RVSUM_1:76
.= |.s*(a-b).| by RVSUM_1:52
.= abs(s)*|.u.| by EUCLID:14
.= s*|.a-b.| by A9,ABSVALUE:def 1
.= s*dist(x,y) by SPPOL_1:20
.= t by A7,XCMPLX_1:88;
then A20: dist(x,z) <= r/2 by SQUARE_1:35;
r/2 < r/1 by A4,REAL_2:200;
then dist(x,z) < r by A20,AXIOMS:22;
then z in Ball(x,r) by METRIC_1:12;
hence (LSeg(p,q) \ {p,q}) meets G by A5,A17,XBOOLE_0:3;
end;
hence p in Cl(LSeg(p,q) \ {p,q}) by TOPS_1:39;
end;
theorem Th7:
for p,q being Point of TOP-REAL 2 st p <> q
holds Cl(LSeg(p,q) \ {p,q}) = LSeg(p,q)
proof let p,q be Point of TOP-REAL 2 such that
A1: p <> q;
LSeg(p,q) \ {p,q} c= LSeg(p,q) by XBOOLE_1:36;
then Cl(LSeg(p,q) \ {p,q}) c= Cl LSeg(p,q) by PRE_TOPC:49;
hence Cl(LSeg(p,q) \ {p,q}) c= LSeg(p,q) by PRE_TOPC:52;
let e be set;
assume
A2: e in LSeg(p,q);
p in LSeg(p,q) & q in LSeg(p,q) by TOPREAL1:6;
then {p,q} c= LSeg(p,q) by ZFMISC_1:38;
then LSeg(p,q) = LSeg(p,q) \ {p,q} \/ {p,q} by XBOOLE_1:45;
then A3: e in LSeg(p,q) \ {p,q} or e in {p,q} by A2,XBOOLE_0:def 2;
per cases by A3,TARSKI:def 2;
suppose
A4: e in LSeg(p,q) \ {p,q};
LSeg(p,q) \ {p,q} c= Cl(LSeg(p,q) \ {p,q}) by PRE_TOPC:48;
hence e in Cl(LSeg(p,q) \ {p,q}) by A4;
suppose e = p or e = q;
hence thesis by A1,Th6;
end;
theorem
for S being Subset of TOP-REAL 2,
p,q be Point of TOP-REAL 2
st p <> q & LSeg(p,q) \ {p,q} c= S
holds LSeg(p,q) c= Cl S
proof
let S be Subset of TOP-REAL 2,
p,q be Point of TOP-REAL 2 such that
A1: p <> q;
assume LSeg(p,q) \ {p,q} c= S;
then Cl(LSeg(p,q) \ {p,q}) c= Cl S by PRE_TOPC:49;
hence thesis by A1,Th7;
end;
begin :: Transforming Finite Sets to Finite Sequences
definition
func RealOrd -> Relation of REAL equals
:Def1: {[r,s] : r <= s };
coherence
proof set R = {[r,s] : r <= s };
let x be set;
assume x in R;
then ex r,s st x = [r,s] & r <= s;
hence x in [:REAL,REAL:] by ZFMISC_1:106;
end;
end;
theorem Th9:
[r,s] in RealOrd implies r <= s
proof
hereby assume [r,s] in RealOrd;
then consider r1,s1 being Real such that
A1: [r,s] = [r1,s1] and
A2: r1 <= s1 by Def1;
r = r1 & s = s1 by A1,ZFMISC_1:33;
hence r <= s by A2;
end;
end;
Lm1: RealOrd is_reflexive_in REAL
proof let x be set such that
A1: x in REAL;
reconsider x as Element of REAL by A1;
x <= x;
hence thesis by Def1;
end;
Lm2: RealOrd is_antisymmetric_in REAL
proof let x,y be set such that
A1: x in REAL & y in REAL and
A2: [x,y] in RealOrd & [y,x] in RealOrd;
reconsider x,y as Element of REAL by A1;
x <= y & y <= x by A2,Th9;
hence thesis by AXIOMS:21;
end;
Lm3: RealOrd is_transitive_in REAL
proof let x,y,z be set such that
A1: x in REAL & y in REAL & z in REAL and
A2: [x,y] in RealOrd & [y,z] in RealOrd;
reconsider x,y,z as Element of REAL by A1;
x <= y & y <= z by A2,Th9;
then x <= z by AXIOMS:22;
hence thesis by Def1;
end;
Lm4: RealOrd is_connected_in REAL
proof
let x,y be set;
assume x in REAL & y in REAL;
then reconsider x,y as Element of REAL;
x <= y or y <= x;
hence thesis by Def1;
end;
theorem Th10:
field RealOrd = REAL
proof
field RealOrd c= REAL \/ REAL by RELSET_1:19;
hence field RealOrd c= REAL;
thus REAL c= field RealOrd by Lm1,PARTIT_2:8;
end;
definition
cluster RealOrd
-> total reflexive antisymmetric transitive being_linear-order;
coherence
proof
A1: REAL c= dom RealOrd
proof let x be set such that
A2: x in REAL;
reconsider x as Element of REAL by A2;
[x,x] in RealOrd by Def1;
hence thesis by RELAT_1:def 4;
end;
dom RealOrd = REAL by A1,XBOOLE_0:def 10;
hence RealOrd is total by PARTFUN1:def 4;
RealOrd is_reflexive_in REAL by Lm1;
hence RealOrd is reflexive by Th10,RELAT_2:def 9;
RealOrd is_antisymmetric_in REAL by Lm2;
hence RealOrd is antisymmetric by Th10,RELAT_2:def 12;
RealOrd is_transitive_in REAL by Lm3;
hence RealOrd is transitive by Th10,RELAT_2:def 16;
thus RealOrd is_reflexive_in field RealOrd by Lm1,Th10;
thus RealOrd is_transitive_in field RealOrd by Lm3,Th10;
thus RealOrd is_antisymmetric_in field RealOrd by Lm2,Th10;
thus RealOrd is_connected_in field RealOrd by Lm4,Th10;
end;
end;
theorem Th11:
RealOrd linearly_orders REAL
proof
thus RealOrd is_reflexive_in REAL by Lm1;
thus RealOrd is_transitive_in REAL by Lm3;
thus RealOrd is_antisymmetric_in REAL by Lm2;
thus RealOrd is_connected_in REAL by Lm4;
end;
theorem Th12:
for A being finite Subset of REAL
holds SgmX(RealOrd,A) is increasing
proof let A be finite Subset of REAL;
set IT = SgmX(RealOrd,A);
let n,m be Nat such that
A1: n in dom IT and
A2: m in dom IT and
A3: n<m;
A4: RealOrd linearly_orders A by Th11,ORDERS_2:36;
then IT is one-to-one by TRIANG_1:8;
then A5: IT.n <> IT.m by A1,A2,A3,FUNCT_1:def 8;
IT/.n = IT.n & IT/.m = IT.m by A1,A2,FINSEQ_4:def 4;
then [IT.n,IT.m] in RealOrd by A1,A2,A3,A4,TRIANG_1:def 2;
then IT.n <= IT.m by Th9;
hence IT.n < IT.m by A5,AXIOMS:21;
end;
theorem Th13:
for f being FinSequence of REAL,
A being finite Subset of REAL st A = rng f
holds SgmX(RealOrd,A) = Incr f
proof let f be FinSequence of REAL, A be finite Subset of REAL such that
A1: A = rng f;
A2: RealOrd linearly_orders A by Th11,ORDERS_2:36;
then A3: rng SgmX(RealOrd,A) = rng f by A1,TRIANG_1:def 2;
reconsider F = SgmX(RealOrd,A) as increasing FinSequence of REAL by Th12;
len F = card rng f by A1,A2,TRIANG_1:9;
hence thesis by A3,GOBOARD2:def 2;
end;
definition let A be finite Subset of REAL;
cluster SgmX(RealOrd,A) -> increasing;
coherence by Th12;
end;
canceled;
theorem Th15:
for X being non empty set,
A being finite Subset of X,
R be being_linear-order Order of X
holds len SgmX(R,A) = card A
proof
let X being non empty set, A being finite Subset of X,
R be being_linear-order Order of X;
A1: field R = X by ORDERS_2:2;
R linearly_orders field R by ORDERS_2:35;
then R linearly_orders A by A1,ORDERS_2:36;
hence thesis by TRIANG_1:9;
end;
begin :: On the construction of go boards
theorem Th16:
for f being FinSequence of TOP-REAL 2
holds X_axis f = proj1*f
proof let f be FinSequence of TOP-REAL 2;
reconsider pf = proj1*f as FinSequence of REAL by FINSEQ_2:36;
A1: len pf = len f by FINSEQ_2:37;
A2: len X_axis f = len f by GOBOARD1:def 3;
then A3: dom X_axis f = dom f by FINSEQ_3:31;
A4: dom X_axis f = dom pf by A1,A2,FINSEQ_3:31;
for k being Nat st k in dom X_axis f holds (X_axis f).k = pf.k
proof let k be Nat such that
A5: k in dom X_axis f;
A6: f/.k = f.k by A3,A5,FINSEQ_4:def 4;
thus (X_axis f).k = (f/.k)`1 by A5,GOBOARD1:def 3
.= proj1.(f.k) by A6,PSCOMP_1:def 28
.= pf.k by A3,A5,FUNCT_1:23;
end;
hence X_axis f = proj1*f by A4,FINSEQ_1:17;
end;
theorem Th17:
for f being FinSequence of TOP-REAL 2
holds Y_axis f = proj2*f
proof let f be FinSequence of TOP-REAL 2;
reconsider pf = proj2*f as FinSequence of REAL by FINSEQ_2:36;
A1: len pf = len f by FINSEQ_2:37;
A2: len Y_axis f = len f by GOBOARD1:def 4;
then A3: dom Y_axis f = dom f by FINSEQ_3:31;
A4: dom Y_axis f = dom pf by A1,A2,FINSEQ_3:31;
for k being Nat st k in dom Y_axis f holds (Y_axis f).k = pf.k
proof let k be Nat such that
A5: k in dom Y_axis f;
A6: f/.k = f.k by A3,A5,FINSEQ_4:def 4;
thus (Y_axis f).k = (f/.k)`2 by A5,GOBOARD1:def 4
.= proj2.(f.k) by A6,PSCOMP_1:def 29
.= pf.k by A3,A5,FUNCT_1:23;
end;
hence Y_axis f = proj2*f by A4,FINSEQ_1:17;
end;
definition let D be non empty set; let M be FinSequence of D*;
redefine func Values M -> Subset of D;
coherence
proof set A = {rng f where f is Element of D*: f in rng M};
for X being set st X in A holds X c= D
proof let X be set;
assume X in A;
then ex f being Element of D* st X = rng f & f in rng M;
hence thesis by FINSEQ_1:def 4;
end;
then union A c= D by ZFMISC_1:94;
hence Values M is Subset of D by GOBRD13:3;
end;
end;
definition let D be non empty with_non-empty_elements set;
let M be non empty non-empty FinSequence of D*;
cluster Values M -> non empty;
coherence
proof
dom rngs M = dom M by EXTENS_1:4;
then reconsider X = rng rngs M as non empty with_non-empty_elements set
by RELAT_1:65;
Values M = Union rngs M by GOBRD13:def 1
.= union X by PROB_1:def 3;
hence thesis;
end;
end;
theorem Th18:
for D being non empty set, M being (Matrix of D), i st i in Seg width M
holds rng Col(M,i) c= Values M
proof let D be non empty set;
let M be (Matrix of D), k such that
A1: k in Seg width M;
A2: Values M = { M*(i,j): [i,j] in Indices M } by GOBRD13:7;
let e be set;
assume e in rng Col(M,k);
then consider u being set such that
A3: u in dom Col(M,k) and
A4: e = Col(M,k).u by FUNCT_1:def 5;
reconsider u as Nat by A3;
A5: len Col(M,k) = len M by MATRIX_1:def 9;
then dom Col(M,k) = dom M by FINSEQ_3:31;
then A6: Col(M,k).u = M*(u,k) by A3,MATRIX_1:def 9;
A7: 1 <= u & u <= len M by A3,A5,FINSEQ_3:27;
1 <= k & k <= width M by A1,FINSEQ_1:3;
then [u,k] in Indices M by A7,GOBOARD7:10;
hence e in Values M by A2,A4,A6;
end;
theorem Th19:
for D being non empty set, M being (Matrix of D), i st i in dom M
holds rng Line(M,i) c= Values M
proof let D be non empty set;
let M be (Matrix of D), k such that
A1: k in dom M;
A2: Values M = { M*(i,j): [i,j] in Indices M } by GOBRD13:7;
let e be set;
assume e in rng Line(M,k);
then consider u being set such that
A3: u in dom Line(M,k) and
A4: e = Line(M,k).u by FUNCT_1:def 5;
reconsider u as Nat by A3;
A5: len Line(M,k) = width M by MATRIX_1:def 8;
then dom Line(M,k) = Seg width M by FINSEQ_1:def 3;
then A6: Line(M,k).u = M*(k,u) by A3,MATRIX_1:def 8;
A7: 1 <= k & k <= len M by A1,FINSEQ_3:27;
1 <= u & u <= width M by A3,A5,FINSEQ_3:27;
then [k,u] in Indices M by A7,GOBOARD7:10;
hence e in Values M by A2,A4,A6;
end;
theorem Th20:
for G being X_increasing-in-column non empty-yielding Matrix of TOP-REAL 2
holds len G <= card(proj1.:Values G)
proof let G be X_increasing-in-column non empty-yielding Matrix of TOP-REAL 2;
0 <> width G by GOBOARD1:def 5;
then 1 <= width G by RLVECT_1:99;
then A1: 1 in Seg width G by FINSEQ_1:3;
then reconsider L = X_axis(Col(G,1)) as increasing FinSequence of REAL
by GOBOARD1:def 9;
A2: rng L = rng(proj1*Col(G,1)) by Th16
.= proj1.:rng Col(G,1) by RELAT_1:160;
A3: card rng L= len L by FINSEQ_4:77
.= len Col(G,1) by GOBOARD1:def 3
.= len G by MATRIX_1:def 9;
rng Col(G,1) c= Values G by A1,Th18;
then proj1.:rng Col(G,1) c= proj1.:Values G by RELAT_1:156;
hence len G <= card(proj1.:Values G) by A2,A3,CARD_1:80;
end;
theorem Th21:
for G being X_equal-in-line Matrix of TOP-REAL 2
holds card(proj1.:Values G) <= len G
proof let G be X_equal-in-line Matrix of TOP-REAL 2;
deffunc F(Nat)=proj1.(G*($1,1));
consider f being FinSequence such that
A1: len f = len G and
A2: for k st k in Seg len G holds f.k = F(k) from SeqLambda;
A3: dom f = dom G by A1,FINSEQ_3:31;
proj1.:Values G c= rng f
proof let y be set;
assume y in proj1.:Values G;
then consider x being set such that
A4: x in the carrier of TOP-REAL 2 and
A5: x in Values G and
A6: y = proj1.x by FUNCT_2:115;
Values G = { G*(i,j): [i,j] in Indices G } by GOBRD13:7;
then consider i,j such that
A7: x = G*(i,j) and
A8: [i,j] in Indices G by A5;
A9: 1 <= i & i <= len G by A8,GOBOARD5:1;
then A10: i in dom G by FINSEQ_3:27;
then A11: i in Seg len G by FINSEQ_1:def 3;
reconsider x as Point of TOP-REAL 2 by A4;
A12: 1 <= j & j <= width G by A8,GOBOARD5:1;
y = x`1 by A6,PSCOMP_1:def 28
.= G*(i,1)`1 by A7,A9,A12,GOBOARD5:3
.= proj1.(G*(i,1)) by PSCOMP_1:def 28
.= f.i by A2,A11;
hence thesis by A3,A10,FUNCT_1:12;
end;
then Card(proj1.:Values G) c= Card dom G by A3,CARD_1:28;
then card(proj1.:Values G) <= card dom G by CARD_2:57;
hence card(proj1.:Values G) <= len G by PRE_CIRC:21;
end;
theorem Th22:
for G being X_equal-in-line X_increasing-in-column
non empty-yielding Matrix of TOP-REAL 2
holds len G = card(proj1.:Values G)
proof
let G be X_equal-in-line X_increasing-in-column
non empty-yielding Matrix of TOP-REAL 2;
A1: len G <= card(proj1.:Values G) by Th20;
card(proj1.:Values G) <= len G by Th21;
hence len G = card(proj1.:Values G) by A1,AXIOMS:21;
end;
theorem Th23:
for G being Y_increasing-in-line non empty-yielding Matrix of TOP-REAL 2
holds width G <= card(proj2.:Values G)
proof let G be Y_increasing-in-line non empty-yielding Matrix of TOP-REAL 2;
0 <> len G by GOBOARD1:def 5;
then 1 <= len G by RLVECT_1:99;
then A1: 1 in dom G by FINSEQ_3:27;
then reconsider L = Y_axis(Line(G,1)) as increasing FinSequence of REAL
by GOBOARD1:def 8;
A2: rng L = rng(proj2*Line(G,1)) by Th17
.= proj2.:rng Line(G,1) by RELAT_1:160;
A3: card rng L= len L by FINSEQ_4:77
.= len Line(G,1) by GOBOARD1:def 4
.= width G by MATRIX_1:def 8;
rng Line(G,1) c= Values G by A1,Th19;
then proj2.:rng Line(G,1) c= proj2.:Values G by RELAT_1:156;
hence width G <= card(proj2.:Values G) by A2,A3,CARD_1:80;
end;
theorem Th24:
for G being Y_equal-in-column non empty-yielding Matrix of TOP-REAL 2
holds card(proj2.:Values G) <= width G
proof let G be Y_equal-in-column non empty-yielding Matrix of TOP-REAL 2;
deffunc F(Nat)=proj2.(G*(1,$1));
consider f being FinSequence such that
A1: len f = width G and
A2: for k st k in Seg width G holds f.k = F(k) from SeqLambda;
A3: dom f = Seg width G by A1,FINSEQ_1:def 3;
proj2.:Values G c= rng f
proof let y be set;
assume y in proj2.:Values G;
then consider x being set such that
A4: x in the carrier of TOP-REAL 2 and
A5: x in Values G and
A6: y = proj2.x by FUNCT_2:115;
Values G = { G*(i,j): [i,j] in Indices G } by GOBRD13:7;
then consider i,j such that
A7: x = G*(i,j) and
A8: [i,j] in Indices G by A5;
A9: 1 <= j & j <= width G by A8,GOBOARD5:1;
then A10: j in Seg width G by FINSEQ_1:3;
reconsider x as Point of TOP-REAL 2 by A4;
A11: 1 <= i & i <= len G by A8,GOBOARD5:1;
y = x`2 by A6,PSCOMP_1:def 29
.= G*(1,j)`2 by A7,A9,A11,GOBOARD5:2
.= proj2.(G*(1,j)) by PSCOMP_1:def 29
.= f.j by A2,A10;
hence thesis by A3,A10,FUNCT_1:12;
end;
then Card(proj2.:Values G) c= Card Seg width G by A3,CARD_1:28;
then card(proj2.:Values G) <= card Seg width G by CARD_2:57;
hence card(proj2.:Values G) <= width G by FINSEQ_1:78;
end;
theorem Th25:
for G being Y_equal-in-column Y_increasing-in-line non empty-yielding
Matrix of TOP-REAL 2
holds width G = card(proj2.:Values G)
proof
let G be Y_equal-in-column Y_increasing-in-line non empty-yielding
Matrix of TOP-REAL 2;
A1: width G <= card(proj2.:Values G) by Th23;
card(proj2.:Values G) <= width G by Th24;
hence width G = card(proj2.:Values G) by A1,AXIOMS:21;
end;
begin :: On go boards
theorem
for G be Go-board
for f be FinSequence of TOP-REAL 2 st f is_sequence_on G
for k be Nat st 1 <= k & k+1 <= len f holds
LSeg(f,k) c= left_cell(f,k,G)
proof
let G be Go-board;
let f be FinSequence of TOP-REAL 2;
assume A1: f is_sequence_on G;
let k be Nat;
assume that
A2: 1 <= k and
A3: k+1 <= len f;
A4: k in dom f & k+1 in dom f by A2,A3,GOBOARD2:3;
then consider i1,j1 be Nat such that
A5: [i1,j1] in Indices G and
A6: f/.k = G*(i1,j1) by A1,GOBOARD1:def 11;
consider i2,j2 be Nat such that
A7: [i2,j2] in Indices G and
A8: f/.(k+1) = G*(i2,j2) by A1,A4,GOBOARD1:def 11;
A9: j1+1+1 = j1+(1+1) by XCMPLX_1:1;
A10: i1+1+1 = i1+(1+1) by XCMPLX_1:1;
A11: 1 <= i1 & i1 <= len G by A5,GOBOARD5:1;
A12: 1 <= j1 & j1 <= width G by A5,GOBOARD5:1;
A13: 1 <= i2 & i2 <= len G by A7,GOBOARD5:1;
A14: 1 <= j2 & j2 <= width G by A7,GOBOARD5:1;
left_cell(f,k,G) = left_cell(f,k,G);
then A15: i1 = i2 & j1+1 = j2 & left_cell(f,k,G) = cell(G,i1-'1,j1) or
i1+1 = i2 & j1 = j2 & left_cell(f,k,G) = cell(G,i1,j1) or
i1 = i2+1 & j1 = j2 & left_cell(f,k,G) = cell(G,i2,j2-'1) or
i1 = i2 & j1 = j2+1 & left_cell(f,k,G) = cell(G,i1,j2)
by A1,A2,A3,A5,A6,A7,A8,GOBRD13:def 3;
abs(i1-i2)+abs(j1-j2) = 1 by A1,A4,A5,A6,A7,A8,GOBOARD1:def 11;
then A16: abs(i1-i2)=1 & j1=j2 or abs(j1-j2)=1 & i1=i2 by GOBOARD1:2;
per cases by A16,GOBOARD1:1;
suppose A17: i1 = i2 & j1+1 = j2;
A18: i1 -' 1 + 1 = i1 by A11,AMI_5:4;
then A19: i1-'1 < len G by A11,NAT_1:38;
j1 < width G by A14,A17,NAT_1:38;
then LSeg(f/.k,f/.(k+1)) c= cell(G,i1-'1,j1)
by A6,A8,A12,A17,A18,A19,GOBOARD5:19;
hence LSeg(f,k) c= left_cell(f,k,G) by A2,A3,A9,A15,A17,REAL_1:69,TOPREAL1:
def 5;
suppose A20: i1+1 = i2 & j1 = j2;
then i1 < len G by A13,NAT_1:38;
then LSeg(f/.k,f/.(k+1)) c= cell(G,i1,j1)
by A6,A8,A11,A12,A20,GOBOARD5:23;
hence LSeg(f,k) c= left_cell(f,k,G)
by A2,A3,A10,A15,A20,REAL_1:69,TOPREAL1:
def 5;
suppose A21: i1 = i2+1 & j1 = j2;
A22: j2 -' 1 + 1 = j2 by A14,AMI_5:4;
then A23: j2 -' 1 < width G by A14,NAT_1:38;
i2 < len G by A11,A21,NAT_1:38;
then LSeg(f/.k,f/.(k+1)) c= cell(G,i2,j2-'1)
by A6,A8,A13,A21,A22,A23,GOBOARD5:22;
hence LSeg(f,k) c= left_cell(f,k,G) by A2,A3,A10,A15,A21,REAL_1:69,TOPREAL1
:def 5;
suppose A24: i1 = i2 & j1 = j2+1;
then j2 < width G by A12,NAT_1:38;
then LSeg(f/.k,f/.(k+1)) c= left_cell(f,k,G) by A6,A8,A9,A11,A14,A15,A24,
GOBOARD5:20,REAL_1:69;
hence LSeg(f,k) c= left_cell(f,k,G) by A2,A3,TOPREAL1:def 5;
end;
theorem
for f being standard special_circular_sequence st 1 <= k & k+1 <= len f
holds left_cell(f,k,GoB f) = left_cell(f,k)
proof let f be standard special_circular_sequence such that
A1: 1 <= k and
A2: k+1 <= len f;
set G = GoB f;
A3: f is_sequence_on GoB f by GOBOARD5:def 5;
for i1,j1,i2,j2 being Nat
st [i1,j1] in Indices G & [i2,j2] in Indices G &
f/.k = G*(i1,j1) & f/.(k+1) = G*(i2,j2)
holds
i1 = i2 & j1+1 = j2 & left_cell(f,k) = cell(GoB f,i1-'1,j1) or
i1+1 = i2 & j1 = j2 & left_cell(f,k) = cell(GoB f,i1,j1) or
i1 = i2+1 & j1 = j2 & left_cell(f,k) = cell(GoB f,i2,j2-'1) or
i1 = i2 & j1 = j2+1 & left_cell(f,k) = cell(GoB f,i1,j2)
proof let i1,j1,i2,j2 be Nat such that
A4: [i1,j1] in Indices G and
A5: [i2,j2] in Indices G and
A6: f/.k = G*(i1,j1) and
A7: f/.(k+1) = G*(i2,j2);
left_cell(f,k) = left_cell(f,k);
then A8: i1 = i2 & j1+1 = j2 & left_cell(f,k) = cell(GoB f,i1-'1,j1) or
i1+1 = i2 & j1 = j2 & left_cell(f,k) = cell(GoB f,i1,j1) or
i1 = i2+1 & j1 = j2 & left_cell(f,k) = cell(GoB f,i2,j2-'1) or
i1 = i2 & j1 = j2+1 & left_cell(f,k) = cell(GoB f,i1,j2)
by A1,A2,A4,A5,A6,A7,GOBOARD5:def 7;
A9: j1+1+1 = j1+(1+1) by XCMPLX_1:1;
A10: i1+1+1 = i1+(1+1) by XCMPLX_1:1;
k < len f by A2,NAT_1:38;
then A11: k in dom f by A1,FINSEQ_3:27;
1 <= k+1 by NAT_1:29;
then k+1 in dom f by A2,FINSEQ_3:27;
then abs(i1-i2)+abs(j1-j2) = 1 by A3,A4,A5,A6,A7,A11,GOBOARD1:def 11;
then A12: abs(i1-i2)=1 & j1=j2 or abs(j1-j2)=1 & i1=i2 by GOBOARD1:2;
per cases by A12,GOBOARD1:1;
case i1 = i2 & j1+1 = j2;
hence left_cell(f,k) = cell(G,i1-'1,j1) by A8,A9,REAL_1:69;
case i1+1 = i2 & j1 = j2;
hence left_cell(f,k) = cell(G,i1,j1) by A8,A10,REAL_1:69;
case i1 = i2+1 & j1 = j2;
hence left_cell(f,k) = cell(G,i2,j2-'1) by A8,A10,REAL_1:69;
case i1 = i2 & j1 = j2+1;
hence left_cell(f,k) = cell(G,i1,j2) by A8,A9,REAL_1:69;
end;
hence left_cell(f,k,GoB f) = left_cell(f,k) by A1,A2,A3,GOBRD13:def 3;
end;
theorem Th28:
for G be Go-board
for f be FinSequence of TOP-REAL 2 st f is_sequence_on G
for k be Nat st 1 <= k & k+1 <= len f holds
LSeg(f,k) c= right_cell(f,k,G)
proof
let G be Go-board;
let f be FinSequence of TOP-REAL 2;
assume A1: f is_sequence_on G;
let k be Nat;
assume that
A2: 1 <= k and
A3: k+1 <= len f;
A4: k in dom f & k+1 in dom f by A2,A3,GOBOARD2:3;
then consider i1,j1 be Nat such that
A5: [i1,j1] in Indices G and
A6: f/.k = G*(i1,j1) by A1,GOBOARD1:def 11;
consider i2,j2 be Nat such that
A7: [i2,j2] in Indices G and
A8: f/.(k+1) = G*(i2,j2) by A1,A4,GOBOARD1:def 11;
A9: j1+1+1 = j1+(1+1) by XCMPLX_1:1;
A10: i1+1+1 = i1+(1+1) by XCMPLX_1:1;
A11: 1 <= i1 & i1 <= len G by A5,GOBOARD5:1;
A12: 1 <= j1 & j1 <= width G by A5,GOBOARD5:1;
A13: 1 <= i2 & i2 <= len G by A7,GOBOARD5:1;
A14: 1 <= j2 & j2 <= width G by A7,GOBOARD5:1;
right_cell(f,k,G) = right_cell(f,k,G);
then A15: i1 = i2 & j1+1 = j2 & right_cell(f,k,G) = cell(G,i1,j1) or
i1+1 = i2 & j1 = j2 & right_cell(f,k,G) = cell(G,i1,j1-'1) or
i1 = i2+1 & j1 = j2 & right_cell(f,k,G) = cell(G,i2,j2) or
i1 = i2 & j1 = j2+1 & right_cell(f,k,G) = cell(G,i1-'1,j2)
by A1,A2,A3,A5,A6,A7,A8,GOBRD13:def 2;
abs(i1-i2)+abs(j1-j2) = 1 by A1,A4,A5,A6,A7,A8,GOBOARD1:def 11;
then A16: abs(i1-i2)=1 & j1=j2 or abs(j1-j2)=1 & i1=i2 by GOBOARD1:2;
per cases by A16,GOBOARD1:1;
suppose A17: i1 = i2 & j1+1 = j2;
then j1 < width G by A14,NAT_1:38;
then LSeg(f/.k,f/.(k+1)) c= cell(G,i1,j1)
by A6,A8,A11,A12,A17,GOBOARD5:20;
hence LSeg(f,k) c= right_cell(f,k,G) by A2,A3,A9,A15,A17,REAL_1:69,TOPREAL1
:def 5;
suppose A18: i1+1 = i2 & j1 = j2;
A19: j1 -' 1 + 1 = j1 by A12,AMI_5:4;
then A20: j1-'1 < width G by A12,NAT_1:38;
i1 < len G by A13,A18,NAT_1:38;
then LSeg(f/.k,f/.(k+1)) c= cell(G,i1,j1-'1)
by A6,A8,A11,A18,A19,A20,GOBOARD5:22;
hence LSeg(f,k) c= right_cell(f,k,G) by A2,A3,A10,A15,A18,REAL_1:69,
TOPREAL1:def 5;
suppose A21: i1 = i2+1 & j1 = j2;
then i2 < len G by A11,NAT_1:38;
then LSeg(f/.k,f/.(k+1)) c= cell(G,i2,j2)
by A6,A8,A13,A14,A21,GOBOARD5:23;
hence LSeg(f,k) c= right_cell(f,k,G) by A2,A3,A10,A15,A21,REAL_1:69,
TOPREAL1:def 5;
suppose A22: i1 = i2 & j1 = j2+1;
A23: i1 -' 1 + 1 = i1 by A11,AMI_5:4;
then A24: i1-'1 < len G by A11,NAT_1:38;
j2 < width G by A12,A22,NAT_1:38;
then LSeg(f/.k,f/.(k+1)) c= right_cell(f,k,G)
by A6,A8,A9,A14,A15,A22,A23,A24,GOBOARD5:19,
REAL_1:69;
hence LSeg(f,k) c= right_cell(f,k,G) by A2,A3,TOPREAL1:def 5;
end;
theorem Th29:
for f being standard special_circular_sequence st 1 <= k & k+1 <= len f
holds right_cell(f,k,GoB f) = right_cell(f,k)
proof let f be standard special_circular_sequence such that
A1: 1 <= k and
A2: k+1 <= len f;
set G = GoB f;
A3: f is_sequence_on GoB f by GOBOARD5:def 5;
for i1,j1,i2,j2 being Nat
st [i1,j1] in Indices G & [i2,j2] in Indices G &
f/.k = G*(i1,j1) & f/.(k+1) = G*(i2,j2)
holds
i1 = i2 & j1+1 = j2 & right_cell(f,k) = cell(G,i1,j1) or
i1+1 = i2 & j1 = j2 & right_cell(f,k) = cell(G,i1,j1-'1) or
i1 = i2+1 & j1 = j2 & right_cell(f,k) = cell(G,i2,j2) or
i1 = i2 & j1 = j2+1 & right_cell(f,k) = cell(G,i1-'1,j2)
proof let i1,j1,i2,j2 be Nat such that
A4: [i1,j1] in Indices G and
A5: [i2,j2] in Indices G and
A6: f/.k = G*(i1,j1) and
A7: f/.(k+1) = G*(i2,j2);
set IT = right_cell(f,k);
right_cell(f,k) = right_cell(f,k);
then A8: i1 = i2 & j1+1 = j2 & IT = cell(GoB f,i1,j1) or
i1+1 = i2 & j1 = j2 & IT = cell(GoB f,i1,j1-'1) or
i1 = i2+1 & j1 = j2 & IT = cell(GoB f,i2,j2) or
i1 = i2 & j1 = j2+1 & IT = cell(GoB f,i1-'1,j2)
by A1,A2,A4,A5,A6,A7,GOBOARD5:def 6;
A9: j1+1+1 = j1+(1+1) by XCMPLX_1:1;
A10: i1+1+1 = i1+(1+1) by XCMPLX_1:1;
k < len f by A2,NAT_1:38;
then A11: k in dom f by A1,FINSEQ_3:27;
1 <= k+1 by NAT_1:29;
then k+1 in dom f by A2,FINSEQ_3:27;
then abs(i1-i2)+abs(j1-j2) = 1 by A3,A4,A5,A6,A7,A11,GOBOARD1:def 11;
then A12: abs(i1-i2)=1 & j1=j2 or abs(j1-j2)=1 & i1=i2 by GOBOARD1:2;
per cases by A12,GOBOARD1:1;
case i1 = i2 & j1+1 = j2;
hence right_cell(f,k) = cell(G,i1,j1) by A8,A9,REAL_1:69;
case i1+1 = i2 & j1 = j2;
hence right_cell(f,k) = cell(G,i1,j1-'1) by A8,A10,REAL_1:69;
case i1 = i2+1 & j1 = j2;
hence right_cell(f,k) = cell(G,i2,j2) by A8,A10,REAL_1:69;
case i1 = i2 & j1 = j2+1;
hence right_cell(f,k) = cell(G,i1-'1,j2) by A8,A9,REAL_1:69;
end;
hence right_cell(f,k,GoB f) = right_cell(f,k) by A1,A2,A3,GOBRD13:def 2;
end;
theorem
for P being Subset of TOP-REAL 2,
f being non constant standard special_circular_sequence st
P is_a_component_of (L~f)` holds
P = RightComp f or P = LeftComp f
proof let P be Subset of TOP-REAL 2,
f be non constant standard special_circular_sequence;
assume P is_a_component_of (L~f)`;
then ex B1 being Subset of (TOP-REAL 2)|(L~f)`
st B1 = P & B1 is_a_component_of (TOP-REAL 2)|(L~f)` by CONNSP_1:def 6;
hence P = RightComp f or P = LeftComp f by GOBRD14:22;
end;
theorem
for f being non constant standard special_circular_sequence st
f is_sequence_on G
for k st 1 <= k & k+1 <= len f
holds
Int right_cell(f,k,G) c= RightComp f & Int left_cell(f,k,G) c= LeftComp f
proof let f be non constant standard special_circular_sequence such that
A1: f is_sequence_on G;
let k such that
A2: 1 <= k & k+1 <= len f;
A3: Int right_cell(f,k,G) c= right_cell(f,k,G) by TOPS_1:44;
Int right_cell(f,k,G) misses L~f by A1,A2,JORDAN9:17;
then A4: Int right_cell(f,k,G) c= right_cell(f,k,G)\L~f by A3,XBOOLE_1:86;
right_cell(f,k,G)\L~f c= RightComp f by A1,A2,JORDAN9:29;
hence Int right_cell(f,k,G) c= RightComp f by A4,XBOOLE_1:1;
A5: Int left_cell(f,k,G) c= left_cell(f,k,G) by TOPS_1:44;
Int left_cell(f,k,G) misses L~f by A1,A2,JORDAN9:17;
then A6: Int left_cell(f,k,G) c= left_cell(f,k,G)\L~f by A5,XBOOLE_1:86;
left_cell(f,k,G)\L~f c= LeftComp f by A1,A2,JORDAN9:29;
hence Int left_cell(f,k,G) c= LeftComp f by A6,XBOOLE_1:1;
end;
theorem Th32:
for i1,j1,i2,j2 being Nat, G being Go-board
st [i1,j1] in Indices G & [i2,j2] in Indices G & G*(i1,j1) = G*(i2,j2)
holds i1 = i2 & j1 = j2
proof let i1,j1,i2,j2 be Nat, G be Go-board such that
A1: [i1,j1] in Indices G and
A2: [i2,j2] in Indices G and
A3: G*(i1,j1) = G*(i2,j2);
A4: 1 <= i1 & i1 <= len G by A1,GOBOARD5:1;
A5: 1 <= j1 & j1 <= width G by A1,GOBOARD5:1;
A6: 1 <= i2 & i2 <= len G by A2,GOBOARD5:1;
A7: 1 <= j2 & j2 <= width G by A2,GOBOARD5:1;
then A8: G*(i1,j2)`1 = G*(i1,1)`1 by A4,GOBOARD5:3
.= G*(i1,j1)`1 by A4,A5,GOBOARD5:3;
A9: G*(i1,j2)`2 = G*(1,j2)`2 by A4,A7,GOBOARD5:2
.= G*(i1,j1)`2 by A3,A6,A7,GOBOARD5:2;
assume
A10: not thesis;
per cases by A10,AXIOMS:21;
suppose i1 < i2;
hence contradiction by A3,A4,A6,A7,A8,GOBOARD5:4;
suppose i1 > i2;
hence contradiction by A3,A4,A6,A7,A8,GOBOARD5:4;
suppose j1 < j2;
hence contradiction by A4,A5,A7,A9,GOBOARD5:5;
suppose j1 > j2;
hence contradiction by A4,A5,A7,A9,GOBOARD5:5;
end;
theorem Th33:
for f being FinSequence of TOP-REAL 2, M being Go-board
holds f is_sequence_on M implies mid(f,i1,i2) is_sequence_on M
proof let f be FinSequence of TOP-REAL 2, M be Go-board;
assume that
A1: f is_sequence_on M;
per cases;
suppose i1<=i2;
then A2: mid(f,i1,i2) = (f/^(i1-'1))|(i2-'i1+1) by JORDAN3:def 1;
f/^(i1-'1) is_sequence_on M by A1,JORDAN8:5;
hence mid(f,i1,i2) is_sequence_on M by A2,GOBOARD1:38;
suppose i1 > i2;
then A3: mid(f,i1,i2) = Rev ((f/^(i2-'1))|(i1-'i2+1)) by JORDAN3:def 1;
f/^(i2-'1) is_sequence_on M by A1,JORDAN8:5;
then (f/^(i2-'1))|(i1-'i2+1) is_sequence_on M by GOBOARD1:38;
hence mid(f,i1,i2) is_sequence_on M by A3,JORDAN9:7;
end;
definition
cluster -> non empty non-empty Go-board;
coherence
proof let G be Go-board;
A1: len G <> 0 by GOBOARD1:def 5;
thus G is non empty by CARD_1:47,GOBOARD1:def 5;
assume G is not non-empty;
then consider n being set such that
A2: n in dom G and
A3: G.n is empty by UNIALG_1:def 6;
len G > 0 by A1,NAT_1:19;
then consider s0 being FinSequence such that
A4: s0 in rng G and
A5: len s0 = width G by MATRIX_1:def 4;
consider n0 being Nat such that
A6: for x being set st x in rng G
ex s being FinSequence st s=x & len s = n0 by MATRIX_1:def 1;
G.n in rng G by A2,FUNCT_1:12;
then consider s1 being FinSequence such that
A7: s1 = G.n and
A8: len s1 = n0 by A6;
ex s being FinSequence st s=s0 & len s = n0 by A4,A6;
hence contradiction by A3,A5,A7,A8,CARD_1:47,GOBOARD1:def 5;
end;
end;
theorem Th34:
for G being Go-board st 1 <= i & i <= len G holds
SgmX(RealOrd, proj1.:Values G).i = G*(i,1)`1
proof let G be Go-board such that
A1: 1 <= i & i <= len G;
deffunc F(Nat)=G*($1,1)`1;
consider f being FinSequence of REAL such that
A2: len f = len G and
A3: for i st i in Seg len G holds f.i = F(i) from SeqLambdaD;
0 <> width G by GOBOARD1:def 5;
then A4: 1 <= width G by RLVECT_1:99;
reconsider A = proj1.:Values G as finite Subset of REAL;
A5: rng f = A
proof
A6: Values G = { G*(m,n): [m,n] in Indices G } by GOBRD13:7;
thus rng f c= A
proof let x be set;
assume
A7: x in rng f;
rng f c= REAL by FINSEQ_1:def 4;
then reconsider x as Element of REAL by A7;
consider y being set such that
A8: y in dom f and
A9: x = f.y by A7,FUNCT_1:def 5;
reconsider y as Nat by A8;
1 <= y & y <= len G by A2,A8,FINSEQ_3:27;
then [y,1] in Indices G by A4,GOBOARD7:10;
then A10: G*(y,1) in Values G by A6;
y in Seg len G by A2,A8,FINSEQ_1:def 3;
then x = G*(y,1)`1 by A3,A9
.= proj1.(G*(y,1)) by PSCOMP_1:def 28;
hence thesis by A10,FUNCT_2:43;
end;
let x be set;
assume
A11: x in A;
then reconsider x as Element of REAL;
consider p being Element of TOP-REAL 2 such that
A12: p in Values G and
A13: x = proj1.p by A11,FUNCT_2:116;
consider m,n such that
A14: p = G*(m,n) and
A15: [m,n] in Indices G by A6,A12;
A16: 1 <= n & n <= width G by A15,GOBOARD5:1;
A17: 1 <= m & m <= len G by A15,GOBOARD5:1;
then A18: m in Seg len G by FINSEQ_1:3;
A19: m in dom f by A2,A17,FINSEQ_3:27;
x = p`1 by A13,PSCOMP_1:def 28
.= G*(m,1)`1 by A14,A16,A17,GOBOARD5:3
.= f.m by A3,A18;
hence thesis by A19,FUNCT_1:def 5;
end;
for n,m be Nat st n in dom f & m in dom f & n < m
holds f/.n <> f/.m & [f/.n, f/.m] in RealOrd
proof let n,m be Nat such that
A20: n in dom f and
A21: m in dom f and
A22: n < m;
dom f = Seg len G by A2,FINSEQ_1:def 3;
then A23: f.n = G*(n,1)`1 & f.m = G*(m,1)`1 by A3,A20,A21;
A24: 1 <= n & m <= len G by A2,A20,A21,FINSEQ_3:27;
then A25: f.n < f.m by A4,A22,A23,GOBOARD5:4;
A26: f/.n = f.n & f/.m = f.m by A20,A21,FINSEQ_4:def 4;
hence f/.n <> f/.m by A4,A22,A23,A24,GOBOARD5:4;
thus [f/.n, f/.m] in RealOrd by A25,A26,Def1;
end;
then A27: f = SgmX(RealOrd, proj1.:Values G) by A5,TRIANG_1:4;
i in dom G by A1,FINSEQ_3:27;
then i in Seg len G by FINSEQ_1:def 3;
hence SgmX(RealOrd, proj1.:Values G).i = G*(i,1)`1 by A3,A27;
end;
theorem Th35:
for G being Go-board st 1 <= j & j <= width G holds
SgmX(RealOrd, proj2.:Values G).j = G*(1,j)`2
proof let G be Go-board such that
A1: 1 <= j & j <= width G;
deffunc F(Nat)=G*(1,$1)`2;
consider f being FinSequence of REAL such that
A2: len f = width G and
A3: for i st i in Seg width G holds f.i = F(i) from SeqLambdaD;
0 <> len G by GOBOARD1:def 5;
then A4: 1 <= len G by RLVECT_1:99;
reconsider A = proj2.:Values G as finite Subset of REAL;
A5: rng f = A
proof
A6: Values G = { G*(m,n): [m,n] in Indices G } by GOBRD13:7;
thus rng f c= A
proof let x be set;
assume
A7: x in rng f;
rng f c= REAL by FINSEQ_1:def 4;
then reconsider x as Element of REAL by A7;
consider y being set such that
A8: y in dom f and
A9: x = f.y by A7,FUNCT_1:def 5;
reconsider y as Nat by A8;
1 <= y & y <= width G by A2,A8,FINSEQ_3:27;
then [1,y] in Indices G by A4,GOBOARD7:10;
then A10: G*(1,y) in Values G by A6;
y in Seg width G by A2,A8,FINSEQ_1:def 3;
then x = G*(1,y)`2 by A3,A9
.= proj2.(G*(1,y)) by PSCOMP_1:def 29;
hence thesis by A10,FUNCT_2:43;
end;
let x be set;
assume
A11: x in A;
then reconsider x as Element of REAL;
consider p being Element of TOP-REAL 2 such that
A12: p in Values G and
A13: x = proj2.p by A11,FUNCT_2:116;
consider m,n such that
A14: p = G*(m,n) and
A15: [m,n] in Indices G by A6,A12;
A16: 1 <= m & m <= len G by A15,GOBOARD5:1;
A17: 1 <= n & n <= width G by A15,GOBOARD5:1;
then A18: n in Seg width G by FINSEQ_1:3;
A19: n in dom f by A2,A17,FINSEQ_3:27;
x = p`2 by A13,PSCOMP_1:def 29
.= G*(1,n)`2 by A14,A16,A17,GOBOARD5:2
.= f.n by A3,A18;
hence thesis by A19,FUNCT_1:def 5;
end;
for n,m be Nat st n in dom f & m in dom f & n < m
holds f/.n <> f/.m & [f/.n, f/.m] in RealOrd
proof let n,m be Nat such that
A20: n in dom f and
A21: m in dom f and
A22: n < m;
dom f = Seg width G by A2,FINSEQ_1:def 3;
then A23: f.n = G*(1,n)`2 & f.m = G*(1,m)`2 by A3,A20,A21;
A24: 1 <= n & m <= width G by A2,A20,A21,FINSEQ_3:27;
then A25: f.n < f.m by A4,A22,A23,GOBOARD5:5;
A26: f/.n = f.n & f/.m = f.m by A20,A21,FINSEQ_4:def 4;
hence f/.n <> f/.m by A4,A22,A23,A24,GOBOARD5:5;
thus [f/.n, f/.m] in RealOrd by A25,A26,Def1;
end;
then A27: f = SgmX(RealOrd, proj2.:Values G) by A5,TRIANG_1:4;
j in Seg width G by A1,FINSEQ_1:3;
hence SgmX(RealOrd, proj2.:Values G).j = G*(1,j)`2 by A3,A27;
end;
theorem Th36:
for f being non empty FinSequence of TOP-REAL 2, G being Go-board
st f is_sequence_on G &
(ex i st [1,i] in Indices G & G*(1,i) in rng f) &
(ex i st [len G,i] in Indices G & G*(len G,i) in rng f)
holds proj1.:rng f = proj1.:Values G
proof let f be non empty FinSequence of TOP-REAL 2, G be Go-board such that
A1: f is_sequence_on G;
given i1 being Nat such that
A2: [1,i1] in Indices G and
A3: G*(1,i1) in rng f;
given i2 being Nat such that
A4: [len G,i2] in Indices G and
A5: G*(len G,i2) in rng f;
rng f c= Values G by A1,GOBRD13:9;
hence proj1.:rng f c= proj1.:Values G by RELAT_1:156;
A6: Values G = { G*(i,j): [i,j] in Indices G } by GOBRD13:7;
consider k1 being set such that
A7: k1 in dom f and
A8: G*(1,i1) = f.k1 by A3,FUNCT_1:def 5;
reconsider k1 as Nat by A7;
A9: 1 <= k1 & k1 <= len f by A7,FINSEQ_3:27;
consider k2 being set such that
A10: k2 in dom f and
A11: G*(len G,i2) = f.k2 by A5,FUNCT_1:def 5;
reconsider k2 as Nat by A10;
A12: 1 <= k2 & k2 <= len f by A10,FINSEQ_3:27;
set g = mid(f,k1,k2);
A13: g is_sequence_on G by A1,Th33;
A14: now per cases;
suppose k1 <= k2;
then A15: len g = k2-'k1+1 by A9,A12,JORDAN4:20;
k2-'k1 >= 0 by NAT_1:18;
hence len g >= 0+1 by A15,AXIOMS:24;
suppose k1 > k2;
then A16: len g=k1-'k2+1 by A9,A12,JORDAN4:21;
k1-'k2 >= 0 by NAT_1:18;
hence len g >= 0+1 by A16,AXIOMS:24;
end;
A17: proj1.:Values G c= proj1.:rng g
proof assume not thesis;
then consider x being Element of REAL such that
A18: x in proj1.:Values G and
A19: not x in proj1.:rng g by SUBSET_1:7;
consider p being Element of TOP-REAL 2 such that
A20: p in Values G and
A21: x = proj1.p by A18,FUNCT_2:116;
consider i0,j0 being Nat such that
A22: p = G*(i0,j0) and
A23: [i0,j0] in Indices G by A6,A20;
A24: 1 <= i0 & i0 <= len G by A23,GOBOARD5:1;
A25: 1 <= j0 & j0 <= width G by A23,GOBOARD5:1;
defpred P[Nat] means 1 <= $1 & $1 <= len g implies
for i,j st [i,j] in Indices G & G*(i,j) = g.$1 holds i < i0;
A26: P[0];
A27: for n st P[n] holds P[n+1]
proof let n such that
A28: 1 <= n & n <= len g implies
for i,j st [i,j] in Indices G & G*(i,j) = g.n
holds i < i0 and
A29: 1 <= n+1 & n+1 <= len g;
let i,j such that
A30: [i,j] in Indices G and
A31: G*(i,j) = g.(n+1);
A32: now assume
A33: i = i0;
A34: n+1 in dom g by A29,FINSEQ_3:27;
then A35: G*(i,j) = g/.(n+1) by A31,FINSEQ_4:def 4;
A36: 1 <= j & j <= width G by A30,GOBOARD5:1;
A37: x = p`1 by A21,PSCOMP_1:def 28
.= G*(i0,1)`1 by A22,A24,A25,GOBOARD5:3
.= G*(i,j)`1 by A24,A33,A36,GOBOARD5:3
.= proj1.(g/.(n+1)) by A35,PSCOMP_1:def 28;
A38: dom proj1 = the carrier of TOP-REAL 2 by FUNCT_2:def 1;
g/.(n+1) in rng g by A31,A34,A35,FUNCT_1:12;
hence contradiction by A19,A37,A38,FUNCT_1:def 12;
end;
per cases;
suppose n = 0;
then G*(i,j) = G*(1,i1) by A8,A9,A12,A31,JORDAN3:27;
then i = 1 by A2,A30,Th32;
hence thesis by A24,A32,AXIOMS:21;
suppose A39: n <> 0;
then A40: 1 <= n by RLVECT_1:99;
A41: n <= n + 1 by NAT_1:29;
then n <= len g by A29,AXIOMS:22;
then A42: n in dom g by A40,FINSEQ_3:27;
then consider i1,j1 being Nat such that
A43: [i1,j1] in Indices G and
A44: g/.n = G*(i1,j1) by A13,GOBOARD1:def 11;
A45: n+1 in dom g by A29,FINSEQ_3:27;
then g/.(n+1) = G*(i,j) by A31,FINSEQ_4:def 4;
then abs(i1-i)+abs(j1-j) = 1 by A13,A30,A42,A43,A44,A45,GOBOARD1:def 11;
then A46: abs(i1-i)=1 & j1=j or abs(j1-j)=1 & i1=i by GOBOARD1:2;
now
g.n = g/.n by A42,FINSEQ_4:def 4;
then A47: i1 < i0 by A28,A29,A39,A41,A43,A44,AXIOMS:22,RLVECT_1:99;
per cases by A46,GOBOARD1:1;
suppose i1 = i or i < i1;
hence i < i0 by A47,AXIOMS:22;
suppose i = i1 + 1;
then i <= i0 by A47,NAT_1:38;
hence thesis by A32,AXIOMS:21;
end;
hence i < i0;
end;
A48: for n holds P[n] from Ind(A26,A27);
G*(len G,i2) = g.len g by A9,A11,A12,JORDAN4:23;
then len G < i0 by A4,A14,A48;
hence contradiction by A23,GOBOARD5:1;
end;
rng g c= rng f by JORDAN3:28;
then proj1.:rng g c= proj1.:rng f by RELAT_1:156;
hence thesis by A17,XBOOLE_1:1;
end;
theorem Th37:
for f being non empty FinSequence of TOP-REAL 2, G being Go-board
st f is_sequence_on G &
(ex i st [i,1] in Indices G & G*(i,1) in rng f) &
(ex i st [i,width G] in Indices G & G*(i,width G) in rng f)
holds proj2.:rng f = proj2.:Values G
proof let f be non empty FinSequence of TOP-REAL 2, G be Go-board such that
A1: f is_sequence_on G;
given i1 being Nat such that
A2: [i1,1] in Indices G and
A3: G*(i1,1) in rng f;
given i2 being Nat such that
A4: [i2,width G] in Indices G and
A5: G*(i2,width G) in rng f;
rng f c= Values G by A1,GOBRD13:9;
hence proj2.:rng f c= proj2.:Values G by RELAT_1:156;
A6: Values G = { G*(i,j): [i,j] in Indices G } by GOBRD13:7;
consider k1 being set such that
A7: k1 in dom f and
A8: G*(i1,1) = f.k1 by A3,FUNCT_1:def 5;
reconsider k1 as Nat by A7;
A9: 1 <= k1 & k1 <= len f by A7,FINSEQ_3:27;
consider k2 being set such that
A10: k2 in dom f and
A11: G*(i2, width G) = f.k2 by A5,FUNCT_1:def 5;
reconsider k2 as Nat by A10;
A12: 1 <= k2 & k2 <= len f by A10,FINSEQ_3:27;
set g = mid(f,k1,k2);
A13: g is_sequence_on G by A1,Th33;
A14: now per cases;
suppose k1 <= k2;
then A15: len g = k2-'k1+1 by A9,A12,JORDAN4:20;
k2-'k1 >= 0 by NAT_1:18;
hence len g >= 0+1 by A15,AXIOMS:24;
suppose k1 > k2;
then A16: len g=k1-'k2+1 by A9,A12,JORDAN4:21;
k1-'k2 >= 0 by NAT_1:18;
hence len g >= 0+1 by A16,AXIOMS:24;
end;
A17: proj2.:Values G c= proj2.:rng g
proof assume not thesis;
then consider x being Element of REAL such that
A18: x in proj2.:Values G and
A19: not x in proj2.:rng g by SUBSET_1:7;
consider p being Element of TOP-REAL 2 such that
A20: p in Values G and
A21: x = proj2.p by A18,FUNCT_2:116;
consider i0,j0 being Nat such that
A22: p = G*(i0,j0) and
A23: [i0,j0] in Indices G by A6,A20;
A24: 1 <= i0 & i0 <= len G by A23,GOBOARD5:1;
A25: 1 <= j0 & j0 <= width G by A23,GOBOARD5:1;
defpred P[Nat] means 1 <= $1 & $1 <= len g implies
for i,j st [i,j] in Indices G & G*(i,j) = g.$1
holds j < j0;
A26: P[0];
A27: for n st P[n] holds P[n+1]
proof let n such that
A28: 1 <= n & n <= len g implies
for i,j st [i,j] in Indices G & G*(i,j) = g.n
holds j < j0 and
A29: 1 <= n+1 & n+1 <= len g;
let i,j such that
A30: [i,j] in Indices G and
A31: G*(i,j) = g.(n+1);
A32: now assume
A33: j = j0;
A34: n+1 in dom g by A29,FINSEQ_3:27;
then A35: G*(i,j) = g/.(n+1) by A31,FINSEQ_4:def 4;
A36: 1 <= i & i <= len G by A30,GOBOARD5:1;
A37: x = p`2 by A21,PSCOMP_1:def 29
.= G*(1,j0)`2 by A22,A24,A25,GOBOARD5:2
.= G*(i,j)`2 by A25,A33,A36,GOBOARD5:2
.= proj2.(g/.(n+1)) by A35,PSCOMP_1:def 29;
A38: dom proj2 = the carrier of TOP-REAL 2 by FUNCT_2:def 1;
g/.(n+1) in rng g by A31,A34,A35,FUNCT_1:12;
hence contradiction by A19,A37,A38,FUNCT_1:def 12;
end;
per cases;
suppose n = 0;
then G*(i,j) = G*(i1,1) by A8,A9,A12,A31,JORDAN3:27;
then j = 1 by A2,A30,Th32;
hence thesis by A25,A32,AXIOMS:21;
suppose A39: n <> 0;
then A40: 1 <= n by RLVECT_1:99;
A41: n <= n + 1 by NAT_1:29;
then n <= len g by A29,AXIOMS:22;
then A42: n in dom g by A40,FINSEQ_3:27;
then consider i1,j1 being Nat such that
A43: [i1,j1] in Indices G and
A44: g/.n = G*(i1,j1) by A13,GOBOARD1:def 11;
A45: n+1 in dom g by A29,FINSEQ_3:27;
then g/.(n+1) = G*(i,j) by A31,FINSEQ_4:def 4;
then abs(i1-i)+abs(j1-j) = 1 by A13,A30,A42,A43,A44,A45,GOBOARD1:def 11;
then A46: abs(i1-i)=1 & j1=j or abs(j1-j)=1 & i1=i by GOBOARD1:2;
now
g.n = g/.n by A42,FINSEQ_4:def 4;
then A47: j1 < j0 by A28,A29,A39,A41,A43,A44,AXIOMS:22,RLVECT_1:99;
per cases by A46,GOBOARD1:1;
suppose j1 = j or j < j1;
hence j < j0 by A47,AXIOMS:22;
suppose j = j1 + 1;
then j <= j0 by A47,NAT_1:38;
hence thesis by A32,AXIOMS:21;
end;
hence j < j0;
end;
A48: for n holds P[n] from Ind(A26,A27);
G*(i2,width G) = g.len g by A9,A11,A12,JORDAN4:23;
then width G < j0 by A4,A14,A48;
hence contradiction by A23,GOBOARD5:1;
end;
rng g c= rng f by JORDAN3:28;
then proj2.:rng g c= proj2.:rng f by RELAT_1:156;
hence thesis by A17,XBOOLE_1:1;
end;
definition let G be Go-board;
cluster Values G -> non empty;
coherence
proof
dom G is non empty;
then reconsider f = rngs G as non empty non-empty Function
by EXTENS_1:4,RELAT_1:60;
Union f is non empty;
hence thesis by GOBRD13:def 1;
end;
end;
theorem Th38:
for G being Go-board holds
G = GoB(SgmX(RealOrd, proj1.:Values G), SgmX(RealOrd,proj2.:Values G))
proof let G be Go-board;
set v1 = SgmX(RealOrd, proj1.:Values G), v2 = SgmX(RealOrd,proj2.:Values G);
A1: len G = card(proj1.:Values G) by Th22
.= len v1 by Th15;
A2: width G = card(proj2.:Values G) by Th25
.= len v2 by Th15;
for n,m st [n,m] in Indices G holds G*(n,m) = |[v1.n,v2.m]|
proof let n,m;
assume
A3: [n,m] in Indices G;
then A4: 1 <= n & n <= len G by GOBOARD5:1;
then A5: v1.n = G*(n,1)`1 by Th34;
A6: 1 <= m & m <= width G by A3,GOBOARD5:1;
then v2.m = G*(1,m)`2 by Th35;
then A7: v2.m = G*(n,m)`2 by A4,A6,GOBOARD5:2;
v1.n = G*(n,m)`1 by A4,A5,A6,GOBOARD5:3;
hence G*(n,m) = |[v1.n,v2.m]| by A7,EUCLID:57;
end;
hence G = GoB(SgmX(RealOrd, proj1.:Values G), SgmX(RealOrd,proj2.:Values G))
by A1,A2,GOBOARD2:def 1;
end;
theorem Th39:
for f being non empty FinSequence of TOP-REAL 2, G being Go-board
st proj1.:rng f = proj1.:Values G & proj2.:rng f = proj2.:Values G
holds G = GoB f
proof let f be non empty FinSequence of TOP-REAL 2, G being Go-board;
assume
A1: proj1.:rng f = proj1.:Values G & proj2.:rng f = proj2.:Values G;
X_axis f = proj1*f by Th16;
then rng X_axis f = proj1.:rng f by RELAT_1:160;
then A2: Incr X_axis f = SgmX(RealOrd, proj1.:rng f) by Th13;
Y_axis f = proj2*f by Th17;
then rng Y_axis f = proj2.:rng f by RELAT_1:160;
then Incr Y_axis f = SgmX(RealOrd, proj2.:rng f) by Th13;
hence G = GoB(Incr X_axis f, Incr Y_axis f) by A1,A2,Th38
.= GoB f by GOBOARD2:def 3;
end;
theorem Th40:
for f being non empty FinSequence of TOP-REAL 2, G being Go-board
st f is_sequence_on G &
(ex i st [1,i] in Indices G & G*(1,i) in rng f) &
(ex i st [i,1] in Indices G & G*(i,1) in rng f) &
(ex i st [len G,i] in Indices G & G*(len G,i) in rng f) &
(ex i st [i,width G] in Indices G & G*(i,width G) in rng f)
holds G = GoB f
proof let f be non empty FinSequence of TOP-REAL 2, G being Go-board such that
A1: f is_sequence_on G;
given i1 being Nat such that
A2: [1,i1] in Indices G and
A3: G*(1,i1) in rng f;
given i2 being Nat such that
A4: [i2,1] in Indices G and
A5: G*(i2,1) in rng f;
given i3 being Nat such that
A6: [len G,i3] in Indices G and
A7: G*(len G,i3) in rng f;
given i4 being Nat such that
A8: [i4,width G] in Indices G and
A9: G*(i4,width G) in rng f;
A10: proj1.:rng f = proj1.:Values G by A1,A2,A3,A6,A7,Th36;
proj2.:rng f = proj2.:Values G by A1,A4,A5,A8,A9,Th37;
hence thesis by A10,Th39;
end;
begin :: More about gauges
theorem Th41:
m <= n & 1 <= i & i+1 <= len Gauge(C,n)
implies [\ (i-2)/2|^(n-'m)+2 /] is Nat
proof assume that
A1: m <= n and
A2: 1 <= i & i+1 <= len Gauge(C,n);
set i1 = [\ (i-2)/2|^(n-'m)+2 /];
(i-2)/2|^(n-'m)+2-1 = (i-2)/2|^(n-'m)+(2-1) by XCMPLX_1:29;
then A3: (i-2)/2|^(n-'m)+1 < i1 by INT_1:def 4;
m + 0 <= n by A1;
then n -' m >= 0 by SPRECT_3:8;
then A4: n -' m + 1 >= 0 + 1 by AXIOMS:24;
A5: n-'m +1 <= 2|^(n-'m) by HEINE:7;
then A6: 0 +1 <= 2|^(n-'m) by A4,AXIOMS:22;
A7: 0 < 2|^(n-'m) by A4,A5,AXIOMS:22;
1-2 <= i-2 by A2,REAL_1:49;
then A8: (-1)/2|^(n-'m) <= (i-2)/2|^(n-'m) by A7,REAL_1:73;
(-1)/1 <= (-1)/2|^(n-'m) by A6,REAL_2:203;
then -1 <= (i-2)/2|^(n-'m) by A8,AXIOMS:22;
then -1 + 1 <= (i-2)/2|^(n-'m) + 1 by AXIOMS:24;
then i1 >= 0 by A3,AXIOMS:22;
hence i1 is Nat by INT_1:16;
end;
theorem Th42:
m <= n & 1 <= i & i+1 <= len Gauge(C,n)
implies
1 <= [\ (i-2)/2|^(n-'m)+2 /] & [\ (i-2)/2|^(n-'m)+2 /]+1 <= len Gauge(C,m)
proof assume that
A1: m <= n and
A2: 1 <= i & i+1 <= len Gauge(C,n);
set i1 = [\ (i-2)/2|^(n-'m)+2 /];
(i-2)/2|^(n-'m)+2-1 = (i-2)/2|^(n-'m)+(2-1) by XCMPLX_1:29;
then A3: (i-2)/2|^(n-'m)+1 < i1 by INT_1:def 4;
m + 0 <= n by A1;
then n -' m >= 0 by SPRECT_3:8;
then A4: n -' m + 1 >= 0 + 1 by AXIOMS:24;
A5: n-'m +1 <= 2|^(n-'m) by HEINE:7;
then A6: 0 +1 <= 2|^(n-'m) by A4,AXIOMS:22;
A7: 0 < 2|^(n-'m) by A4,A5,AXIOMS:22;
1-2 <= i-2 by A2,REAL_1:49;
then A8: (-1)/2|^(n-'m) <= (i-2)/2|^(n-'m) by A7,REAL_1:73;
(-1)/1 <= (-1)/2|^(n-'m) by A6,REAL_2:203;
then -1 <= (i-2)/2|^(n-'m) by A8,AXIOMS:22;
then -1 + 1 <= (i-2)/2|^(n-'m) + 1 by AXIOMS:24;
then i1 >= 1+0 by A3,INT_1:20;
hence 1 <= i1;
i1 <= (i-2)/2|^(n-'m)+2 by INT_1:def 4;
then i1+1 <= (i-2)/2|^(n-'m)+2+1 by AXIOMS:24;
then A9: i1+1 <= (i-2)/2|^(n-'m)+(2+1) by XCMPLX_1:1;
i+1 <= 2|^n+ (2+1) by A2,JORDAN8:def 1;
then i+1 <= 2|^n+ 2+1 by XCMPLX_1:1;
then i <= 2|^n+ 2 by REAL_1:53;
then i-2 <= 2|^n by REAL_1:86;
then (i-2) <= 2|^(m+(n-'m)) by A1,AMI_5:4;
then (i-2)*1 <= 2|^m*2|^(n-'m) by NEWTON:13;
then (i-2)/2|^(n-'m) <= 2|^m/1 by A7,REAL_2:187;
then (i-2)/2|^(n-'m) + 3 <= 2|^m + 3 by AXIOMS:24;
then (i-2)/2|^(n-'m) + 3 <= len Gauge(C,m) by JORDAN8:def 1;
hence i1+1 <= len Gauge(C,m) by A9,AXIOMS:22;
end;
theorem Th43:
m <= n & 1 <= i & i+1 <= len Gauge(C,n) & 1 <= j & j+1 <= width Gauge(C,n)
implies
ex i1,j1 st
i1 = [\ (i-2)/2|^(n-'m)+2 /] & j1 = [\ (j-2)/2|^(n-'m)+2 /] &
cell(Gauge(C,n),i,j) c= cell(Gauge(C,m),i1,j1)
proof assume that
A1: m <= n and
A2: 1 <= i & i+1 <= len Gauge(C,n) and
A3: 1 <= j & j+1 <= width Gauge(C,n);
A4: len Gauge(C,m) = width Gauge(C,m) & len Gauge(C,n) = width Gauge(C,n)
by JORDAN8:def 1;
then reconsider i1 = [\ (i-2)/2|^(n-'m)+2 /],
j1 = [\ (j-2)/2|^(n-'m)+2 /] as Nat by A1,A2,A3,Th41;
take i1,j1;
thus i1 = [\ (i-2)/2|^(n-'m)+2 /];
thus j1 = [\ (j-2)/2|^(n-'m)+2 /];
(i-2)/2|^(n-'m)+2-1 = (i-2)/2|^(n-'m)+(2-1) by XCMPLX_1:29;
then A5: (i-2)/2|^(n-'m)+1 < i1 by INT_1:def 4;
m + 0 <= n by A1;
then A6: n -' m >= 0 by SPRECT_3:8;
then A7: n -' m + 1 >= 0 + 1 by AXIOMS:24;
A8: n-'m +1 <= 2|^(n-'m) by HEINE:7;
then A9: 0 +1 <= 2|^(n-'m) by A7,AXIOMS:22;
A10: 0 < 2|^(n-'m) by A7,A8,AXIOMS:22;
1-2 <= i-2 by A2,REAL_1:49;
then A11: (-1)/2|^(n-'m) <= (i-2)/2|^(n-'m) by A10,REAL_1:73;
A12: (-1)/1 <= (-1)/2|^(n-'m) by A9,REAL_2:203;
then -1 <= (i-2)/2|^(n-'m) by A11,AXIOMS:22;
then -1 + 1 <= (i-2)/2|^(n-'m) + 1 by AXIOMS:24;
then A13: i1 >= 1+0 by A5,INT_1:20;
(j-2)/2|^(n-'m)+2-1 = (j-2)/2|^(n-'m)+(2-1) by XCMPLX_1:29;
then A14: (j-2)/2|^(n-'m)+1 < j1 by INT_1:def 4;
1-2 <= j-2 by A3,REAL_1:49;
then (-1)/2|^(n-'m) <= (j-2)/2|^(n-'m) by A10,REAL_1:73;
then -1 <= (j-2)/2|^(n-'m) by A12,AXIOMS:22;
then -1 + 1 <= (j-2)/2|^(n-'m) + 1 by AXIOMS:24;
then A15: j1 >= 1+0 by A14,INT_1:20;
A16:i1 <= (i-2)/2|^(n-'m)+2 by INT_1:def 4;
A17: i1+1 <= len Gauge(C,m) by A1,A2,Th42;
A18: j1 <= (j-2)/2|^(n-'m)+2 by INT_1:def 4;
A19: j1+1 <= width Gauge(C,m) by A1,A3,A4,Th42;
let e be set;
set Gm = Gauge(C,m), Gn = Gauge(C,n);
assume
A20: e in cell(Gauge(C,n),i,j);
then reconsider p = e as Point of TOP-REAL 2;
A21: 2|^m >m by HEINE:8;
A22: m >= 0 by NAT_1:18;
i <= len Gn & j <= width Gn by A2,A3,NAT_1:38;
then [i,j] in Indices Gn by A2,A3,GOBOARD7:10;
then A23: Gn*(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)]|
by JORDAN8:def 1;
then A24: Gn*(i,j)`1 =(W-bound C)+(((E-bound C)-(W-bound C))/(2|^n))*((i-2)
/1)
by EUCLID:56
.= (W-bound C)+((E-bound C)-(W-bound C))/1 *((i-2)/(2|^n)) by XCMPLX_1:
86;
A25: Gn*(i,j)`2 =(S-bound C)+(((N-bound C)-(S-bound C))/(2|^n))*((j-2)/1)
by A23,EUCLID:56
.= (S-bound C)+(((N-bound C)-(S-bound C))/1)*((j-2)/(2|^n)) by XCMPLX_1:86
;
i1 <= len Gauge(C,m) & j1 <= width Gauge(C,m) by A17,A19,NAT_1:38;
then [i1,j1] in Indices Gm by A13,A15,GOBOARD7:10;
then A26: Gm*(i1,j1) =|[(W-bound C)+(((E-bound C)-(W-bound C))/(2|^m))*(i1-
2),
(S-bound C)+(((N-bound C)-(S-bound C))/(2|^m))*(j1-2)]|
by JORDAN8:def 1;
then A27: Gm*(i1,j1)`1 =(W-bound C)+(((E-bound C)-(W-bound C))/(2|^m))*((i1
-2)/1)
by EUCLID:56
.= (W-bound C)+(((E-bound C)-(W-bound C))/1)*((i1-2)/(2|^m)) by XCMPLX_1:
86;
A28: Gm*(i1,j1)`2 =(S-bound C)+(((N-bound C)-(S-bound C))/(2|^m))*((j1-2)/1)
by A26,EUCLID:56
.= (S-bound C)+(((N-bound C)-(S-bound C))/1)*((j1-2)/(2|^m)) by XCMPLX_1:
86;
(E-bound C) >= (W-bound C)+0 by SPRECT_1:23;
then A29: (E-bound C)-(W-bound C) >= 0 by REAL_1:84;
(N-bound C) >= (S-bound C)+0 by SPRECT_1:24;
then A30: (N-bound C)-(S-bound C) >= 0 by REAL_1:84;
A31: Gn*(i,j)`1 <= p`1 by A2,A3,A20,JORDAN9:19;
i1-2 <= (i-2)/2|^(n-'m) by A16,REAL_1:86;
then (i1-2)/2|^m <= (i-2)/2|^(n-'m)/2|^m by A21,A22,REAL_1:73;
then (i1-2)/2|^m <= (i-2)/(2|^(n-'m)*2|^m) by XCMPLX_1:79;
then (i1-2)/2|^m <= (i-2)/2|^(n-'m+m) by NEWTON:13;
then (i1-2)/2|^m <= (i-2)/2|^n by A1,AMI_5:4;
then (((E-bound C)-(W-bound C)))*((i1-2)/(2|^m))
<= (((E-bound C)-(W-bound C)))*((i-2)/(2|^n)) by A29,AXIOMS:25;
then Gm*(i1,j1)`1 <= Gn*(i,j)`1 by A24,A27,AXIOMS:24;
then A32: Gm*(i1,j1)`1 <= p`1 by A31,AXIOMS:22;
1 <= i1+1 & j1 <= width Gauge(C,m) by A19,NAT_1:29,38;
then [i1+1,j1] in Indices Gm by A15,A17,GOBOARD7:10;
then Gm*(i1+1,j1)
=|[(W-bound C)+(((E-bound C)-(W-bound C))/(2|^m))*(i1+1-2),
(S-bound C)+(((N-bound C)-(S-bound C))/(2|^m))*(j1-2)]|
by JORDAN8:def 1;
then A33: Gm*(i1+1,j1)`1
=(W-bound C)+(((E-bound C)-(W-bound C))/(2|^m))*((i1+1-2)/1)
by EUCLID:56
.= (W-bound C)+(((E-bound C)-(W-bound C))/1)*((i1+1-2)/(2|^m))
by XCMPLX_1:86;
1 <= i+1 & j <= width Gn by A3,NAT_1:29,38;
then [i+1,j] in Indices Gn by A2,A3,GOBOARD7:10;
then Gn*(i+1,j) =|[(W-bound C)+(((E-bound C)-(W-bound C))/(2|^n))*(i+1-2),
(S-bound C)+(((N-bound C)-(S-bound C))/(2|^n))*(j-2)]|
by JORDAN8:def 1;
then A34: Gn*(i+1,j)`1
=(W-bound C)+(((E-bound C)-(W-bound C))/(2|^n))*((i+1-2)/1)
by EUCLID:56
.= (W-bound C)+(((E-bound C)-(W-bound C))/1)*((i+1-2)/(2|^n))
by XCMPLX_1:86;
A35: p`1 <= Gn*(i+1,j)`1 by A2,A3,A20,JORDAN9:19;
A36: 2|^(n-'m) >n-'m by HEINE:8;
(i-2)/2|^(n-'m)+2-1 < i1 by INT_1:def 4;
then (i-2)/2|^(n-'m)+2 < i1+1 by REAL_1:84;
then (i-2)/2|^(n-'m) < i1+1-2 by REAL_1:86;
then (i-2) < (i1+1-2)*2|^(n-'m) by A6,A36,REAL_2:177;
then (i-2) + 1 <= (i1+1-2)*2|^(n-'m) by INT_1:20;
then i+1-2 <= (i1+1-2)*2|^(n-'m) by XCMPLX_1:29;
then (i+1-2)/2|^(n-'m) <= i1+1-2 by A6,A36,REAL_2:177;
then (i+1-2)/2|^(n-'m)/2|^m <= (i1+1-2)/2|^m by A21,A22,REAL_1:73;
then (i+1-2)/(2|^(n-'m)*2|^m) <= (i1+1-2)/2|^m by XCMPLX_1:79;
then (i+1-2)/2|^(n-'m+m) <= (i1+1-2)/2|^m by NEWTON:13;
then (i+1-2)/2|^n <= (i1+1-2)/2|^m by A1,AMI_5:4;
then (((E-bound C)-(W-bound C)))*((i+1-2)/(2|^n))
<= (((E-bound C)-(W-bound C)))*((i1+1-2)/(2|^m)) by A29,AXIOMS:25;
then Gn*(i+1,j)`1 <= Gm*(i1+1,j1)`1 by A33,A34,AXIOMS:24;
then A37: p`1 <= Gm*(i1+1,j1)`1 by A35,AXIOMS:22;
A38: Gn*(i,j)`2 <= p`2 by A2,A3,A20,JORDAN9:19;
j1-2 <= (j-2)/2|^(n-'m) by A18,REAL_1:86;
then (j1-2)/2|^m <= (j-2)/2|^(n-'m)/2|^m by A21,A22,REAL_1:73;
then (j1-2)/2|^m <= (j-2)/(2|^(n-'m)*2|^m) by XCMPLX_1:79;
then (j1-2)/2|^m <= (j-2)/2|^(n-'m+m) by NEWTON:13;
then (j1-2)/2|^m <= (j-2)/2|^n by A1,AMI_5:4;
then (((N-bound C)-(S-bound C)))*((j1-2)/(2|^m))
<= (((N-bound C)-(S-bound C)))*((j-2)/(2|^n)) by A30,AXIOMS:25;
then Gm*(i1,j1)`2 <= Gn*(i,j)`2 by A25,A28,AXIOMS:24;
then A39: Gm*(i1,j1)`2 <= p`2 by A38,AXIOMS:22;
1 <= j1+1 & i1 <= len Gauge(C,m) by A17,NAT_1:29,38;
then [i1,j1+1] in Indices Gm by A13,A19,GOBOARD7:10;
then Gm*(i1,j1+1) =|[(W-bound C)+(((E-bound C)-(W-bound C))/(2|^m))*(i1-2),
(S-bound C)+(((N-bound C)-(S-bound C))/(2|^m))*(j1+1-2)]|
by JORDAN8:def 1;
then A40: Gm*(i1,j1+1)`2
=(S-bound C)+(((N-bound C)-(S-bound C))/(2|^m))*((j1+1-2)/1)
by EUCLID:56
.= (S-bound C)+(((N-bound C)-(S-bound C))/1)*((j1+1-2)/(2|^m))
by XCMPLX_1:86;
1 <= j+1 & i <= len Gn by A2,NAT_1:29,38;
then [i,j+1] in Indices Gn by A2,A3,GOBOARD7:10;
then Gn*(i,j+1) =|[(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+1-2)]|
by JORDAN8:def 1;
then A41: Gn*(i,j+1)`2
=(S-bound C)+(((N-bound C)-(S-bound C))/(2|^n))*((j+1-2)/1)
by EUCLID:56
.= (S-bound C)+(((N-bound C)-(S-bound C))/1)*((j+1-2)/(2|^n))
by XCMPLX_1:86;
A42: p`2 <= Gn*(i,j+1)`2 by A2,A3,A20,JORDAN9:19;
(j-2)/2|^(n-'m)+2-1 < j1 by INT_1:def 4;
then (j-2)/2|^(n-'m)+2 < j1+1 by REAL_1:84;
then (j-2)/2|^(n-'m) < j1+1-2 by REAL_1:86;
then (j-2) < (j1+1-2)*2|^(n-'m) by A6,A36,REAL_2:177;
then (j-2) + 1 <= (j1+1-2)*2|^(n-'m) by INT_1:20;
then j+1-2 <= (j1+1-2)*2|^(n-'m) by XCMPLX_1:29;
then (j+1-2)/2|^(n-'m) <= j1+1-2 by A6,A36,REAL_2:177;
then (j+1-2)/2|^(n-'m)/2|^m <= (j1+1-2)/2|^m by A21,A22,REAL_1:73;
then (j+1-2)/(2|^(n-'m)*2|^m) <= (j1+1-2)/2|^m by XCMPLX_1:79;
then (j+1-2)/2|^(n-'m+m) <= (j1+1-2)/2|^m by NEWTON:13;
then (j+1-2)/2|^n <= (j1+1-2)/2|^m by A1,AMI_5:4;
then (((N-bound C)-(S-bound C)))*((j+1-2)/(2|^n))
<= (((N-bound C)-(S-bound C)))*((j1+1-2)/(2|^m)) by A30,AXIOMS:25;
then Gn*(i,j+1)`2 <= Gm*(i1,j1+1)`2 by A40,A41,AXIOMS:24;
then p`2 <= Gm*(i1,j1+1)`2 by A42,AXIOMS:22;
hence e in cell(Gauge(C,m),i1,j1) by A13,A15,A17,A19,A32,A37,A39,JORDAN9:19;
end;
theorem Th44:
m <= n & 1 <= i & i+1 <= len Gauge(C,n) & 1 <= j & j+1 <= width Gauge(C,n)
implies
ex i1,j1 st
1 <= i1 & i1+1 <= len Gauge(C,m) & 1 <= j1 & j1+1 <= width Gauge(C,m) &
cell(Gauge(C,n),i,j) c= cell(Gauge(C,m),i1,j1)
proof assume that
A1: m <= n and
A2: 1 <= i & i+1 <= len Gauge(C,n) and
A3: 1 <= j & j+1 <= width Gauge(C,n);
consider i1,j1 such that
A4: i1 = [\ (i-2)/2|^(n-'m)+2 /] and
A5: j1 = [\ (j-2)/2|^(n-'m)+2 /] and
A6: cell(Gauge(C,n),i,j) c= cell(Gauge(C,m),i1,j1) by A1,A2,A3,Th43;
take i1,j1;
thus 1 <= i1 & i1+1 <= len Gauge(C,m) by A1,A2,A4,Th42;
len Gauge(C,m) = width Gauge(C,m) & len Gauge(C,n) = width Gauge(C,n)
by JORDAN8:def 1;
hence 1 <= j1 & j1+1 <= width Gauge(C,m) by A1,A3,A5,Th42;
thus thesis by A6;
end;
canceled 2;
theorem
for P being Subset of TOP-REAL2 st P is Bounded
holds UBD P is not Bounded
proof let P be Subset of TOP-REAL2;
assume P is Bounded;
then ex B being Subset of TOP-REAL 2 st B is_outside_component_of P & B=UBD
P
by JORDAN2C:76;
hence UBD P is not Bounded by JORDAN2C:def 4;
end;
theorem Th48:
for f being non constant standard special_circular_sequence
st Rotate(f,p) is clockwise_oriented
holds f is clockwise_oriented
proof let f be non constant standard special_circular_sequence;
assume Rotate(f,p) is clockwise_oriented;
then reconsider g = Rotate(f,p) as
clockwise_oriented non constant standard special_circular_sequence;
1 < i & i < len f implies f/.i <> f/.1 by GOBOARD7:38;
then f = Rotate(g,f/.1) by REVROT_1:16;
hence thesis;
end;
theorem
for f being non constant standard special_circular_sequence
st LeftComp f = UBD L~f
holds f is clockwise_oriented
proof let f be non constant standard special_circular_sequence such that
A1: LeftComp f = UBD L~f;
set g = Rotate(f,N-min L~f);
A2: L~f = L~g by REVROT_1:33;
assume not thesis;
then g is not clockwise_oriented by Th48;
then A3: Rev g is clockwise_oriented by REVROT_1:38;
UBD L~f = UBD L~Rev g by A2,SPPOL_2:22
.= LeftComp Rev g by A3,GOBRD14:46
.= RightComp g by GOBOARD9:26
.= RightComp f by REVROT_1:37;
hence contradiction by A1,SPRECT_4:7;
end;
begin :: More about cages
theorem Th50:
for f being non constant standard special_circular_sequence
holds (Cl LeftComp(f))` = RightComp f
proof let f be non constant standard special_circular_sequence;
A1:Cl LeftComp f = (LeftComp f) \/ L~f by GOBRD14:32;
A2: Cl LeftComp f \/ RightComp f
= L~f \/ LeftComp f \/ RightComp f by GOBRD14:32
.= L~f \/ RightComp f \/ LeftComp f by XBOOLE_1:4
.= the carrier of TOP-REAL 2 by GOBRD14:25;
(Cl LeftComp(f))` misses Cl LeftComp(f) by SUBSET_1:44;
hence (Cl LeftComp(f))` c= RightComp(f) by A2,XBOOLE_1:73;
A3:L~f misses RightComp(f) by SPRECT_3:42;
RightComp f misses LeftComp f by GOBRD14:24;
then Cl LeftComp(f) misses RightComp(f) by A1,A3,XBOOLE_1:70;
hence RightComp(f) c= (Cl LeftComp(f))` by SUBSET_1:43;
end;
theorem
for f being non constant standard special_circular_sequence
holds (Cl RightComp(f))` = LeftComp f
proof let f be non constant standard special_circular_sequence;
A1:Cl RightComp f = (RightComp f) \/ L~f by GOBRD14:31;
A2: Cl RightComp f \/ LeftComp f
= L~f \/ RightComp f \/ LeftComp f by GOBRD14:31
.= the carrier of TOP-REAL 2 by GOBRD14:25;
(Cl RightComp(f))` misses Cl RightComp(f) by SUBSET_1:44;
hence (Cl RightComp(f))` c= LeftComp(f) by A2,XBOOLE_1:73;
A3:L~f misses LeftComp(f) by SPRECT_3:43;
LeftComp f misses RightComp f by GOBRD14:24;
then Cl RightComp(f) misses LeftComp(f) by A1,A3,XBOOLE_1:70;
hence LeftComp(f) c= (Cl RightComp(f))` by SUBSET_1:43;
end;
theorem Th52:
C is connected implies GoB Cage(C,n) = Gauge(C,n)
proof assume
A1: C is connected;
A2: 1 <= len Gauge(C,n) & 1 <= width Gauge(C,n) by GOBRD11:34;
consider iw being Nat such that
A3: 1 <= iw & iw <= width Gauge(C,n) and
A4: W-min L~Cage(C,n) = Gauge(C,n)*(1,iw) by A1,JORDAN1D:34;
A5: [1,iw] in Indices Gauge(C,n) by A2,A3,GOBOARD7:10;
A6: W-min L~Cage(C,n) in rng Cage(C,n) by SPRECT_2:47;
consider iS being Nat such that
A7: 1 <= iS & iS <= len Gauge(C,n) and
A8: Gauge(C,n)*(iS,1) = S-max L~Cage(C,n) by A1,JORDAN1D:32;
A9: [iS,1] in Indices Gauge(C,n) by A2,A7,GOBOARD7:10;
A10: S-max L~Cage(C,n) in rng Cage(C,n) by SPRECT_2:46;
consider ie being Nat such that
A11: 1 <= ie & ie <= width Gauge(C,n) and
A12: Gauge(C,n)*(len Gauge(C,n),ie) = E-max L~Cage(C,n) by A1,JORDAN1D:29;
A13: [len Gauge(C,n),ie] in Indices Gauge(C,n) by A2,A11,GOBOARD7:10;
A14: E-max L~Cage(C,n) in rng Cage(C,n) by SPRECT_2:50;
consider IN being Nat such that
A15: 1 <= IN & IN <= len Gauge(C,n) and
A16: Gauge(C,n)*(IN,width Gauge(C,n)) = N-min L~Cage(C,n) by A1,JORDAN1D:25;
A17: [IN,width Gauge(C,n)] in Indices Gauge(C,n) by A2,A15,GOBOARD7:10;
A18: N-min L~Cage(C,n) in rng Cage(C,n) by SPRECT_2:43;
Cage(C,n) is_sequence_on Gauge(C,n) by A1,JORDAN9:def 1;
hence thesis by A4,A5,A6,A8,A9,A10,A12,A13,A14,A16,A17,A18,Th40;
end;
theorem
C is connected implies N-min C in right_cell(Cage(C,n),1)
proof assume
A1: C is connected;
then consider i such that
A2: 1 <= i & i+1 <= len Gauge(C,n) and
A3: Cage(C,n)/.1 = Gauge(C,n)*(i,width Gauge(C,n)) and
A4: Cage(C,n)/.2 = Gauge(C,n)*(i+1,width Gauge(C,n)) and
A5: N-min C in cell(Gauge(C,n),i,width Gauge(C,n)-'1) and
N-min C <> Gauge(C,n)*(i,width Gauge(C,n)-'1) by JORDAN9:def 1;
len Cage(C,n) > 4 by GOBOARD7:36;
then A6: 1+1 <= len Cage(C,n) by AXIOMS:22;
for i1,j1,i2,j2 being Nat st
[i1,j1] in Indices GoB Cage(C,n) & [i2,j2] in Indices GoB Cage(C,n) &
Cage(C,n)/.1 = (GoB Cage(C,n))*(i1,j1) &
Cage(C,n)/.(1+1) = (GoB Cage(C,n))*(i2,j2) holds
i1 = i2 & j1+1 = j2 &
cell(Gauge(C,n),i,width Gauge(C,n)-'1) = cell(GoB Cage(C,n),i1,j1) or
i1+1 = i2 & j1 = j2 &
cell(Gauge(C,n),i,width Gauge(C,n)-'1) = cell(GoB Cage(C,n),i1,j1-'1) or
i1 = i2+1 & j1 = j2 &
cell(Gauge(C,n),i,width Gauge(C,n)-'1) = cell(GoB Cage(C,n),i2,j2) or
i1 = i2 & j1 = j2+1 &
cell(Gauge(C,n),i,width Gauge(C,n)-'1) = cell(GoB Cage(C,n),i1-'1,j2)
proof let i1,j1,i2,j2 be Nat such that
A7: [i1,j1] in Indices GoB Cage(C,n) and
A8: [i2,j2] in Indices GoB Cage(C,n) and
A9: Cage(C,n)/.1 = (GoB Cage(C,n))*(i1,j1) and
A10: Cage(C,n)/.(1+1) = (GoB Cage(C,n))*(i2,j2);
A11: GoB Cage(C,n) = Gauge(C,n) by A1,Th52;
0 <> width Gauge(C,n) by GOBOARD1:def 5;
then A12: 1 <= width Gauge(C,n) by RLVECT_1:99;
i < len Gauge(C,n) by A2,NAT_1:38;
then A13: [i,width Gauge(C,n)] in Indices Gauge(C,n) by A2,A12,GOBOARD7:10;
then A14: i1 = i & j1 = width Gauge(C,n) by A3,A7,A9,A11,GOBOARD1:21;
1 <= i+1 by NAT_1:29;
then [i+1,width Gauge(C,n)] in Indices Gauge(C,n) by A2,A12,GOBOARD7:10;
then A15: i2 = i+1 & j2 = width Gauge(C,n) by A4,A8,A10,A11,GOBOARD1:21;
per cases by A3,A7,A9,A11,A13,A15,GOBOARD1:21;
case i1 = i2 & j1+1 = j2;
hence cell(Gauge(C,n),i,width Gauge(C,n)-'1) = cell(GoB Cage(C,n),i1,j1)
by A14,A15,NAT_1:38;
case i1+1 = i2 & j1 = j2;
thus cell(Gauge(C,n),i,width Gauge(C,n)-'1) = cell(GoB Cage(C,n),i1,j1-'1)
by A1,A14,Th52;
case i1 = i2+1 & j1 = j2;
then i2 < i1 by NAT_1:38;
hence cell(Gauge(C,n),i,width Gauge(C,n)-'1) = cell(GoB Cage(C,n),i2,j2)
by A14,A15,NAT_1:38;
case i1 = i2 & j1 = j2+1;
hence cell(Gauge(C,n),i,width Gauge(C,n)-'1) = cell(GoB Cage(C,n),i1-'1,j2)
by A14,A15,NAT_1:38;
end;
hence thesis by A5,A6,GOBOARD5:def 6;
end;
theorem Th54:
C is connected & i <= j implies L~Cage(C,j) c= Cl RightComp(Cage(C,i))
proof assume that
A1: C is connected and
A2: i <= j and
A3: not L~Cage(C,j) c= Cl RightComp(Cage(C,i));
A4: Cage(C,j) is_sequence_on Gauge(C,j) by A1,JORDAN9:def 1;
consider p being Point of TOP-REAL 2 such that
A5: p in L~Cage(C,j) and
A6: not p in Cl RightComp(Cage(C,i)) by A3,SUBSET_1:7;
reconsider D = (L~Cage(C,i))` as Subset of TOP-REAL 2;
consider i1 such that
A7: 1 <= i1 and
A8: i1+1 <= len Cage(C,j) and
A9: p in LSeg(Cage(C,j),i1) by A5,SPPOL_2:13;
A10: i1 < len Cage(C,j) by A8,NAT_1:38;
A11: GoB Cage(C,i) = Gauge(C,i) by A1,Th52;
A12: GoB Cage(C,j) = Gauge(C,j) by A1,Th52;
then A13: right_cell(Cage(C,j),i1,Gauge(C,j)) = right_cell(Cage(C,j),i1)
by A7,A8,Th29;
A14: now assume
A15: not right_cell(Cage(C,j),i1) c= Cl LeftComp Cage(C,i);
ex i2,j2 being Nat st
1 <= i2 & i2+1 <= len Gauge(C,i) & 1 <= j2 & j2+1 <= width Gauge(C,i) &
right_cell(Cage(C,j),i1) c= cell(Gauge(C,i),i2,j2)
proof set f = Cage(C,j);
A16: i1 in dom f by A7,A10,FINSEQ_3:27;
then consider i4,j4 being Nat such that
A17: [i4,j4] in Indices Gauge(C,j) and
A18: f/.i1 = (Gauge(C,j))*(i4,j4) by A4,GOBOARD1:def 11;
A19: 1 <= i4 & i4 <= len Gauge(C,j) by A17,GOBOARD5:1;
A20: 1 <= j4 & j4 <= width Gauge(C,j) by A17,GOBOARD5:1;
1 <= i1+1 by NAT_1:29;
then A21: i1+1 in dom f by A8,FINSEQ_3:27;
then consider i5,j5 being Nat such that
A22: [i5,j5] in Indices Gauge(C,j) and
A23: f/.(i1+1) = (Gauge(C,j))*(i5,j5) by A4,GOBOARD1:def 11;
A24: 1 <= i5 & i5 <= len Gauge(C,j) by A22,GOBOARD5:1;
A25: 1 <= j5 & j5 <= width Gauge(C,j) by A22,GOBOARD5:1;
right_cell(f,i1) = right_cell(f,i1);
then A26: i4 = i5 & j4+1 = j5 & right_cell(f,i1) = cell(GoB f,i4,j4)
or
i4+1 = i5 & j4 = j5 & right_cell(f,i1) = cell(GoB f,i4,j4-'1) or
i4 = i5+1 & j4 = j5 & right_cell(f,i1) = cell(GoB f,i5,j5) or
i4 = i5 & j4 = j5+1 & right_cell(f,i1) = cell(GoB f,i4-'1,j5)
by A7,A8,A12,A17,A18,A22,A23,GOBOARD5:def 6;
A27: j4+1+1 = j4+(1+1) by XCMPLX_1:1;
A28: i4+1+1 = i4+(1+1) by XCMPLX_1:1;
abs(i4-i5)+abs(j4-j5) = 1 by A4,A16,A17,A18,A21,A22,A23,GOBOARD1:def 11;
then A29: abs(i4-i5)=1 & j4=j5 or abs(j4-j5)=1 & i4=i5 by GOBOARD1:2;
per cases by A29,GOBOARD1:1;
suppose
A30: i4 = i5 & j4+1 = j5;
then i4 < len Gauge(C,j) by A1,A7,A8,A17,A18,A22,A23,JORDAN10:1;
then i4+1 <= len Gauge(C,j) by NAT_1:38;
hence thesis by A2,A12,A19,A20,A25,A26,A27,A30,Th44,REAL_1:69;
suppose
A31: i4+1 = i5 & j4 = j5;
A32: j4-'1+1 = j4 by A20,AMI_5:4;
1 < j4 by A1,A7,A8,A17,A18,A22,A23,A31,JORDAN10:3;
then 1+1 <= j4 by NAT_1:38;
then 1 <= j4-'1 by JORDAN5B:2;
hence thesis by A2,A12,A19,A20,A24,A26,A28,A31,A32,Th44,REAL_1:69;
suppose
A33: i4 = i5+1 & j4 = j5;
then j5 < width Gauge(C,j) by A1,A7,A8,A17,A18,A22,A23,JORDAN10:4;
then j5+1 <= width Gauge(C,j) by NAT_1:38;
hence thesis by A2,A12,A19,A24,A25,A26,A28,A33,Th44,REAL_1:69;
suppose
A34: i4 = i5 & j4 = j5+1;
A35: i4-'1+1 = i4 by A19,AMI_5:4;
1 < i4 by A1,A7,A8,A17,A18,A22,A23,A34,JORDAN10:2;
then 1+1 <= i4 by NAT_1:38;
then 1 <= i4-'1 by JORDAN5B:2;
hence thesis by A2,A12,A19,A20,A25,A26,A27,A34,A35,Th44,REAL_1:69;
end;
then consider i2,j2 being Nat such that
A36: 1 <= i2 & i2+1 <= len Gauge(C,i) and
A37: 1 <= j2 & j2+1 <= width Gauge(C,i) and
A38: right_cell(Cage(C,j),i1) c= cell(Gauge(C,i),i2,j2);
A39: i2< len Gauge(C,i) by A36,NAT_1:38;
A40: j2 < width Gauge(C,i) by A37,NAT_1:38;
A41: not cell(Gauge(C,i),i2,j2) c= Cl LeftComp Cage(C,i) by A15,A38,XBOOLE_1:1
;
Cl LeftComp Cage(C,i) \/ RightComp Cage(C,i)
= L~Cage(C,i) \/ LeftComp Cage(C,i) \/ RightComp Cage(C,i)
by GOBRD14:32
.= L~Cage(C,i) \/ RightComp Cage(C,i) \/ LeftComp Cage(C,i)
by XBOOLE_1:4
.= the carrier of TOP-REAL 2 by GOBRD14:25;
then A42: cell(Gauge(C,i),i2,j2) meets RightComp Cage(C,i) by A41,XBOOLE_1
:73;
cell(Gauge(C,i),i2,j2) = Cl Int cell(Gauge(C,i),i2,j2)
by A39,A40,GOBRD11:35;
then A43: Int cell(Gauge(C,i),i2,j2) meets RightComp Cage(C,i)
by A42,TSEP_1:40;
A44: Int cell(Gauge(C,i),i2,j2) c= (L~Cage(C,i))` by A11,A39,A40,GOBRD12:2;
A45: RightComp Cage(C,i) is_a_component_of (L~Cage(C,i))` by GOBOARD9:def 2;
Int cell(Gauge(C,i),i2,j2) is connected by A39,A40,GOBOARD9:21;
then A46: Int cell(Gauge(C,i),i2,j2) c= RightComp Cage(C,i)
by A43,A44,A45,JORDAN1A:8;
Int right_cell(Cage(C,j),i1) c= Int cell(Gauge(C,i),i2,j2)
by A38,TOPS_1:48;
then Int right_cell(Cage(C,j),i1) c= RightComp Cage(C,i) by A46,XBOOLE_1:1
;
then Cl Int right_cell(Cage(C,j),i1) c= Cl RightComp Cage(C,i)
by PRE_TOPC:49;
then A47: right_cell(Cage(C,j),i1) c= Cl RightComp Cage(C,i)
by A4,A7,A8,A13,JORDAN9:13;
A48: LSeg(Cage(C,j),i1) c= right_cell(Cage(C,j),i1,Gauge(C,j))
by A4,A7,A8,Th28;
right_cell(Cage(C,j),i1,Gauge(C,j)) c= right_cell(Cage(C,j),i1)
by A4,A7,A8,GOBRD13:34;
then LSeg(Cage(C,j),i1) c= right_cell(Cage(C,j),i1) by A48,XBOOLE_1:1;
then LSeg(Cage(C,j),i1) c= Cl RightComp Cage(C,i) by A47,XBOOLE_1:1;
hence contradiction by A6,A9;
end;
A49: C c= RightComp Cage(C,i) by A1,JORDAN10:11;
right_cell(Cage(C,j),i1,Gauge(C,j)) meets C by A1,A7,A8,JORDAN9:33;
then A50: C meets Cl LeftComp Cage(C,i) by A13,A14,XBOOLE_1:63;
A51: Cl LeftComp Cage(C,i) = LeftComp Cage(C,i) \/ L~Cage(C,i)
by GOBRD14:32;
C misses L~Cage(C,i) by A1,JORDAN10:5;
then A52: C meets LeftComp Cage(C,i) by A50,A51,XBOOLE_1:70;
A53: LeftComp Cage(C,i) is_a_component_of D by GOBOARD9:def 1;
D = LeftComp Cage(C,i) \/ RightComp Cage(C,i) by GOBRD12:11;
then RightComp Cage(C,i) c= D by XBOOLE_1:7;
then A54: C c= D by A49,XBOOLE_1:1;
A55: RightComp Cage(C,i) is_a_component_of D by GOBOARD9:def 2;
C meets C;
then C meets RightComp Cage(C,i) by A49,XBOOLE_1:63;
then LeftComp Cage(C,i) = RightComp Cage(C,i) by A1,A52,A53,A54,A55,JORDAN9:3
;
hence contradiction by SPRECT_4:7;
end;
theorem Th55:
C is connected & i <= j implies LeftComp(Cage(C,i)) c= LeftComp(Cage(C,j))
proof assume that
A1: C is connected and
A2: i <= j;
set p = |[E-bound L~Cage(C,i) + 1,0]|;
p`1 = E-bound L~Cage(C,i) + 1 by EUCLID:56;
then A3: p`1 > E-bound (L~Cage(C,i)) by REAL_1:69;
Cage(C,i)/.1 = N-min L~Cage(C,i) by A1,JORDAN9:34;
then A4: p in LeftComp Cage(C,i) by A3,JORDAN2C:119;
i < j or i = j by A2,AXIOMS:21;
then E-bound (L~Cage(C,i)) > E-bound (L~Cage(C,j)) or
E-bound (L~Cage(C,i)) = E-bound (L~Cage(C,j)) by A1,JORDAN1A:88;
then A5: p`1 > E-bound (L~Cage(C,j)) by A3,AXIOMS:22;
Cage(C,j)/.1 = N-min L~Cage(C,j) by A1,JORDAN9:34;
then p in LeftComp Cage(C,j) by A5,JORDAN2C:119;
then A6:LeftComp(Cage(C,i)) meets LeftComp(Cage(C,j)) by A4,XBOOLE_0:3;
A7: LeftComp(Cage(C,j)) is_a_component_of (L~Cage(C,j))` by GOBOARD9:def 1;
A8: L~Cage(C,j) c= Cl RightComp(Cage(C,i)) by A1,A2,Th54;
A9:Cl RightComp Cage(C,i) = (RightComp Cage(C,i)) \/ L~Cage(C,i) by GOBRD14:31;
A10:L~Cage(C,i) misses LeftComp(Cage(C,i)) by SPRECT_3:43;
LeftComp Cage(C,i) misses RightComp Cage(C,i) by GOBRD14:24;
then Cl RightComp(Cage(C,i)) misses LeftComp(Cage(C,i)) by A9,A10,XBOOLE_1:70
;
then L~Cage(C,j) misses LeftComp(Cage(C,i)) by A8,XBOOLE_1:63;
then LeftComp(Cage(C,i)) c= (L~Cage(C,j))` by SUBSET_1:43;
hence LeftComp(Cage(C,i)) c= LeftComp(Cage(C,j)) by A6,A7,JORDAN1A:8;
end;
theorem
C is connected & i <= j implies RightComp(Cage(C,j)) c= RightComp(Cage(C,i))
proof assume that
A1: C is connected and
A2: i <= j;
LeftComp(Cage(C,i)) c= LeftComp(Cage(C,j)) by A1,A2,Th55;
then A3: Cl LeftComp(Cage(C,i)) c= Cl LeftComp(Cage(C,j)) by PRE_TOPC:49;
(Cl LeftComp(Cage(C,i)))` = RightComp(Cage(C,i)) &
(Cl LeftComp(Cage(C,j)))` = RightComp(Cage(C,j)) by Th50;
hence RightComp(Cage(C,j)) c= RightComp(Cage(C,i)) by A3,SUBSET_1:31;
end;
begin :: Preparing the Internal Approximation
definition let C,n;
func X-SpanStart(C,n) -> Nat equals
:Def2: 2|^(n-'1) + 2;
correctness;
end;
theorem
X-SpanStart(C,n) = Center Gauge(C,n)
proof
thus X-SpanStart(C,n) = 2|^(n-'1) + 2 by Def2
.= Center Gauge(C,n) by JORDAN1B:17;
end;
theorem Th58:
2 < X-SpanStart(C,n) & X-SpanStart(C,n) < len Gauge(C,n)
proof
2|^(n-'1) > 0 by HEINE:5;
then 2|^(n-'1) + 2 > 0+2 by REAL_1:53;
hence 2 < X-SpanStart(C,n) by Def2;
A1: len Gauge(C,n) = 2|^n + 3 by JORDAN8:def 1;
A2: X-SpanStart(C,n) = 2|^(n-'1) + 2 by Def2;
n-'1 <= n by JORDAN3:7;
then 2|^(n-'1) <= 2|^n by PCOMPS_2:4;
hence X-SpanStart(C,n) < len Gauge(C,n) by A1,A2,REAL_1:67;
end;
theorem Th59:
1 <= X-SpanStart(C,n)-'1 & X-SpanStart(C,n)-'1 < len Gauge(C,n)
proof
2 < X-SpanStart(C,n) by Th58;
then A1: 1 < X-SpanStart(C,n) by AXIOMS:22;
then X-SpanStart(C,n)-'1+1 = X-SpanStart(C,n) by AMI_5:4;
hence 1 <= X-SpanStart(C,n)-'1 by A1,NAT_1:38;
A2: X-SpanStart(C,n) < len Gauge(C,n) by Th58;
X-SpanStart(C,n)-'1 <= X-SpanStart(C,n) by JORDAN3:7;
hence X-SpanStart(C,n)-'1 < len Gauge(C,n) by A2,AXIOMS:22;
end;
definition let C,n;
pred n is_sufficiently_large_for C means
:Def3: ex j st j < width Gauge(C,n) &
cell(Gauge(C,n),X-SpanStart(C,n)-'1,j) c= BDD C;
end;
theorem
n is_sufficiently_large_for C implies n >= 1
proof assume n is_sufficiently_large_for C;
then consider j such that
A1: j < width Gauge(C,n) and
A2: cell(Gauge(C,n),X-SpanStart(C,n)-'1,j) c= BDD C by Def3;
A3: width Gauge(C,n) = 2|^n + 3 by JORDAN1A:49;
A4: j > 1
proof
A5: X-SpanStart(C,n)-'1 <= len Gauge(C,n) by Th59;
assume
A6: j <= 1;
per cases by A6,CQC_THE1:2;
suppose
A7: j = 0;
0 <= width Gauge(C,n) by NAT_1:18;
then A8: cell(Gauge(C,n),X-SpanStart(C,n)-'1,0) is non empty by A5,JORDAN1A:
45;
cell(Gauge(C,n),X-SpanStart(C,n)-'1,0) c= UBD C by A5,JORDAN1A:70;
then UBD C meets BDD C by A2,A7,A8,XBOOLE_1:68;
hence contradiction by JORDAN2C:28;
suppose
A9: j = 1;
width Gauge(C,n) <> 0 by GOBOARD1:def 5;
then A10: 0+1 <= width Gauge(C,n) by RLVECT_1:99;
then A11: cell(Gauge(C,n),X-SpanStart(C,n)-'1,1) is non empty by A5,JORDAN1A
:45;
A12: cell(Gauge(C,n),X-SpanStart(C,n)-'1,0) c= UBD C by A5,JORDAN1A:70;
set i1 = X-SpanStart(C,n);
A13: C is Bounded by JORDAN2C:73;
A14: i1 < len Gauge(C,n) by Th58;
i1-'1 <= i1 by JORDAN3:7;
then A15: i1-'1 < len Gauge(C,n) by A14,AXIOMS:22;
A16: 0 < width Gauge(C,n) by A10,NAT_1:38;
1 <= i1-'1 by Th59;
then cell(Gauge(C,n),i1-'1,0) /\ cell(Gauge(C,n),i1-'1,0+1)
= LSeg(Gauge(C,n)*(i1-'1,0+1),Gauge(C,n)*(i1-'1+1,0+1))
by A15,A16,GOBOARD5:27;
then A17: cell(Gauge(C,n),i1-'1,0) meets cell(Gauge(C,n),i1-'1,0+1) by
XBOOLE_0:def 7;
ex B being Subset of TOP-REAL 2 st B is_outside_component_of C & B=UBD C
by A13,JORDAN2C:76;
then A18: UBD C is_a_component_of C` by JORDAN2C:def 4;
A19: cell(Gauge(C,n),X-SpanStart(C,n)-'1,1) is connected by A10,A15,JORDAN1A:
46;
BDD C c= C` by JORDAN2C:29;
then cell(Gauge(C,n),X-SpanStart(C,n)-'1,1) c= C` by A2,A9,XBOOLE_1:1;
then cell(Gauge(C,n),X-SpanStart(C,n)-'1,1) c= UBD C by A12,A17,A18,A19,
GOBOARD9:6;
then UBD C meets BDD C by A2,A9,A11,XBOOLE_1:68;
hence contradiction by JORDAN2C:28;
end;
A20: j + 1 < width Gauge(C,n)
proof
A21: X-SpanStart(C,n)-'1 <= len Gauge(C,n) by Th59;
assume j + 1 >= width Gauge(C,n);
then A22: j + 1 > width Gauge(C,n) or
j + 1 = width Gauge(C,n) by AXIOMS:21;
per cases by A1,A22,NAT_1:38;
suppose
A23: j = width Gauge(C,n);
A24: cell(Gauge(C,n),X-SpanStart(C,n)-'1,width Gauge(C,n)) is non empty
by A21,JORDAN1A:45;
cell(Gauge(C,n),X-SpanStart(C,n)-'1,width Gauge(C,n)) c= UBD C by A21,
JORDAN1A:71;
then UBD C meets BDD C by A2,A23,A24,XBOOLE_1:68;
hence contradiction by JORDAN2C:28;
suppose j + 1 = width Gauge(C,n);
then A25: cell(Gauge(C,n),X-SpanStart(C,n)-'1,width Gauge(C,n)-'1) c= BDD C
by A2,BINARITH:39;
width Gauge(C,n)-'1 <= width Gauge(C,n) by JORDAN3:7;
then A26: cell(Gauge(C,n),X-SpanStart(C,n)-'1,width Gauge(C,n)-'1) is non
empty
by A21,JORDAN1A:45;
A27: cell(Gauge(C,n),X-SpanStart(C,n)-'1,width Gauge(C,n)) c= UBD C by A21,
JORDAN1A:71
;
set i1 = X-SpanStart(C,n);
A28: C is Bounded by JORDAN2C:73;
A29: i1 < len Gauge(C,n) by Th58;
width Gauge(C,n) <> 0 by GOBOARD1:def 5;
then A30: 0+1 <= width Gauge(C,n) by RLVECT_1:99;
i1-'1 <= i1 by JORDAN3:7;
then A31: i1-'1 < len Gauge(C,n) by A29,AXIOMS:22;
width Gauge(C,n)-1 < width Gauge(C,n) by INT_1:26;
then A32: width Gauge(C,n)-'1 < width Gauge(C,n) by A30,SCMFSA_7:3;
A33: width Gauge(C,n)-'1+1 = width Gauge(C,n) by A30,AMI_5:4;
1 <= i1-'1 by Th59;
then cell(Gauge(C,n),i1-'1,width Gauge(C,n)) /\
cell(Gauge(C,n),i1-'1,width Gauge(C,n)-'1)
= LSeg(Gauge(C,n)*(i1-'1,width Gauge(C,n)),
Gauge(C,n)*(i1-'1+1,width Gauge(C,n))) by A31,A32,A33,GOBOARD5:27;
then A34: cell(Gauge(C,n),i1-'1,width Gauge(C,n)) meets
cell(Gauge(C,n),i1-'1,width Gauge(C,n)-'1) by XBOOLE_0:def 7;
ex B being Subset of TOP-REAL 2 st B is_outside_component_of C & B=UBD C
by A28,JORDAN2C:76;
then A35: UBD C is_a_component_of C` by JORDAN2C:def 4;
A36: cell(Gauge(C,n),X-SpanStart(C,n)-'1,width Gauge(C,n)-'1) is connected
by A31,A32,JORDAN1A:46;
BDD C c= C` by JORDAN2C:29;
then cell(Gauge(C,n),X-SpanStart(C,n)-'1,width Gauge(C,n)-'1) c= C`
by A25,XBOOLE_1:1;
then cell(Gauge(C,n),X-SpanStart(C,n)-'1,width Gauge(C,n)-'1)
c= UBD C by A27,A34,A35,A36,GOBOARD9:6;
then UBD C meets BDD C by A25,A26,XBOOLE_1:68;
hence contradiction by JORDAN2C:28;
end;
A37: 2|^0 = 1 by NEWTON:9;
assume n < 1;
then A38: n = 0 by RLVECT_1:99;
per cases by A1,A3,A37,A38,CQC_THE1:5;
suppose j= 0 or j=1;
hence thesis by A4;
suppose
A39: j=2;
A40: X-SpanStart(C,0) = 2|^(0-'1) + 2 by Def2
.= 1 + 2 by A37,POLYNOM4:1;
then X-SpanStart(C,0)-'1 = X-SpanStart(C,0)-1 by JORDAN3:1
.= 2 by A40;
hence contradiction by A2,A38,A39,JORDAN1B:19;
suppose j=3 or j=4;
hence thesis by A3,A20,A37,A38;
end;
theorem
for C being compact non vertical non horizontal non empty
Subset of TOP-REAL 2
for n
for f being FinSequence of TOP-REAL 2 st f is_sequence_on Gauge(C,n) &
len f > 1
for i1,j1 being Nat st
left_cell(f,(len f)-'1,Gauge(C,n)) meets C &
[i1,j1] in Indices Gauge(C,n) & f/.((len f) -'1) = Gauge(C,n)*(i1,j1) &
[i1,j1+1] in Indices Gauge(C,n) & f/.len f = Gauge(C,n)*(i1,j1+1)
holds [i1-'1,j1+1] in Indices Gauge(C,n)
proof
let C be compact non vertical non horizontal non empty Subset of TOP-REAL 2;
let n;
set G = Gauge(C,n);
A1: len G = width G by JORDAN8:def 1;
let f be FinSequence of TOP-REAL 2 such that
A2: f is_sequence_on G and
A3: len f > 1;
let i1,j1 being Nat such that
A4: left_cell(f,(len f)-'1,G) meets C and
A5: [i1,j1] in Indices G & f/.((len f) -'1) = G*(i1,j1) and
A6: [i1,j1+1] in Indices G & f/.len f = G*(i1,j1+1);
A7: 1 <= (len f)-'1 by A3,JORDAN3:12;
A8: (len f) -'1 +1 = len f by A3,AMI_5:4;
A9: 1 <= i1 & i1 <= len G & 1 <= j1 & j1 <= width G by A5,GOBOARD5:1;
A10: 1 <= i1 & i1 <= len G & 1 <= j1+1 & j1+1 <= width G by A6,GOBOARD5:1;
i1-'1 <= i1 by GOBOARD9:2;
then A11: i1-'1 <= len G by A9,AXIOMS:22;
now assume i1-'1 < 1;
then i1-'1 = 0 by RLVECT_1:98;
then i1 <= 1 by JORDAN4:1;
then i1 = 1 by A10,AXIOMS:21;
then cell(G,1-'1,j1) meets C by A2,A4,A5,A6,A7,A8,GOBRD13:22;
then cell(G,0,j1) meets C by GOBOARD9:1;
hence contradiction by A1,A9,JORDAN8:21;
end;
hence [i1-'1,j1+1] in Indices G by A10,A11,GOBOARD7:10;
end;
theorem
for C being compact non vertical non horizontal non empty
Subset of TOP-REAL 2
for n
for f being FinSequence of TOP-REAL 2 st f is_sequence_on Gauge(C,n) &
len f > 1
for i1,j1 being Nat st
left_cell(f,(len f)-'1,Gauge(C,n)) meets C &
[i1,j1] in Indices Gauge(C,n) & f/.((len f) -'1) = Gauge(C,n)*(i1,j1) &
[i1+1,j1] in Indices Gauge(C,n) & f/.len f = Gauge(C,n)*(i1+1,j1)
holds [i1+1,j1+1] in Indices Gauge(C,n)
proof
let C be compact non vertical non horizontal non empty Subset of TOP-REAL 2;
let n;
set G = Gauge(C,n);
let f be FinSequence of TOP-REAL 2 such that
A1: f is_sequence_on G and
A2: len f > 1;
A3: len G = width G by JORDAN8:def 1;
let i1,j1 being Nat such that
A4: left_cell(f,(len f)-'1,G) meets C and
A5: [i1,j1] in Indices G & f/.((len f) -'1) = G*(i1,j1) and
A6: [i1+1,j1] in Indices G & f/.len f = G*(i1+1,j1);
A7: 1 <= (len f)-'1 by A2,JORDAN3:12;
A8: (len f) -'1 +1 = len f by A2,AMI_5:4;
A9: 1 <= i1 & i1 <= len G & 1 <= j1 & j1 <= width G by A5,GOBOARD5:1;
A10: 1 <= i1+1 & i1+1 <= len G & 1 <= j1 & j1 <= width G by A6,GOBOARD5:1;
A11: 1 <= j1+1 by NAT_1:29;
now assume j1+1 > len G;
then j1+1 <= (len G)+1 & (len G)+1 <= j1+1
by A3,A10,AXIOMS:24,NAT_1:38;
then j1+1 = (len G)+1 by AXIOMS:21;
then j1 = len G by XCMPLX_1:2;
then cell(G,i1,len G) meets C by A1,A4,A5,A6,A7,A8,GOBRD13:24;
hence contradiction by A9,JORDAN8:18;
end;
hence [i1+1,j1+1] in Indices G by A3,A10,A11,GOBOARD7:10;
end;
theorem
for C being compact non vertical non horizontal non empty
Subset of TOP-REAL 2
for n
for f being FinSequence of TOP-REAL 2 st f is_sequence_on Gauge(C,n) &
len f > 1
for j1,i2 being Nat st
left_cell(f,(len f)-'1,Gauge(C,n)) meets C &
[i2+1,j1] in Indices Gauge(C,n) & f/.((len f) -'1) = Gauge(C,n)*(i2+1,j1) &
[i2,j1] in Indices Gauge(C,n) & f/.len f = Gauge(C,n)*(i2,j1)
holds [i2,j1-'1] in Indices Gauge(C,n)
proof
let C be compact non vertical non horizontal non empty Subset of TOP-REAL 2;
let n;
set G = Gauge(C,n);
let f be FinSequence of TOP-REAL 2 such that
A1: f is_sequence_on G and
A2: len f > 1;
let j1,i2 being Nat such that
A3: left_cell(f,(len f)-'1,G) meets C and
A4: [i2+1,j1] in Indices G & f/.((len f) -'1) = G*(i2+1,j1) and
A5: [i2,j1] in Indices G & f/.len f = G*(i2,j1);
A6: 1 <= (len f)-'1 by A2,JORDAN3:12;
A7: (len f) -'1 +1 = len f by A2,AMI_5:4;
A8: 1 <= i2 & i2 <= len G & 1 <= j1 & j1 <= width G by A5,GOBOARD5:1;
j1-'1 <= j1 by GOBOARD9:2;
then A9: j1-'1 <= width G by A8,AXIOMS:22;
now assume j1-'1 < 1;
then j1-'1 = 0 by RLVECT_1:98;
then j1 <= 1 by JORDAN4:1;
then j1 = 1 by A8,AXIOMS:21;
then cell(G,i2,1-'1) meets C by A1,A3,A4,A5,A6,A7,GOBRD13:26;
then cell(G,i2,0) meets C by GOBOARD9:1;
hence contradiction by A8,JORDAN8:20;
end;
hence [i2,j1-'1] in Indices G by A8,A9,GOBOARD7:10;
end;
theorem
for C being compact non vertical non horizontal non empty
Subset of TOP-REAL 2
for n
for f being FinSequence of TOP-REAL 2 st f is_sequence_on Gauge(C,n) &
len f > 1
for i1,j2 being Nat st
left_cell(f,(len f)-'1,Gauge(C,n)) meets C &
[i1,j2+1] in Indices Gauge(C,n) & f/.((len f) -'1) = Gauge(C,n)*(i1,j2+1) &
[i1,j2] in Indices Gauge(C,n) & f/.len f = Gauge(C,n)*(i1,j2)
holds [i1+1,j2] in Indices Gauge(C,n)
proof
let C be compact non vertical non horizontal non empty Subset of TOP-REAL 2;
let n;
set G = Gauge(C,n);
A1: len G = width G by JORDAN8:def 1;
let f be FinSequence of TOP-REAL 2 such that
A2: f is_sequence_on G and
A3: len f > 1;
let i1,j2 being Nat such that
A4: left_cell(f,(len f)-'1,G) meets C and
A5: [i1,j2+1] in Indices G & f/.((len f) -'1) = G*(i1,j2+1) and
A6: [i1,j2] in Indices G & f/.len f = G*(i1,j2);
A7: 1 <= (len f)-'1 by A3,JORDAN3:12;
A8: (len f) -'1 +1 = len f by A3,AMI_5:4;
A9: 1 <= i1 & i1 <= len G & 1 <= j2 & j2 <= width G by A6,GOBOARD5:1;
A10: 1 <= i1+1 by NAT_1:29;
now assume i1+1 > len G;
then i1+1 <= (len G)+1 & (len G)+1 <= i1+1 by A9,AXIOMS:24,NAT_1:38;
then i1+1 = (len G)+1 by AXIOMS:21;
then i1 = len G by XCMPLX_1:2;
then cell(G,len G,j2) meets C by A2,A4,A5,A6,A7,A8,GOBRD13:28;
hence contradiction by A1,A9,JORDAN8:19;
end;
hence [i1+1,j2] in Indices G by A9,A10,GOBOARD7:10;
end;
theorem
for C being compact non vertical non horizontal non empty
Subset of TOP-REAL 2
for n
for f being FinSequence of TOP-REAL 2 st f is_sequence_on Gauge(C,n) &
len f > 1
for i1,j1 being Nat st
front_left_cell(f,(len f)-'1,Gauge(C,n)) meets C &
[i1,j1] in Indices Gauge(C,n) & f/.((len f) -'1) = Gauge(C,n)*(i1,j1) &
[i1,j1+1] in Indices Gauge(C,n) & f/.len f = Gauge(C,n)*(i1,j1+1)
holds [i1,j1+2] in Indices Gauge(C,n)
proof
let C be compact non vertical non horizontal non empty Subset of TOP-REAL 2;
let n;
set G = Gauge(C,n);
A1: len G = width G by JORDAN8:def 1;
let f be FinSequence of TOP-REAL 2 such that
A2: f is_sequence_on G and
A3: len f > 1;
let i1,j1 being Nat such that
A4: front_left_cell(f,(len f)-'1,G) meets C and
A5: [i1,j1] in Indices G & f/.((len f) -'1) = G*(i1,j1) and
A6: [i1,j1+1] in Indices G & f/.len f = G*(i1,j1+1);
A7: 1 <= (len f)-'1 by A3,JORDAN3:12;
A8: (len f) -'1 +1 = len f by A3,AMI_5:4;
A9: 1 <= i1 & i1 <= len G & 1 <= j1+1 & j1+1 <= width G by A6,GOBOARD5:1;
A10: 1 <= i1+1 & 1 <= j1+1+1 by NAT_1:37;
i1-'1 <= i1 by GOBOARD9:2;
then A11: i1-'1 <= len G by A9,AXIOMS:22;
A12: j1+1+1 = j1+(1+1) by XCMPLX_1:1;
now assume j1+1+1 > len G;
then j1+1+1 <= (len G)+1 & (len G)+1 <= j1+1+1
by A1,A9,AXIOMS:24,NAT_1:38;
then j1+1+1 = (len G)+1 by AXIOMS:21;
then j1+1 = len G by XCMPLX_1:2;
then cell(G,i1-'1,len G) meets C by A2,A4,A5,A6,A7,A8,GOBRD13:35;
hence contradiction by A11,JORDAN8:18;
end;
hence [i1,j1+2] in Indices G by A1,A9,A10,A12,GOBOARD7:10;
end;
theorem
for C being compact non vertical non horizontal non empty
Subset of TOP-REAL 2
for n
for f being FinSequence of TOP-REAL 2 st f is_sequence_on Gauge(C,n) &
len f > 1
for i1,j1 being Nat st
front_left_cell(f,(len f)-'1,Gauge(C,n)) meets C &
[i1,j1] in Indices Gauge(C,n) & f/.((len f) -'1) = Gauge(C,n)*(i1,j1) &
[i1+1,j1] in Indices Gauge(C,n) & f/.len f = Gauge(C,n)*(i1+1,j1)
holds [i1+2,j1] in Indices Gauge(C,n)
proof
let C be compact non vertical non horizontal non empty Subset of TOP-REAL 2;
let n;
set G = Gauge(C,n);
A1: len G = width G by JORDAN8:def 1;
let f be FinSequence of TOP-REAL 2 such that
A2: f is_sequence_on G and
A3: len f > 1;
let i1,j1 being Nat such that
A4: front_left_cell(f,(len f)-'1,G) meets C and
A5: [i1,j1] in Indices G & f/.((len f) -'1) = G*(i1,j1) and
A6: [i1+1,j1] in Indices G & f/.len f = G*(i1+1,j1);
A7: 1 <= (len f)-'1 by A3,JORDAN3:12;
A8: (len f) -'1 +1 = len f by A3,AMI_5:4;
A9: 1 <= i1+1 & i1+1 <= len G & 1 <= j1 & j1 <= width G by A6,GOBOARD5:1;
A10: 1 <= i1+1+1 & 1 <= j1+1 by NAT_1:37;
A11: i1+1+1 = i1 +(1+1) by XCMPLX_1:1;
now assume i1+1+1 > len G;
then i1+1+1 <= (len G)+1 & (len G)+1 <= i1+1+1
by A9,AXIOMS:24,NAT_1:38;
then i1+1+1 = (len G)+1 by AXIOMS:21;
then i1+1 = len G by XCMPLX_1:2;
then cell(G,len G,j1) meets C by A2,A4,A5,A6,A7,A8,GOBRD13:37;
hence contradiction by A1,A9,JORDAN8:19;
end;
hence [i1+2,j1] in Indices G by A9,A10,A11,GOBOARD7:10;
end;
theorem
for C being compact non vertical non horizontal non empty
Subset of TOP-REAL 2
for n
for f being FinSequence of TOP-REAL 2 st f is_sequence_on Gauge(C,n) &
len f > 1
for j1,i2 being Nat st
front_left_cell(f,(len f)-'1,Gauge(C,n)) meets C &
[i2+1,j1] in Indices Gauge(C,n) & f/.((len f) -'1) = Gauge(C,n)*(i2+1,j1) &
[i2,j1] in Indices Gauge(C,n) & f/.len f = Gauge(C,n)*(i2,j1)
holds [i2-'1,j1] in Indices Gauge(C,n)
proof
let C be compact non vertical non horizontal non empty Subset of TOP-REAL 2;
let n;
set G = Gauge(C,n);
A1: len G = width G by JORDAN8:def 1;
let f be FinSequence of TOP-REAL 2 such that
A2: f is_sequence_on G and
A3: len f > 1;
let j1,i2 being Nat such that
A4: front_left_cell(f,(len f)-'1,G) meets C and
A5: [i2+1,j1] in Indices G & f/.((len f) -'1) = G*(i2+1,j1) and
A6: [i2,j1] in Indices G & f/.len f = G*(i2,j1);
A7: 1 <= (len f)-'1 by A3,JORDAN3:12;
A8: (len f) -'1 +1 = len f by A3,AMI_5:4;
A9: 1 <= i2 & i2 <= len G & 1 <= j1 & j1 <= width G by A6,GOBOARD5:1;
then A10: i2-'1 <= len G & j1-'1 <= width G by JORDAN3:7;
now assume i2-'1 < 1;
then i2-'1 = 0 by RLVECT_1:98;
then i2 <= 1 by JORDAN4:1;
then i2 = 1 by A9,AXIOMS:21;
then cell(G,1-'1,j1-'1) meets C by A2,A4,A5,A6,A7,A8,GOBRD13:39;
then cell(G,0,j1-'1) meets C by GOBOARD9:1;
hence contradiction by A1,A10,JORDAN8:21;
end;
hence [i2-'1,j1] in Indices G by A9,A10,GOBOARD7:10;
end;
theorem
for C being compact non vertical non horizontal non empty
Subset of TOP-REAL 2
for n
for f being FinSequence of TOP-REAL 2 st f is_sequence_on Gauge(C,n) &
len f > 1
for i1,j2 being Nat st
front_left_cell(f,(len f)-'1,Gauge(C,n)) meets C &
[i1,j2+1] in Indices Gauge(C,n) & f/.((len f) -'1) = Gauge(C,n)*(i1,j2+1) &
[i1,j2] in Indices Gauge(C,n) & f/.len f = Gauge(C,n)*(i1,j2)
holds [i1,j2-'1] in Indices Gauge(C,n)
proof
let C be compact non vertical non horizontal non empty Subset of TOP-REAL 2;
let n;
set G = Gauge(C,n);
let f be FinSequence of TOP-REAL 2 such that
A1: f is_sequence_on G and
A2: len f > 1;
let i1,j2 being Nat such that
A3: front_left_cell(f,(len f)-'1,G) meets C and
A4: [i1,j2+1] in Indices G & f/.((len f) -'1) = G*(i1,j2+1) and
A5: [i1,j2] in Indices G & f/.len f = G*(i1,j2);
A6: 1 <= (len f)-'1 by A2,JORDAN3:12;
A7: (len f) -'1 +1 = len f by A2,AMI_5:4;
A8: 1 <= i1 & i1 <= len G & 1 <= j2+1 & j2+1 <= width G by A4,GOBOARD5:1;
A9: 1 <= i1 & i1 <= len G & 1 <= j2 & j2 <= width G by A5,GOBOARD5:1;
then A10: i1-'1 <= len G & j2-'1 <= width G by JORDAN3:7;
now assume j2-'1 < 1;
then j2-'1 = 0 by RLVECT_1:98;
then j2 <= 1 by JORDAN4:1;
then j2 = 1 by A9,AXIOMS:21;
then cell(G,i1,1-'1) meets C by A1,A3,A4,A5,A6,A7,GOBRD13:41;
then cell(G,i1,0) meets C by GOBOARD9:1;
hence contradiction by A8,JORDAN8:20;
end;
hence [i1,j2-'1] in Indices G by A9,A10,GOBOARD7:10;
end;
theorem
for C being compact non vertical non horizontal non empty
Subset of TOP-REAL 2
for n
for f being FinSequence of TOP-REAL 2 st f is_sequence_on Gauge(C,n) &
len f > 1
for i1,j1 being Nat st
front_right_cell(f,(len f)-'1,Gauge(C,n)) meets C &
[i1,j1] in Indices Gauge(C,n) & f/.((len f) -'1) = Gauge(C,n)*(i1,j1) &
[i1,j1+1] in Indices Gauge(C,n) & f/.len f = Gauge(C,n)*(i1,j1+1)
holds [i1+1,j1+1] in Indices Gauge(C,n)
proof
let C be compact non vertical non horizontal non empty Subset of TOP-REAL 2;
let n;
set G = Gauge(C,n);
A1: len G = width G by JORDAN8:def 1;
let f be FinSequence of TOP-REAL 2 such that
A2: f is_sequence_on G and
A3: len f > 1;
let i1,j1 being Nat such that
A4: front_right_cell(f,(len f)-'1,G) meets C and
A5: [i1,j1] in Indices G & f/.((len f) -'1) = G*(i1,j1) and
A6: [i1,j1+1] in Indices G & f/.len f = G*(i1,j1+1);
A7: 1 <= (len f)-'1 by A3,JORDAN3:12;
A8: (len f) -'1 +1 = len f by A3,AMI_5:4;
A9: 1 <= i1 & i1 <= len G & 1 <= j1+1 & j1+1 <= width G by A6,GOBOARD5:1;
A10: 1 <= i1+1 by NAT_1:29;
now assume i1+1 > len G;
then i1+1 <= (len G)+1 & (len G)+1 <= i1+1 by A9,AXIOMS:24,NAT_1:38;
then i1+1 = (len G)+1 by AXIOMS:21;
then i1 = len G by XCMPLX_1:2;
then cell(G,len G,j1+1) meets C by A2,A4,A5,A6,A7,A8,GOBRD13:36;
hence contradiction by A1,A9,JORDAN8:19;
end;
hence [i1+1,j1+1] in Indices G by A9,A10,GOBOARD7:10;
end;
theorem
for C being compact non vertical non horizontal non empty
Subset of TOP-REAL 2
for n
for f being FinSequence of TOP-REAL 2 st f is_sequence_on Gauge(C,n) &
len f > 1
for i1,j1 being Nat st
front_right_cell(f,(len f)-'1,Gauge(C,n)) meets C &
[i1,j1] in Indices Gauge(C,n) & f/.((len f) -'1) = Gauge(C,n)*(i1,j1) &
[i1+1,j1] in Indices Gauge(C,n) & f/.len f = Gauge(C,n)*(i1+1,j1)
holds [i1+1,j1-'1] in Indices Gauge(C,n)
proof
let C be compact non vertical non horizontal non empty Subset of TOP-REAL 2;
let n;
set G = Gauge(C,n);
let f be FinSequence of TOP-REAL 2 such that
A1: f is_sequence_on G and
A2: len f > 1;
let i1,j1 being Nat such that
A3: front_right_cell(f,(len f)-'1,G) meets C and
A4: [i1,j1] in Indices G & f/.((len f) -'1) = G*(i1,j1) and
A5: [i1+1,j1] in Indices G & f/.len f = G*(i1+1,j1);
A6: 1 <= (len f)-'1 by A2,JORDAN3:12;
A7: (len f) -'1 +1 = len f by A2,AMI_5:4;
A8: 1 <= i1+1 & i1+1 <= len G & 1 <= j1 & j1 <= width G by A5,GOBOARD5:1;
j1-'1 <= j1 by GOBOARD9:2;
then A9: j1-'1 <= width G by A8,AXIOMS:22;
now assume j1-'1 < 1;
then j1-'1 = 0 by RLVECT_1:98;
then j1 <= 1 by JORDAN4:1;
then j1 = 1 by A8,AXIOMS:21;
then cell(G,i1+1,1-'1) meets C by A1,A3,A4,A5,A6,A7,GOBRD13:38;
then cell(G,i1+1,0) meets C by GOBOARD9:1;
hence contradiction by A8,JORDAN8:20;
end;
hence [i1+1,j1-'1] in Indices G by A8,A9,GOBOARD7:10;
end;
theorem
for C being compact non vertical non horizontal non empty
Subset of TOP-REAL 2
for n
for f being FinSequence of TOP-REAL 2 st f is_sequence_on Gauge(C,n) &
len f > 1
for j1,i2 being Nat st
front_right_cell(f,(len f)-'1,Gauge(C,n)) meets C &
[i2+1,j1] in Indices Gauge(C,n) & f/.((len f) -'1) = Gauge(C,n)*(i2+1,j1) &
[i2,j1] in Indices Gauge(C,n) & f/.len f = Gauge(C,n)*(i2,j1)
holds [i2,j1+1] in Indices Gauge(C,n)
proof
let C be compact non vertical non horizontal non empty Subset of TOP-REAL 2;
let n;
set G = Gauge(C,n);
let f be FinSequence of TOP-REAL 2 such that
A1: f is_sequence_on G and
A2: len f > 1;
let j1,i2 being Nat such that
A3: front_right_cell(f,(len f)-'1,G) meets C and
A4: [i2+1,j1] in Indices G & f/.((len f) -'1) = G*(i2+1,j1) and
A5: [i2,j1] in Indices G & f/.len f = G*(i2,j1);
A6: 1 <= (len f)-'1 by A2,JORDAN3:12;
A7: (len f) -'1 +1 = len f by A2,AMI_5:4;
A8: 1 <= i2 & i2 <= len G & 1 <= j1 & j1 <= width G by A5,GOBOARD5:1;
then A9: i2-'1 <= len G & j1-'1 <= width G by JORDAN3:7;
A10: 1 <= j1+1 by NAT_1:29;
A11: len G = width G by JORDAN8:def 1;
now assume j1+1 > len G;
then j1+1 <= (len G)+1 & (len G)+1 <= j1+1
by A8,A11,AXIOMS:24,NAT_1:38;
then j1+1 = (len G)+1 by AXIOMS:21;
then j1 = len G by XCMPLX_1:2;
then cell(G,i2-'1,len G) meets C by A1,A3,A4,A5,A6,A7,GOBRD13:40;
hence contradiction by A9,JORDAN8:18;
end;
hence [i2,j1+1] in Indices G by A8,A10,A11,GOBOARD7:10;
end;
theorem
for C being compact non vertical non horizontal non empty
Subset of TOP-REAL 2
for n
for f being FinSequence of TOP-REAL 2 st f is_sequence_on Gauge(C,n) &
len f > 1
for i1,j2 being Nat st
front_right_cell(f,(len f)-'1,Gauge(C,n)) meets C &
[i1,j2+1] in Indices Gauge(C,n) & f/.((len f) -'1) = Gauge(C,n)*(i1,j2+1) &
[i1,j2] in Indices Gauge(C,n) & f/.len f = Gauge(C,n)*(i1,j2)
holds [i1-'1,j2] in Indices Gauge(C,n)
proof
let C be compact non vertical non horizontal non empty Subset of TOP-REAL 2;
let n;
set G = Gauge(C,n);
A1: len G = width G by JORDAN8:def 1;
let f be FinSequence of TOP-REAL 2 such that
A2: f is_sequence_on G and
A3: len f > 1;
let i1,j2 being Nat such that
A4: front_right_cell(f,(len f)-'1,G) meets C and
A5: [i1,j2+1] in Indices G & f/.((len f) -'1) = G*(i1,j2+1) and
A6: [i1,j2] in Indices G & f/.len f = G*(i1,j2);
A7: 1 <= (len f)-'1 by A3,JORDAN3:12;
A8: (len f) -'1 +1 = len f by A3,AMI_5:4;
A9: 1 <= i1 & i1 <= len G & 1 <= j2 & j2 <= width G by A6,GOBOARD5:1;
then A10: i1-'1 <= len G & j2-'1 <= width G by JORDAN3:7;
now assume i1-'1 < 1;
then i1-'1 = 0 by RLVECT_1:98;
then i1 <= 1 by JORDAN4:1;
then i1 = 1 by A9,AXIOMS:21;
then cell(G,1-'1,j2-'1) meets C by A2,A4,A5,A6,A7,A8,GOBRD13:42;
then cell(G,0,j2-'1) meets C by GOBOARD9:1;
hence contradiction by A1,A10,JORDAN8:21;
end;
hence [i1-'1,j2] in Indices G by A9,A10,GOBOARD7:10;
end;