:: More on External Approximation of a Continuum
:: by Andrzej Trybulec
::
:: Received October 7, 2001
:: Copyright (c) 2001-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies NUMBERS, SUBSET_1, REAL_1, RCOMP_1, SPPOL_1, EUCLID, GOBOARD1,
PRE_TOPC, SETFAM_1, XBOOLE_0, RELAT_1, FINSEQ_1, TARSKI, FUNCOP_1,
FUNCT_1, FUNCT_6, RLTOPSP1, PCOMPS_1, XXREAL_0, CARD_1, METRIC_1,
ARYTM_3, ARYTM_1, FINSEQ_2, COMPLEX1, ZFMISC_1, RELAT_2, PARTFUN1,
ORDERS_1, FINSET_1, PRE_POLY, ORDINAL2, GOBOARD2, NAT_1, MCART_1,
GOBRD13, CARD_3, MATRIX_1, TREES_1, INCSP_1, STRUCT_0, GOBOARD5,
CONNSP_1, TOPREAL1, GOBOARD9, TOPS_1, JORDAN3, RFINSEQ, FINSEQ_5, INT_1,
NEWTON, JORDAN8, PSCOMP_1, JORDAN2C, FINSEQ_6, SPRECT_2, JORDAN9,
JORDAN1H, CONVEX1, XXREAL_2, FUNCT_7;
notations TARSKI, XBOOLE_0, SETFAM_1, ZFMISC_1, SUBSET_1, FINSEQ_6, GOBOARD5,
ORDERS_1, ORDINAL1, CARD_1, NUMBERS, XXREAL_0, XREAL_0, XCMPLX_0,
COMPLEX1, REAL_1, FUNCT_1, NAT_1, INT_1, NAT_D, RELAT_1, RELAT_2,
RELSET_1, PARTFUN1, NEWTON, FINSET_1, FINSEQ_1, SEQM_3, RVSUM_1,
STRUCT_0, FUNCT_6, CARD_3, FUNCOP_1, FINSEQ_2, FINSEQ_5, RFINSEQ,
MATRIX_0, MATRIX_1, SEQ_4, METRIC_1, PRE_TOPC, TOPS_1, COMPTS_1,
CONNSP_1, PCOMPS_1, RLVECT_1, RLTOPSP1, EUCLID, SPRECT_2, TOPREAL1,
GOBOARD1, GOBOARD2, JORDAN2C, SPPOL_1, PSCOMP_1, GOBOARD9, JORDAN8,
GOBRD13, JORDAN9, PRE_POLY;
constructors REAL_1, NEWTON, RFINSEQ, NAT_D, WSIERP_1, TOPS_1, CONNSP_1,
TOPREAL4, GOBOARD2, PSCOMP_1, TRIANG_1, GOBOARD9, SPRECT_1, JORDAN2C,
JORDAN8, GOBRD13, JORDAN9, BINOP_2, RELSET_1, FUNCSDOM, CONVEX1,
PCOMPS_1, SEQ_4, DOMAIN_1;
registrations SETFAM_1, RELAT_1, FUNCT_1, FUNCOP_1, FINSET_1, NUMBERS,
XXREAL_0, XREAL_0, NAT_1, INT_1, MEMBERED, FINSEQ_1, FINSEQ_6, GENEALG1,
STRUCT_0, COMPTS_1, EUCLID, TOPREAL1, GOBOARD1, GOBOARD2, SPPOL_2,
GOBOARD9, WAYBEL_2, SPRECT_1, SPRECT_3, REVROT_1, TOPREAL6, JORDAN8,
MATRIX_0, VALUED_0, RELSET_1, RLTOPSP1, PRE_POLY, SEQM_3, CARD_1,
JORDAN1, JORDAN2C, NEWTON;
requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
definitions TARSKI, RELAT_2, ORDERS_1, RELAT_1, XBOOLE_0, SEQM_3;
equalities XBOOLE_0, EUCLID, VALUED_1, RLTOPSP1, ORDINAL1;
expansions TARSKI, RELAT_2, XBOOLE_0;
theorems JORDAN9, GOBOARD5, TOPREAL1, GOBOARD7, GOBOARD1, SPRECT_2, GOBOARD2,
FINSEQ_4, ORDERS_1, CARD_1, FINSEQ_3, FUNCT_2, GOBRD13, PSCOMP_1,
FINSEQ_1, FUNCT_1, MATRIX_0, RELAT_1, EUCLID, NAT_1, SUBSET_1, GOBRD11,
JORDAN1D, ZFMISC_1, RELSET_1, FUNCT_7, TARSKI, CARD_3, FUNCT_6,
JORDAN8, TOPREAL3, GOBRD14, GOBOARD9, SPRECT_4, GOBRD12, SPPOL_2,
PRE_TOPC, TOPS_1, SPRECT_3, JORDAN1A, TSEP_1, INT_1, NEWTON, JORDAN5B,
JORDAN2C, TOPMETR, RVSUM_1, ABSVALUE, METRIC_1, JORDAN1B, SPRECT_1,
FINSEQ_2, JORDAN10, SPPOL_1, CONNSP_1, REVROT_1, XBOOLE_0, XBOOLE_1,
XREAL_0, PARTIT_2, XCMPLX_1, PARTFUN1, SETFAM_1, XREAL_1, NAT_2,
XXREAL_0, PREPOWER, NAT_D, RLTOPSP1, PRE_POLY, FINSEQ_6, SEQM_3, SEQ_4,
XTUPLE_0, RLVECT_1, RLVECT_4;
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;
registration
let D be non empty with_non-empty_element set;
cluster non empty non-empty for FinSequence of D*;
existence
proof
consider X being non empty set such that
A1: X in D by SETFAM_1:def 10;
A2: rng<*<*X*>*> = {<*X*>} by FINSEQ_1:39;
<*X*> in D* by A1,FUNCT_7:18;
then rng<*<*X*>*> c= D* by A2,ZFMISC_1:31;
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;
end;
end;
registration
let F be non-empty Function-yielding Function;
cluster rngs F -> non-empty;
coherence
proof
now
let n be object;
assume n in dom rngs F;
then n in dom F by FUNCT_6:60;
then (rngs F).n = rng(F.n) & F.n is non empty by FUNCT_1:def 9,FUNCT_6:22
;
hence (rngs F).n is non empty;
end;
hence thesis by FUNCT_1:def 9;
end;
end;
theorem Th1:
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
reconsider x = p, y = q as Point of Euclid 2 by TOPREAL3:8;
let G be Subset of TOP-REAL 2 such that
A2: G is open and
A3: p in G;
A4: the TopStruct of TOP-REAL 2 = TopSpaceMetr Euclid 2 by EUCLID:def 8;
then reconsider P = G as Subset of TopSpaceMetr Euclid 2;
P is open by A2,A4,PRE_TOPC:30;
then consider r being Real such that
A5: r>0 and
A6: Ball(x,r) c= P by A3,TOPMETR:15;
reconsider r as Real;
A7: r/2 > 0 by A5,XREAL_1:139;
set t = min(r/2,dist(x,y)/2), s = t/dist(x,y);
set pp = (1-s)*p+s*q;
reconsider z = pp as Point of Euclid 2 by TOPREAL3:8;
reconsider x9 = x, y9 = y, z9 = z as Element of REAL 2;
reconsider a = x9, b = y9 as Element of 2-tuples_on REAL;
reconsider u = a-b as Element of REAL 2;
A8: 0 < dist(x,y) by A1,METRIC_1:7;
then 0 < dist(x,y)/2 by XREAL_1:139;
then
A9: 0 < t by A7,XXREAL_0:21;
dist(x,z) = |.x9-z9.| by SPPOL_1:5
.= |.a-(1-s)*a-s*b.| by RVSUM_1:39
.= |.1 *a-(1-s)*a-s*b.| by RVSUM_1:52
.= |.1 *a +(-1)*(1-s)*a-s*b.| by RVSUM_1:49
.= |.(1+ (-(1-s)))*a-s*b.| by RVSUM_1:50
.= |.s*a+ (-1)*s*b.| by RVSUM_1:49
.= |.s*a+ s*((-1)*b).| by RVSUM_1:49
.= |.s*(a+ (-1)*b).| by RVSUM_1:51
.= |.s*(a+ -b).|
.= |.s*(a-b).|
.= |.s.|*|.u.| by EUCLID:11
.= s*|.a-b.| by A8,A9,ABSVALUE:def 1
.= s*dist(x,y) by SPPOL_1:5
.= t by A8,XCMPLX_1:87;
then
A10: dist(x,z) <= r/2 by XXREAL_0:17;
r/2 < r/1 by A5,XREAL_1:76;
then dist(x,z) < r by A10,XXREAL_0:2;
then
A11: z in Ball(x,r) by METRIC_1:11;
A12: (1-s)*p+s*p = (1-s+s)*p by RLVECT_1:def 6
.= p by RLVECT_1:def 8;
t <= dist(x,y)/2 & dist(x,y)/2 < dist(x,y)/1 by A8,XREAL_1:76,XXREAL_0:17;
then
A13: t < dist(x,y) by XXREAL_0:2;
then s < 1 by A9,XREAL_1:189;
then
A14: pp in LSeg(p,q) by A8,A9;
A15: (1-s)*q+s*q = (1-s+s)*q by RLVECT_1:def 6
.= q by RLVECT_1:def 8;
A16: 1-s <> 0 by A9,A13,XREAL_1:189;
A17: now
assume pp = q;
then (1-s)*q = pp - s*q by A15,RLVECT_4:1
.= (1-s)*p by RLVECT_4:1;
hence contradiction by A1,A16,RLVECT_1:36;
end;
A18: 0 < s by A8,A9,XREAL_1:139;
now
assume pp = p;
then s*p = pp - (1-s)*p by A12,RLVECT_4:1
.= s*q by RLVECT_4:1;
hence contradiction by A1,A18,RLVECT_1:36;
end;
then not pp in {p,q} by A17,TARSKI:def 2;
then pp in LSeg(p,q) \ {p,q} by A14,XBOOLE_0:def 5;
hence thesis by A6,A11,XBOOLE_0:3;
end;
hence thesis by TOPS_1:12;
end;
theorem Th2:
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;
Cl(LSeg(p,q) \ {p,q}) c= Cl LSeg(p,q) by PRE_TOPC:19,XBOOLE_1:36;
hence Cl(LSeg(p,q) \ {p,q}) c= LSeg(p,q) by PRE_TOPC:22;
let e be object;
p in LSeg(p,q) & q in LSeg(p,q) by RLTOPSP1:68;
then {p,q} c= LSeg(p,q) by ZFMISC_1:32;
then
A2: LSeg(p,q) = LSeg(p,q) \ {p,q} \/ {p,q} by XBOOLE_1:45;
assume e in LSeg(p,q);
then
A3: e in LSeg(p,q) \ {p,q} or e in {p,q} by A2,XBOOLE_0:def 3;
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:18;
hence thesis by A4;
end;
suppose
e = p or e = q;
hence thesis by A1,Th1;
end;
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:19;
hence thesis by A1,Th2;
end;
begin :: Transforming Finite Sets to Finite Sequences
definition
func RealOrd -> Relation of REAL equals
{[r,s] : r <= s };
coherence
proof
set R = {[r,s] : r <= s };
R c= [:REAL,REAL:]
proof
let x be object;
assume x in R;
then consider r,s such that
A1: x = [r,s] & r <= s;
r in REAL & s in REAL by XREAL_0:def 1;
hence thesis by A1,ZFMISC_1:87;
end;
hence thesis;
end;
end;
theorem Th4:
[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;
r = r1 by A1,XTUPLE_0:1;
hence r <= s by A1,A2,XTUPLE_0:1;
end;
end;
Lm1: RealOrd is_reflexive_in REAL;
Lm2: RealOrd is_antisymmetric_in REAL
proof
let x,y be object 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,Th4;
hence thesis by XXREAL_0:1;
end;
Lm3: RealOrd is_transitive_in REAL
proof
let x,y,z be object 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,Th4;
then x <= z by XXREAL_0:2;
hence thesis;
end;
Lm4: RealOrd is_connected_in REAL
proof
let x,y be object;
assume x in REAL & y in REAL;
then reconsider x,y as Element of REAL;
x <= y or y <= x;
hence thesis;
end;
theorem Th5:
field RealOrd = REAL
proof
field RealOrd c= REAL \/ REAL by RELSET_1:8;
hence field RealOrd c= REAL;
thus thesis by Lm1,PARTIT_2:8;
end;
registration
cluster RealOrd -> total reflexive antisymmetric transitive
being_linear-order;
coherence
proof
REAL c= dom RealOrd
proof
let x be object;
assume x in REAL;
then reconsider x as Element of REAL;
[x,x] in RealOrd;
hence thesis by XTUPLE_0:def 12;
end;
then dom RealOrd = REAL;
hence RealOrd is total by PARTFUN1:def 2;
thus RealOrd is reflexive by Lm1,Th5;
thus RealOrd is antisymmetric by Lm2,Th5;
thus RealOrd is transitive by Lm3,Th5;
thus RealOrd is_reflexive_in field RealOrd by Th5;
thus RealOrd is_transitive_in field RealOrd by Lm3,Th5;
thus RealOrd is_antisymmetric_in field RealOrd by Lm2,Th5;
thus RealOrd is_connected_in field RealOrd by Lm4,Th5;
end;
end;
theorem Th6:
RealOrd linearly_orders REAL
proof
thus RealOrd is_reflexive_in REAL;
thus RealOrd is_transitive_in REAL by Lm3;
thus RealOrd is_antisymmetric_in REAL by Lm2;
thus thesis by Lm4;
end;
theorem Th7:
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 & m in dom IT and
A2: n<m;
A3: RealOrd linearly_orders A by Th6,ORDERS_1:38;
IT/.n = IT.n & IT/.m = IT.m by A1,PARTFUN1:def 6;
then [IT.n,IT.m] in RealOrd by A1,A2,A3,PRE_POLY:def 2;
then
A4: IT.n <= IT.m by Th4;
IT is one-to-one by Th6,ORDERS_1:38,PRE_POLY:10;
then IT.n <> IT.m by A1,A2,FUNCT_1:def 4;
hence thesis by A4,XXREAL_0:1;
end;
theorem Th8:
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;
reconsider F = SgmX(RealOrd,A) as increasing FinSequence of REAL by Th7;
RealOrd linearly_orders A by Th6,ORDERS_1:38;
then
A2: rng SgmX(RealOrd,A) = rng f by A1,PRE_POLY:def 2;
len F = card rng f by A1,Th6,ORDERS_1:38,PRE_POLY:11;
hence thesis by A2,SEQ_4:def 21;
end;
registration
let A be finite Subset of REAL;
cluster SgmX(RealOrd,A) -> increasing;
coherence by Th7;
end;
theorem Th9:
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;
field R = X & R linearly_orders field R by ORDERS_1:15,37;
hence thesis by ORDERS_1:38,PRE_POLY:11;
end;
begin :: On the construction of go boards
theorem Th10:
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:32;
A1: len X_axis f = len f by GOBOARD1:def 1;
then
A2: dom X_axis f = dom f by FINSEQ_3:29;
A3: 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
A4: k in dom X_axis f;
A5: f/.k = f.k by A2,A4,PARTFUN1:def 6;
thus (X_axis f).k = (f/.k)`1 by A4,GOBOARD1:def 1
.= proj1.(f.k) by A5,PSCOMP_1:def 5
.= pf.k by A2,A4,FUNCT_1:13;
end;
len pf = len f by FINSEQ_2:33;
then dom X_axis f = dom pf by A1,FINSEQ_3:29;
hence thesis by A3,FINSEQ_1:13;
end;
theorem Th11:
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:32;
A1: len Y_axis f = len f by GOBOARD1:def 2;
then
A2: dom Y_axis f = dom f by FINSEQ_3:29;
A3: 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
A4: k in dom Y_axis f;
A5: f/.k = f.k by A2,A4,PARTFUN1:def 6;
thus (Y_axis f).k = (f/.k)`2 by A4,GOBOARD1:def 2
.= proj2.(f.k) by A5,PSCOMP_1:def 6
.= pf.k by A2,A4,FUNCT_1:13;
end;
len pf = len f by FINSEQ_2:33;
then dom Y_axis f = dom pf by A1,FINSEQ_3:29;
hence thesis by A3,FINSEQ_1:13;
end;
definition
let D be non empty set;
let M be FinSequence of D*;
redefine func Values M -> Subset of D; :: redefines Values (MATRIX_0, definition)
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;
end;
then union A c= D by ZFMISC_1:76;
hence thesis by MATRIX_0:35;
end;
end;
registration
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 FUNCT_6:60;
then reconsider
X = rng rngs M as non empty with_non-empty_elements set by RELAT_1:42;
Values M = Union rngs M by MATRIX_0:def 9
.= union X by CARD_3:def 4;
hence thesis;
end;
end;
theorem Th12:
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;
assume k in Seg width M;
then
A1: 1 <= k & k <= width M by FINSEQ_1:1;
let e be object;
assume e in rng Col(M,k);
then consider u being object such that
A2: u in dom Col(M,k) and
A3: e = Col(M,k).u by FUNCT_1:def 3;
reconsider u as Nat by A2;
A4: 1 <= u by A2,FINSEQ_3:25;
A5: len Col(M,k) = len M by MATRIX_0:def 8;
then u <= len M by A2,FINSEQ_3:25;
then
A6: [u,k] in Indices M by A4,A1,MATRIX_0:30;
A7: Values M = { M*(i,j) where i,j is Nat:
[i,j] in Indices M } by MATRIX_0:39;
dom Col(M,k) = dom M by A5,FINSEQ_3:29;
then Col(M,k).u = M*(u,k) by A2,MATRIX_0:def 8;
hence thesis by A7,A3,A6;
end;
theorem Th13:
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;
assume k in dom M;
then
A1: 1 <= k & k <= len M by FINSEQ_3:25;
let e be object;
assume e in rng Line(M,k);
then consider u being object such that
A2: u in dom Line(M,k) and
A3: e = Line(M,k).u by FUNCT_1:def 3;
reconsider u as Nat by A2;
A4: 1 <= u by A2,FINSEQ_3:25;
A5: len Line(M,k) = width M by MATRIX_0:def 7;
then u <= width M by A2,FINSEQ_3:25;
then
A6: [k,u] in Indices M by A1,A4,MATRIX_0:30;
A7: Values M = { M*(i,j) where i,j is Nat: [i,j] in Indices M }
by MATRIX_0:39;
dom Line(M,k) = Seg width M by A5,FINSEQ_1:def 3;
then Line(M,k).u = M*(k,u) by A2,MATRIX_0:def 7;
hence thesis by A7,A3,A6;
end;
theorem Th14:
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 MATRIX_0:def 10;
then 1 <= width G by NAT_1:14;
then
A1: 1 in Seg width G by FINSEQ_1:1;
then reconsider L = X_axis(Col(G,1)) as increasing FinSequence of REAL by
GOBOARD1:def 7;
A2: card rng L= len L by FINSEQ_4:62
.= len Col(G,1) by GOBOARD1:def 1
.= len G by MATRIX_0:def 8;
A3: rng L = rng(proj1*Col(G,1)) by Th10
.= proj1.:rng Col(G,1) by RELAT_1:127;
rng Col(G,1) c= Values G by A1,Th12;
hence thesis by A3,A2,NAT_1:43,RELAT_1:123;
end;
theorem Th15:
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 be Nat st k in dom f holds f.k = F(k) from FINSEQ_1:sch 2;
A3: dom f = dom G by A1,FINSEQ_3:29;
proj1.:Values G c= rng f
proof
let y be object;
A4: Values G = { G*(i,j) where i,j is Nat: [i,j] in Indices G }
by MATRIX_0:39;
assume y in proj1.:Values G;
then consider x being object such that
A5: x in the carrier of TOP-REAL 2 and
A6: x in Values G and
A7: y = proj1.x by FUNCT_2:64;
consider i,j such that
A8: x = G*(i,j) and
A9: [i,j] in Indices G by A6,A4;
reconsider x as Point of TOP-REAL 2 by A5;
A10: 1 <= j & j <= width G by A9,MATRIX_0:32;
A11: 1 <= i & i <= len G by A9,MATRIX_0:32;
then
A12: i in dom G by FINSEQ_3:25;
y = x`1 by A7,PSCOMP_1:def 5
.= G*(i,1)`1 by A8,A11,A10,GOBOARD5:2
.= proj1.(G*(i,1)) by PSCOMP_1:def 5
.= f.i by A2,A3,A12;
hence thesis by A3,A12,FUNCT_1:3;
end;
then Segm card(proj1.:Values G) c= Segm card dom G by A3,CARD_1:12;
then card(proj1.:Values G) <= card dom G by NAT_1:39;
hence thesis by CARD_1:62;
end;
theorem Th16:
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;
len G <= card(proj1.:Values G) & card(proj1.:Values G) <= len G by Th14,Th15;
hence thesis by XXREAL_0:1;
end;
theorem Th17:
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 MATRIX_0:def 10;
then 1 <= len G by NAT_1:14;
then
A1: 1 in dom G by FINSEQ_3:25;
then reconsider L = Y_axis(Line(G,1)) as increasing FinSequence of REAL by
GOBOARD1:def 6;
A2: card rng L= len L by FINSEQ_4:62
.= len Line(G,1) by GOBOARD1:def 2
.= width G by MATRIX_0:def 7;
A3: rng L = rng(proj2*Line(G,1)) by Th11
.= proj2.:rng Line(G,1) by RELAT_1:127;
rng Line(G,1) c= Values G by A1,Th13;
hence thesis by A3,A2,NAT_1:43,RELAT_1:123;
end;
theorem Th18:
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 be Nat st k in dom f holds f.k = F(k) from FINSEQ_1:sch 2;
A3: dom f = Seg width G by A1,FINSEQ_1:def 3;
proj2.:Values G c= rng f
proof
let y be object;
A4: Values G = { G*(i,j) where i,j is Nat: [i,j] in Indices G }
by MATRIX_0:39;
assume y in proj2.:Values G;
then consider x being object such that
A5: x in the carrier of TOP-REAL 2 and
A6: x in Values G and
A7: y = proj2.x by FUNCT_2:64;
consider i,j such that
A8: x = G*(i,j) and
A9: [i,j] in Indices G by A6,A4;
reconsider x as Point of TOP-REAL 2 by A5;
A10: 1 <= i & i <= len G by A9,MATRIX_0:32;
A11: 1 <= j & j <= width G by A9,MATRIX_0:32;
then
A12: j in Seg width G by FINSEQ_1:1;
y = x`2 by A7,PSCOMP_1:def 6
.= G*(1,j)`2 by A8,A11,A10,GOBOARD5:1
.= proj2.(G*(1,j)) by PSCOMP_1:def 6
.= f.j by A2,A3,A12;
hence thesis by A3,A12,FUNCT_1:3;
end;
then Segm card(proj2.:Values G) c= Segm card Seg width G by A3,CARD_1:12;
then card(proj2.:Values G) <= card Seg width G by NAT_1:39;
hence thesis by FINSEQ_1:57;
end;
theorem Th19:
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;
width G <= card(proj2.:Values G) & card(proj2.:Values G) <= width G by Th17
,Th18;
hence thesis by XXREAL_0:1;
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
A2: 1 <= k & k+1 <= len f;
then
A3: k in dom f by SEQ_4:134;
then consider i1,j1 be Nat such that
A4: [i1,j1] in Indices G and
A5: f/.k = G*(i1,j1) by A1,GOBOARD1:def 9;
A6: k+1 in dom f by A2,SEQ_4:134;
then consider i2,j2 be Nat such that
A7: [i2,j2] in Indices G and
A8: f/.(k+1) = G*(i2,j2) by A1,GOBOARD1:def 9;
A9: 1 <= i2 by A7,MATRIX_0:32;
A10: 1 <= j1 by A4,MATRIX_0:32;
left_cell(f,k,G) = left_cell(f,k,G);
then
A11: 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,A4,A5,A7,A8,GOBRD13:def 3;
A12: 1 <= j2 by A7,MATRIX_0:32;
A13: j1 <= width G by A4,MATRIX_0:32;
A14: j2 <= width G by A7,MATRIX_0:32;
A15: i2 <= len G by A7,MATRIX_0:32;
A16: 1 <= i1 by A4,MATRIX_0:32;
|.i1-i2.|+|.j1-j2.| = 1 by A1,A3,A6,A4,A5,A7,A8,GOBOARD1:def 9;
then
A17: |.i1-i2.|=1 & j1=j2 or |.j1-j2.|=1 & i1=i2 by SEQM_3:42;
A18: i1 <= len G by A4,MATRIX_0:32;
per cases by A17,SEQM_3:41;
suppose
A19: i1 = i2 & j1+1 = j2;
then
A20: j1 < width G by A14,NAT_1:13;
A21: i1 -' 1 + 1 = i1 by A16,XREAL_1:235;
then i1-'1 < len G by A18,NAT_1:13;
then LSeg(f/.k,f/.(k+1)) c= cell(G,i1-'1,j1) by A5,A8,A10,A19,A21,A20,
GOBOARD5:18;
hence thesis by A2,A11,A19,TOPREAL1:def 3;
end;
suppose
A22: i1+1 = i2 & j1 = j2;
then i1 < len G by A15,NAT_1:13;
then LSeg(f/.k,f/.(k+1)) c= cell(G,i1,j1) by A5,A8,A16,A10,A13,A22,
GOBOARD5:22;
hence thesis by A2,A11,A22,TOPREAL1:def 3;
end;
suppose
A23: i1 = i2+1 & j1 = j2;
then
A24: i2 < len G by A18,NAT_1:13;
A25: j2 -' 1 + 1 = j2 by A12,XREAL_1:235;
then j2 -' 1 < width G by A14,NAT_1:13;
then LSeg(f/.k,f/.(k+1)) c= cell(G,i2,j2-'1) by A5,A8,A9,A23,A25,A24,
GOBOARD5:21;
hence thesis by A2,A11,A23,TOPREAL1:def 3;
end;
suppose
A26: i1 = i2 & j1 = j2+1;
then j2 < width G by A13,NAT_1:13;
then
LSeg(f/.k,f/.(k+1)) c= left_cell(f,k,G) by A5,A8,A16,A18,A12,A11,A26,
GOBOARD5:19;
hence thesis by A2,TOPREAL1:def 3;
end;
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
1 <= k+1 by NAT_1:11;
then
A4: k+1 in dom f by A2,FINSEQ_3:25;
let i1,j1,i2,j2 be Nat such that
A5: [i1,j1] in Indices G & [i2,j2] in Indices G & f/.k = G*(i1,j1) & f
/.( k+1) = G*(i2,j2);
k < len f by A2,NAT_1:13;
then k in dom f by A1,FINSEQ_3:25;
then |.i1-i2.|+|.j1-j2.| = 1 by A3,A5,A4,GOBOARD1:def 9;
then
A6: |.i1-i2.|=1 & j1=j2 or |.j1-j2.|=1 & i1=i2 by SEQM_3:42;
left_cell(f,k) = left_cell(f,k);
then
A7: 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,A5,GOBOARD5:def 7;
per cases by A6,SEQM_3:41;
case
i1 = i2 & j1+1 = j2;
hence thesis by A7;
end;
case
i1+1 = i2 & j1 = j2;
hence thesis by A7;
end;
case
i1 = i2+1 & j1 = j2;
hence thesis by A7;
end;
case
i1 = i2 & j1 = j2+1;
hence thesis by A7;
end;
end;
hence thesis by A1,A2,A3,GOBRD13:def 3;
end;
theorem Th22:
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
A2: 1 <= k & k+1 <= len f;
then
A3: k in dom f by SEQ_4:134;
then consider i1,j1 be Nat such that
A4: [i1,j1] in Indices G and
A5: f/.k = G*(i1,j1) by A1,GOBOARD1:def 9;
A6: k+1 in dom f by A2,SEQ_4:134;
then consider i2,j2 be Nat such that
A7: [i2,j2] in Indices G and
A8: f/.(k+1) = G*(i2,j2) by A1,GOBOARD1:def 9;
A9: 1 <= i2 by A7,MATRIX_0:32;
A10: 1 <= j1 by A4,MATRIX_0:32;
right_cell(f,k,G) = right_cell(f,k,G);
then
A11: 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,A4,A5,A7,A8,GOBRD13:def 2;
A12: 1 <= j2 by A7,MATRIX_0:32;
A13: j1 <= width G by A4,MATRIX_0:32;
A14: j2 <= width G by A7,MATRIX_0:32;
A15: i2 <= len G by A7,MATRIX_0:32;
A16: 1 <= i1 by A4,MATRIX_0:32;
|.i1-i2.|+|.j1-j2.| = 1 by A1,A3,A6,A4,A5,A7,A8,GOBOARD1:def 9;
then
A17: |.i1-i2.|=1 & j1=j2 or |.j1-j2.|=1 & i1=i2 by SEQM_3:42;
A18: i1 <= len G by A4,MATRIX_0:32;
per cases by A17,SEQM_3:41;
suppose
A19: i1 = i2 & j1+1 = j2;
then j1 < width G by A14,NAT_1:13;
then LSeg(f/.k,f/.(k+1)) c= cell(G,i1,j1) by A5,A8,A16,A18,A10,A19,
GOBOARD5:19;
hence thesis by A2,A11,A19,TOPREAL1:def 3;
end;
suppose
A20: i1+1 = i2 & j1 = j2;
then
A21: i1 < len G by A15,NAT_1:13;
A22: j1 -' 1 + 1 = j1 by A10,XREAL_1:235;
then j1-'1 < width G by A13,NAT_1:13;
then LSeg(f/.k,f/.(k+1)) c= cell(G,i1,j1-'1) by A5,A8,A16,A20,A22,A21,
GOBOARD5:21;
hence thesis by A2,A11,A20,TOPREAL1:def 3;
end;
suppose
A23: i1 = i2+1 & j1 = j2;
then i2 < len G by A18,NAT_1:13;
then LSeg(f/.k,f/.(k+1)) c= cell(G,i2,j2) by A5,A8,A9,A12,A14,A23,
GOBOARD5:22;
hence thesis by A2,A11,A23,TOPREAL1:def 3;
end;
suppose
A24: i1 = i2 & j1 = j2+1;
then
A25: j2 < width G by A13,NAT_1:13;
A26: i1 -' 1 + 1 = i1 by A16,XREAL_1:235;
then i1-'1 < len G by A18,NAT_1:13;
then LSeg(f/.k,f/.(k+1)) c= right_cell(f,k,G) by A5,A8,A12,A11,A24,A26,A25,
GOBOARD5:18;
hence thesis by A2,TOPREAL1:def 3;
end;
end;
theorem Th23:
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
1 <= k+1 by NAT_1:11;
then
A4: k+1 in dom f by A2,FINSEQ_3:25;
set IT = right_cell(f,k);
let i1,j1,i2,j2 be Nat such that
A5: [i1,j1] in Indices G & [i2,j2] in Indices G & f/.k = G*(i1,j1) & f
/.( k+1) = G*(i2,j2);
k < len f by A2,NAT_1:13;
then k in dom f by A1,FINSEQ_3:25;
then |.i1-i2.|+|.j1-j2.| = 1 by A3,A5,A4,GOBOARD1:def 9;
then
A6: |.i1-i2.|=1 & j1=j2 or |.j1-j2.|=1 & i1=i2 by SEQM_3:42;
right_cell(f,k) = right_cell(f,k);
then
A7: 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,A5,GOBOARD5:def 6;
per cases by A6,SEQM_3:41;
case
i1 = i2 & j1+1 = j2;
hence thesis by A7;
end;
case
i1+1 = i2 & j1 = j2;
hence thesis by A7;
end;
case
i1 = i2+1 & j1 = j2;
hence thesis by A7;
end;
case
i1 = i2 & j1 = j2+1;
hence thesis by A7;
end;
end;
hence thesis 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 by CONNSP_1:def 6;
hence thesis by GOBRD14:12;
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;
Int right_cell(f,k,G) misses L~f by A1,A2,JORDAN9:15;
then
A3: Int right_cell(f,k,G) c= right_cell(f,k,G)\L~f by TOPS_1:16,XBOOLE_1:86;
Int left_cell(f,k,G) misses L~f by A1,A2,JORDAN9:15;
then
A4: Int left_cell(f,k,G) c= left_cell(f,k,G)\L~f by TOPS_1:16,XBOOLE_1:86;
right_cell(f,k,G)\L~f c= RightComp f by A1,A2,JORDAN9:27;
hence Int right_cell(f,k,G) c= RightComp f by A3;
left_cell(f,k,G)\L~f c= LeftComp f by A1,A2,JORDAN9:27;
hence thesis by A4;
end;
theorem Th26:
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 by A1,MATRIX_0:32;
A5: j1 <= width G by A1,MATRIX_0:32;
A6: 1 <= j1 by A1,MATRIX_0:32;
A7: 1 <= i2 by A2,MATRIX_0:32;
A8: i1 <= len G by A1,MATRIX_0:32;
A9: i2 <= len G by A2,MATRIX_0:32;
A10: j2 <= width G by A2,MATRIX_0:32;
A11: 1 <= j2 by A2,MATRIX_0:32;
then
A12: G*(i1,j2)`2 = G*(1,j2)`2 by A4,A8,A10,GOBOARD5:1
.= G*(i1,j1)`2 by A3,A7,A9,A11,A10,GOBOARD5:1;
A13: G*(i1,j2)`1 = G*(i1,1)`1 by A4,A8,A11,A10,GOBOARD5:2
.= G*(i1,j1)`1 by A4,A8,A6,A5,GOBOARD5:2;
assume
A14: not thesis;
per cases by A14,XXREAL_0:1;
suppose
i1 < i2;
hence contradiction by A3,A4,A9,A11,A10,A13,GOBOARD5:3;
end;
suppose
i1 > i2;
hence contradiction by A3,A8,A7,A11,A10,A13,GOBOARD5:3;
end;
suppose
j1 < j2;
hence contradiction by A4,A8,A6,A10,A12,GOBOARD5:4;
end;
suppose
j1 > j2;
hence contradiction by A4,A8,A5,A11,A12,GOBOARD5:4;
end;
end;
theorem Th27:
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
A1: f is_sequence_on M;
per cases;
suppose
A2: i1<=i2;
A3: f/^(i1-'1) is_sequence_on M by A1,JORDAN8:2;
mid(f,i1,i2) = (f/^(i1-'1))|(i2-'i1+1) by A2,FINSEQ_6:def 3;
hence thesis by A3,GOBOARD1:22;
end;
suppose
A4: i1 > i2;
f/^(i2-'1) is_sequence_on M by A1,JORDAN8:2;
then
A5: (f/^(i2-'1))|(i1-'i2+1) is_sequence_on M by GOBOARD1:22;
mid(f,i1,i2) = Rev ((f/^(i2-'1))|(i1-'i2+1)) by A4,FINSEQ_6:def 3;
hence thesis by A5,JORDAN9:5;
end;
end;
registration
cluster -> non empty non-empty for Go-board;
coherence
proof
let G be Go-board;
thus G is non empty;
consider n0 being Nat such that
A1: for x being object st x in rng G ex s being FinSequence st s=x & len
s = n0 by MATRIX_0:def 1;
len G <> 0 by MATRIX_0:def 10;
then consider s0 being FinSequence such that
A2: s0 in rng G and
A3: len s0 = width G by MATRIX_0:def 3;
A4: ex s being FinSequence st s=s0 & len s = n0 by A2,A1;
assume G is not non-empty;
then consider n being object such that
A5: n in dom G and
A6: G.n is empty by FUNCT_1:def 9;
A7: card(G.n) is empty by A6;
ex s1 being FinSequence st s1 = G.n & len s1 = n0 by A5,A1,FUNCT_1:3;
hence contradiction by A3,A4,A7,MATRIX_0:def 10;
end;
end;
theorem Th28:
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;
assume 1 <= i & i <= len G;
then i in dom G by FINSEQ_3:25;
then
A1: i in Seg len G by FINSEQ_1:def 3;
0 <> width G by MATRIX_0:def 10;
then
A2: 1 <= width G by NAT_1:14;
reconsider A = proj1.:Values G as finite Subset of REAL;
deffunc F(Nat)=In(G*($1,1)`1,REAL);
consider f being FinSequence of REAL such that
A3: len f = len G and
A4: for i be Nat st i in dom f holds f.i = F(i) from FINSEQ_2:sch 1;
A5: dom f = Seg len G by A3,FINSEQ_1:def 3;
A6: rng f = A
proof
A7: Values G = { G*(m,n): [m,n] in Indices G } by MATRIX_0:39;
thus rng f c= A
proof
let x be object;
assume
A8: x in rng f;
then reconsider x as Element of REAL;
consider y being object such that
A9: y in dom f and
A10: x = f.y by A8,FUNCT_1:def 3;
reconsider y as Nat by A9;
1 <= y & y <= len G by A3,A9,FINSEQ_3:25;
then [y,1] in Indices G by A2,MATRIX_0:30;
then
A11: G*(y,1) in Values G by A7;
x = F(y) by A4,A9,A10
.= proj1.(G*(y,1)) by PSCOMP_1:def 5;
hence thesis by A11,FUNCT_2:35;
end;
let x be object;
assume
A12: x in A;
then reconsider x as Element of REAL;
consider p being Element of TOP-REAL 2 such that
A13: p in Values G and
A14: x = proj1.p by A12,FUNCT_2:65;
consider m,n such that
A15: p = G*(m,n) and
A16: [m,n] in Indices G by A7,A13;
A17: 1 <= n & n <= width G by A16,MATRIX_0:32;
A18: 1 <= m & m <= len G by A16,MATRIX_0:32;
then
A19: m in Seg len G by FINSEQ_1:1;
A20: m in dom f by A3,A18,FINSEQ_3:25;
x = p`1 by A14,PSCOMP_1:def 5
.= F(m) by A15,A17,A18,GOBOARD5:2
.= f.m by A4,A5,A19;
hence thesis by A20,FUNCT_1:def 3;
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
A21: n in dom f & m in dom f and
A22: n < m;
A23: 1 <= n & m <= len G by A3,A21,FINSEQ_3:25;
reconsider n9=n,m9=m as Nat;
A24: f/.n = f.n & f/.m = f.m by A21,PARTFUN1:def 6;
A25: f.n = F(n9) & f.m = F(m9) by A4,A21;
hence f/.n <> f/.m by A2,A22,A23,A24,GOBOARD5:3;
f.n9 < f.m9 by A2,A22,A25,A23,GOBOARD5:3;
hence thesis by A24;
end;
then f = SgmX(RealOrd, proj1.:Values G) by A6,PRE_POLY:9;
then SgmX(RealOrd, proj1.:Values G).i = F(i) by A4,A5,A1;
hence thesis;
end;
theorem Th29:
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;
assume 1 <= j & j <= width G;
then
A1: j in Seg width G by FINSEQ_1:1;
A2: 1 <= len G by NAT_1:14;
reconsider A = proj2.:Values G as finite Subset of REAL;
deffunc F(Nat)=In(G*(1,$1)`2,REAL);
consider f being FinSequence of REAL such that
A3: len f = width G and
A4: for i be Nat st i in dom f holds f.i = F(i) from FINSEQ_2:sch 1;
A5: dom f = Seg width G by A3,FINSEQ_1:def 3;
A6: rng f = A
proof
A7: Values G = { G*(m,n): [m,n] in Indices G } by MATRIX_0:39;
thus rng f c= A
proof
let x be object;
assume
A8: x in rng f;
then reconsider x as Element of REAL;
consider y being object such that
A9: y in dom f and
A10: x = f.y by A8,FUNCT_1:def 3;
reconsider y as Nat by A9;
1 <= y & y <= width G by A3,A9,FINSEQ_3:25;
then [1,y] in Indices G by A2,MATRIX_0:30;
then
A11: G*(1,y) in Values G by A7;
x = F(y) by A4,A9,A10
.= proj2.(G*(1,y)) by PSCOMP_1:def 6;
hence thesis by A11,FUNCT_2:35;
end;
let x be object;
assume
A12: x in A;
then reconsider x as Element of REAL;
consider p being Element of TOP-REAL 2 such that
A13: p in Values G and
A14: x = proj2.p by A12,FUNCT_2:65;
consider m,n such that
A15: p = G*(m,n) and
A16: [m,n] in Indices G by A7,A13;
A17: 1 <= m & m <= len G by A16,MATRIX_0:32;
A18: 1 <= n & n <= width G by A16,MATRIX_0:32;
then
A19: n in Seg width G by FINSEQ_1:1;
A20: n in dom f by A3,A18,FINSEQ_3:25;
x = p`2 by A14,PSCOMP_1:def 6
.= F(n) by A15,A17,A18,GOBOARD5:1
.= f.n by A4,A5,A19;
hence thesis by A20,FUNCT_1:def 3;
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
A21: n in dom f & m in dom f and
A22: n < m;
A23: 1 <= n & m <= width G by A3,A21,FINSEQ_3:25;
reconsider n9=n,m9=m as Nat;
A24: f/.n = f.n & f/.m = f.m by A21,PARTFUN1:def 6;
A25: f.n = F(n9) & f.m = F(m9) by A4,A21;
hence f/.n <> f/.m by A2,A22,A23,A24,GOBOARD5:4;
f.n9 < f.m9 by A2,A22,A25,A23,GOBOARD5:4;
hence thesis by A24;
end;
then f = SgmX(RealOrd, proj2.:Values G) by A6,PRE_POLY:9;
then SgmX(RealOrd, proj2.:Values G).j = F(j) by A4,A5,A1;
hence thesis;
end;
theorem Th30:
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;
consider k1 being object such that
A4: k1 in dom f and
A5: G*(1,i1) = f.k1 by A3,FUNCT_1:def 3;
reconsider k1 as Nat by A4;
A6: 1 <= k1 by A4,FINSEQ_3:25;
given i2 being Nat such that
A7: [len G,i2] in Indices G and
A8: G*(len G,i2) in rng f;
consider k2 being object such that
A9: k2 in dom f and
A10: G*(len G,i2) = f.k2 by A8,FUNCT_1:def 3;
reconsider k2 as Nat by A9;
A11: k2 <= len f by A9,FINSEQ_3:25;
A12: k1 <= len f by A4,FINSEQ_3:25;
set g = mid(f,k1,k2);
A13: g is_sequence_on G by A1,Th27;
A14: 1 <= k2 by A9,FINSEQ_3:25;
A15: now
per cases;
suppose
k1 <= k2;
then len g = k2-'k1+1 by A6,A11,FINSEQ_6:186;
hence len g >= 0 qua Nat+1 by XREAL_1:6;
end;
suppose
k1 > k2;
then len g=k1-'k2+1 by A12,A14,FINSEQ_6:187;
hence len g >= 0 qua Nat+1 by XREAL_1:6;
end;
end;
A16: Values G = { G*(i,j) where i,j is Nat: [i,j] in Indices G }
by MATRIX_0:39;
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;
consider p being Element of TOP-REAL 2 such that
A20: p in Values G and
A21: x = proj1.p by A18,FUNCT_2:65;
consider i0,j0 being Nat such that
A22: p = G*(i0,j0) and
A23: [i0,j0] in Indices G by A16,A20;
A24: i0 <= len G by A23,MATRIX_0:32;
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;
A25: 1 <= i0 by A23,MATRIX_0:32;
A26: 1 <= j0 & j0 <= width G by A23,MATRIX_0:32;
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 and
A30: n+1 <= len g;
let i,j such that
A31: [i,j] in Indices G and
A32: G*(i,j) = g.(n+1);
A33: now
A34: n+1 in dom g by A29,A30,FINSEQ_3:25;
then
A35: G*(i,j) = g/.(n+1) by A32,PARTFUN1:def 6;
then
A36: dom proj1 = the carrier of TOP-REAL 2 & g/.(n+1) in rng g by A32,A34,
FUNCT_1:3,FUNCT_2:def 1;
A37: 1 <= j & j <= width G by A31,MATRIX_0:32;
assume
A38: i = i0;
x = p`1 by A21,PSCOMP_1:def 5
.= G*(i0,1)`1 by A22,A25,A24,A26,GOBOARD5:2
.= G*(i,j)`1 by A25,A24,A38,A37,GOBOARD5:2
.= proj1.(g/.(n+1)) by A35,PSCOMP_1:def 5;
hence contradiction by A19,A36,FUNCT_1:def 6;
end;
per cases;
suppose
n = 0;
then G*(i,j) = G*(1,i1) by A5,A6,A12,A14,A11,A32,FINSEQ_6:118;
then i = 1 by A2,A31,Th26;
hence thesis by A25,A33,XXREAL_0:1;
end;
suppose
A39: n <> 0;
then
A40: 1 <= n by NAT_1:14;
A41: n <= n + 1 by NAT_1:11;
then n <= len g by A30,XXREAL_0:2;
then
A42: n in dom g by A40,FINSEQ_3:25;
then consider i1,j1 being Nat such that
A43: [i1,j1] in Indices G & g/.n = G*(i1,j1) by A13,GOBOARD1:def 9;
A44: n+1 in dom g by A29,A30,FINSEQ_3:25;
then g/.(n+1) = G*(i,j) by A32,PARTFUN1:def 6;
then |.i1-i.|+|.j1-j.| = 1 by A13,A31,A42,A43,A44,GOBOARD1:def 9;
then
A45: |.i1-i.|=1 & j1=j or |.j1-j.|=1 & i1=i by SEQM_3:42;
now
g.n = g/.n by A42,PARTFUN1:def 6;
then
A46: i1 < i0 by A28,A30,A39,A41,A43,NAT_1:14,XXREAL_0:2;
per cases by A45,SEQM_3:41;
suppose
i1 = i or i < i1;
hence thesis by A46,XXREAL_0:2;
end;
suppose
i = i1 + 1;
then i <= i0 by A46,NAT_1:13;
hence thesis by A33,XXREAL_0:1;
end;
end;
hence thesis;
end;
end;
A47: G*(len G,i2) = g.len g by A6,A12,A10,A14,A11,FINSEQ_6:189;
A48: P[0];
for n holds P[n] from NAT_1:sch 2(A48,A27);
then len G < i0 by A7,A15,A47;
hence contradiction by A23,MATRIX_0:32;
end;
thus proj1.:rng f c= proj1.:Values G by A1,GOBRD13:8,RELAT_1:123;
proj1.:rng g c= proj1.:rng f by FINSEQ_6:119,RELAT_1:123;
hence thesis by A17;
end;
theorem Th31:
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;
consider k1 being object such that
A4: k1 in dom f and
A5: G*(i1,1) = f.k1 by A3,FUNCT_1:def 3;
reconsider k1 as Nat by A4;
A6: 1 <= k1 by A4,FINSEQ_3:25;
given i2 being Nat such that
A7: [i2,width G] in Indices G and
A8: G*(i2,width G) in rng f;
consider k2 being object such that
A9: k2 in dom f and
A10: G*(i2, width G) = f.k2 by A8,FUNCT_1:def 3;
reconsider k2 as Nat by A9;
A11: k2 <= len f by A9,FINSEQ_3:25;
A12: k1 <= len f by A4,FINSEQ_3:25;
set g = mid(f,k1,k2);
A13: g is_sequence_on G by A1,Th27;
A14: 1 <= k2 by A9,FINSEQ_3:25;
A15: now
per cases;
suppose
k1 <= k2;
then len g = k2-'k1+1 by A6,A11,FINSEQ_6:186;
hence len g >= 0 qua Nat+1 by XREAL_1:6;
end;
suppose
k1 > k2;
then len g=k1-'k2+1 by A12,A14,FINSEQ_6:187;
hence len g >= 0 qua Nat+1 by XREAL_1:6;
end;
end;
A16: Values G = { G*(i,j) where i,j is Nat: [i,j] in Indices G }
by MATRIX_0:39;
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;
consider p being Element of TOP-REAL 2 such that
A20: p in Values G and
A21: x = proj2.p by A18,FUNCT_2:65;
consider i0,j0 being Nat such that
A22: p = G*(i0,j0) and
A23: [i0,j0] in Indices G by A16,A20;
A24: j0 <= width G by A23,MATRIX_0:32;
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;
A25: 1 <= j0 by A23,MATRIX_0:32;
A26: 1 <= i0 & i0 <= len G by A23,MATRIX_0:32;
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 and
A30: n+1 <= len g;
let i,j such that
A31: [i,j] in Indices G and
A32: G*(i,j) = g.(n+1);
A33: now
A34: n+1 in dom g by A29,A30,FINSEQ_3:25;
then
A35: G*(i,j) = g/.(n+1) by A32,PARTFUN1:def 6;
then
A36: dom proj2 = the carrier of TOP-REAL 2 & g/.(n+1) in rng g by A32,A34,
FUNCT_1:3,FUNCT_2:def 1;
A37: 1 <= i & i <= len G by A31,MATRIX_0:32;
assume
A38: j = j0;
x = p`2 by A21,PSCOMP_1:def 6
.= G*(1,j0)`2 by A22,A26,A25,A24,GOBOARD5:1
.= G*(i,j)`2 by A25,A24,A38,A37,GOBOARD5:1
.= proj2.(g/.(n+1)) by A35,PSCOMP_1:def 6;
hence contradiction by A19,A36,FUNCT_1:def 6;
end;
per cases;
suppose
n = 0;
then G*(i,j) = G*(i1,1) by A5,A6,A12,A14,A11,A32,FINSEQ_6:118;
then j = 1 by A2,A31,Th26;
hence thesis by A25,A33,XXREAL_0:1;
end;
suppose
A39: n <> 0;
then
A40: 1 <= n by NAT_1:14;
A41: n <= n + 1 by NAT_1:11;
then n <= len g by A30,XXREAL_0:2;
then
A42: n in dom g by A40,FINSEQ_3:25;
then consider i1,j1 being Nat such that
A43: [i1,j1] in Indices G & g/.n = G*(i1,j1) by A13,GOBOARD1:def 9;
A44: n+1 in dom g by A29,A30,FINSEQ_3:25;
then g/.(n+1) = G*(i,j) by A32,PARTFUN1:def 6;
then |.i1-i.|+|.j1-j.| = 1 by A13,A31,A42,A43,A44,GOBOARD1:def 9;
then
A45: |.i1-i.|=1 & j1=j or |.j1-j.|=1 & i1=i by SEQM_3:42;
now
g.n = g/.n by A42,PARTFUN1:def 6;
then
A46: j1 < j0 by A28,A30,A39,A41,A43,NAT_1:14,XXREAL_0:2;
per cases by A45,SEQM_3:41;
suppose
j1 = j or j < j1;
hence thesis by A46,XXREAL_0:2;
end;
suppose
j = j1 + 1;
then j <= j0 by A46,NAT_1:13;
hence thesis by A33,XXREAL_0:1;
end;
end;
hence thesis;
end;
end;
A47: G*(i2,width G) = g.len g by A6,A12,A10,A14,A11,FINSEQ_6:189;
A48: P[0];
for n holds P[n] from NAT_1:sch 2(A48,A27);
then width G < j0 by A7,A15,A47;
hence contradiction by A23,MATRIX_0:32;
end;
thus proj2.:rng f c= proj2.:Values G by A1,GOBRD13:8,RELAT_1:123;
proj2.:rng g c= proj2.:rng f by FINSEQ_6:119,RELAT_1:123;
hence thesis by A17;
end;
registration
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 FUNCT_6:60
,RELAT_1:38;
Union f is non empty;
hence thesis by MATRIX_0:def 9;
end;
end;
theorem Th32:
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: width G = card(proj2.:Values G) by Th19
.= len v2 by Th9;
A2: 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 MATRIX_0:32;
A5: 1 <= m & m <= width G by A3,MATRIX_0:32;
v1.n = G*(n,1)`1 by A4,Th28;
then
A6: v1.n = G*(n,m)`1 by A4,A5,GOBOARD5:2;
v2.m = G*(1,m)`2 by A5,Th29;
then v2.m = G*(n,m)`2 by A4,A5,GOBOARD5:1;
hence thesis by A6,EUCLID:53;
end;
len G = card(proj1.:Values G) by Th16
.= len v1 by Th9;
hence thesis by A1,A2,GOBOARD2:def 1;
end;
theorem Th33:
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;
X_axis f = proj1*f by Th10;
then rng X_axis f = proj1.:rng f by RELAT_1:127;
then
A1: Incr X_axis f = SgmX(RealOrd, proj1.:rng f) by Th8;
Y_axis f = proj2*f by Th11;
then rng Y_axis f = proj2.:rng f by RELAT_1:127;
then
A2: Incr Y_axis f = SgmX(RealOrd, proj2.:rng f) by Th8;
assume proj1.:rng f = proj1.:Values G & proj2.:rng f = proj2.:Values G;
hence G = GoB(Incr X_axis f, Incr Y_axis f) by A1,A2,Th32
.= GoB f by GOBOARD2:def 2;
end;
theorem Th34:
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 & G*(1,i1) in rng f;
given i2 being Nat such that
A3: [i2,1] in Indices G & G*(i2,1) in rng f;
given i3 being Nat such that
A4: [len G,i3] in Indices G & G*(len G,i3) in rng f;
given i4 being Nat such that
A5: [i4,width G] in Indices G & G*(i4,width G) in rng f;
A6: proj2.:rng f = proj2.:Values G by A1,A3,A5,Th31;
proj1.:rng f = proj1.:Values G by A1,A2,A4,Th30;
hence thesis by A6,Th33;
end;
begin :: More about gauges
theorem Th35:
1 <= i implies [\ (i-2)/2|^(n-'m)+2 /] is Element of NAT
proof
set i1 = [\ (i-2)/2|^(n-'m)+2 /];
(i-2)/2|^(n-'m)+2-1 = (i-2)/2|^(n-'m)+(2-1);
then
A1: (i-2)/2|^(n-'m)+1 < i1 by INT_1:def 6;
n -' m + 1 >= 0 qua Nat + 1 & n-'m +1 <= 2|^(n-'m) by NEWTON:85,XREAL_1:6;
then 0 qua Nat + 1 <= 2|^(n-'m) by XXREAL_0:2;
then
A2: (-1)/1 <= (-1)/2|^(n-'m) by XREAL_1:120;
assume 1 <= i;
then 1-2 <= i-2 by XREAL_1:9;
then (-1)/2|^(n-'m) <= (i-2)/2|^(n-'m) by XREAL_1:72;
then -1 <= (i-2)/2|^(n-'m) by A2,XXREAL_0:2;
then -1 + 1 <= (i-2)/2|^(n-'m) + 1 by XREAL_1:6;
hence thesis by A1,INT_1:3;
end;
theorem Th36:
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 and
A3: i+1 <= len Gauge(C,n);
A4: n-'m +1 <= 2|^(n-'m) by NEWTON:85;
i+1 <= 2|^n+ (2+1) by A3,JORDAN8:def 1;
then i+1 <= 2|^n+ 2+1;
then i <= 2|^n+ 2 by XREAL_1:6;
then i-2 <= 2|^n by XREAL_1:20;
then (i-2) <= 2|^(m+(n-'m)) by A1,XREAL_1:235;
then (i-2)*1 <= 2|^m*2|^(n-'m) by NEWTON:8;
then (i-2)/2|^(n-'m) <= 2|^m/1 by A4,XREAL_1:102;
then (i-2)/2|^(n-'m) + 3 <= 2|^m + 3 by XREAL_1:6;
then
A5: (i-2)/2|^(n-'m) + 3 <= len Gauge(C,m) by JORDAN8:def 1;
set i1 = [\ (i-2)/2|^(n-'m)+2 /];
(i-2)/2|^(n-'m)+2-1 = (i-2)/2|^(n-'m)+(2-1);
then
A6: (i-2)/2|^(n-'m)+1 < i1 by INT_1:def 6;
n -' m + 1 >= 0 qua Nat + 1 by XREAL_1:6;
then 0 qua Nat + 1 <= 2|^(n-'m) by A4,XXREAL_0:2;
then
A7: (-1)/1 <= (-1)/2|^(n-'m) by XREAL_1:120;
1-2 <= i-2 by A2,XREAL_1:9;
then (-1)/2|^(n-'m) <= (i-2)/2|^(n-'m) by XREAL_1:72;
then -1 <= (i-2)/2|^(n-'m) by A7,XXREAL_0:2;
then -1 + 1 <= (i-2)/2|^(n-'m) + 1 by XREAL_1:6;
then i1 >= 1+(0 qua Nat) by A6,INT_1:7;
hence 1 <= i1;
i1 <= (i-2)/2|^(n-'m)+2 by INT_1:def 6;
then i1+1 <= (i-2)/2|^(n-'m)+2+1 by XREAL_1:6;
hence thesis by A5,XXREAL_0:2;
end;
theorem Th37:
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 and
A3: i+1 <= len Gauge(C,n) and
A4: 1 <= j and
A5: j+1 <= width Gauge(C,n);
reconsider i1 = [\ (i-2)/2|^(n-'m)+2 /], j1 = [\ (j-2)/2|^(n-'m)+2 /] as
Nat by A2,A4,Th35;
set Gm = Gauge(C,m), Gn = Gauge(C,n);
A6: 2|^(n-'m) >n-'m by NEWTON:86;
take i1,j1;
thus i1 = [\ (i-2)/2|^(n-'m)+2 /];
thus j1 = [\ (j-2)/2|^(n-'m)+2 /];
let e be object;
assume
A7: e in cell(Gauge(C,n),i,j);
then reconsider p = e as Point of TOP-REAL 2;
A8: p`2 <= Gn*(i,j+1)`2 by A2,A3,A4,A5,A7,JORDAN9:17;
i <= len Gn & j <= width Gn by A3,A5,NAT_1:13;
then [i,j] in Indices Gn by A2,A4,MATRIX_0:30;
then
A9: 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
A10: Gn*(i,j)`1 =(W-bound C)+(((E-bound C)-(W-bound C))/(2|^n))*((i-2) / 1)
.= (W-bound C)+((E-bound C)-(W-bound C))/1 *((i-2)/(2|^n)) by XCMPLX_1:85;
A11: Gn*(i,j)`1 <= p`1 by A2,A3,A4,A5,A7,JORDAN9:17;
A12: Gn*(i,j)`2 =(S-bound C)+(((N-bound C)-(S-bound C))/(2|^n))*((j-2)/1) by A9
.= (S-bound C)+(((N-bound C)-(S-bound C))/1)*((j-2)/(2|^n)) by XCMPLX_1:85;
A13: p`1 <= Gn*(i+1,j)`1 by A2,A3,A4,A5,A7,JORDAN9:17;
(E-bound C) >= (W-bound C)+(0 qua Nat) by SPRECT_1:21;
then
A14: (E-bound C)-(W-bound C) >= 0 by XREAL_1:19;
1 <= j+1 & i <= len Gn by A3,NAT_1:11,13;
then [i,j+1] in Indices Gn by A2,A5,MATRIX_0:30;
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
A15: Gn*(i,j+1)`2 =(S-bound C)+(((N-bound C)-(S-bound C))/(2|^n))*((j+1- 2)/
1)
.= (S-bound C)+(((N-bound C)-(S-bound C))/1)*((j+1-2)/(2|^n)) by
XCMPLX_1:85;
n -' m + 1 >= 0 qua Nat + 1 & n-'m +1 <= 2|^(n-'m) by NEWTON:85,XREAL_1:6;
then 0 qua Nat + 1 <= 2|^(n-'m) by XXREAL_0:2;
then
A16: (-1)/1 <= (-1)/2|^(n-'m) by XREAL_1:120;
A17: Gn*(i,j)`2 <= p`2 by A2,A3,A4,A5,A7,JORDAN9:17;
1 <= i+1 & j <= width Gn by A5,NAT_1:11,13;
then [i+1,j] in Indices Gn by A3,A4,MATRIX_0:30;
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
A18: Gn*(i+1,j)`1 =(W-bound C)+(((E-bound C)-(W-bound C))/(2|^n))*((i+1- 2)/
1)
.= (W-bound C)+(((E-bound C)-(W-bound C))/1)*((i+1-2)/(2|^n)) by
XCMPLX_1:85;
(i-2)/2|^(n-'m)+2-1 = (i-2)/2|^(n-'m)+(2-1);
then
A19: (i-2)/2|^(n-'m)+1 < i1 by INT_1:def 6;
1-2 <= i-2 by A2,XREAL_1:9;
then (-1)/2|^(n-'m) <= (i-2)/2|^(n-'m) by XREAL_1:72;
then -1 <= (i-2)/2|^(n-'m) by A16,XXREAL_0:2;
then -1 + 1 <= (i-2)/2|^(n-'m) + 1 by XREAL_1:6;
then
A20: i1 >= 1+(0 qua Nat) by A19,INT_1:7;
(N-bound C) >= (S-bound C)+(0 qua Nat) by SPRECT_1:22;
then
A21: (N-bound C)-(S-bound C) >= 0 by XREAL_1:19;
(i-2)/2|^(n-'m)+2-1 < i1 by INT_1:def 6;
then (i-2)/2|^(n-'m)+2 < i1+1 by XREAL_1:19;
then (i-2)/2|^(n-'m) < i1+1-2 by XREAL_1:20;
then (i-2) + 1 <= (i1+1-2)*2|^(n-'m) by A6,INT_1:7,XREAL_1:77;
then (i+1-2)/2|^(n-'m) <= i1+1-2 by A6,XREAL_1:79;
then (i+1-2)/2|^(n-'m)/2|^m <= (i1+1-2)/2|^m by XREAL_1:72;
then (i+1-2)/(2|^(n-'m)*2|^m) <= (i1+1-2)/2|^m by XCMPLX_1:78;
then (i+1-2)/2|^(n-'m+m) <= (i1+1-2)/2|^m by NEWTON:8;
then (i+1-2)/2|^n <= (i1+1-2)/2|^m by A1,XREAL_1:235;
then
A22: ((E-bound C)-(W-bound C)) *((i+1-2)/(2|^n)) <= (((E-bound C)-(W-bound C
)))*((i1+1-2)/(2|^m)) by A14,XREAL_1:64;
i1 <= (i-2)/2|^(n-'m)+2 by INT_1:def 6;
then i1-2 <= (i-2)/2|^(n-'m) by XREAL_1:20;
then (i1-2)/2|^m <= (i-2)/2|^(n-'m)/2|^m by XREAL_1:72;
then (i1-2)/2|^m <= (i-2)/(2|^(n-'m)*2|^m) by XCMPLX_1:78;
then (i1-2)/2|^m <= (i-2)/2|^(n-'m+m) by NEWTON:8;
then (i1-2)/2|^m <= (i-2)/2|^n by A1,XREAL_1:235;
then
A23: ((E-bound C)-(W-bound C)) *((i1-2)/(2|^m)) <= (((E-bound C)-(W-bound C)
))*((i-2)/(2|^n)) by A14,XREAL_1:64;
j1 <= (j-2)/2|^(n-'m)+2 by INT_1:def 6;
then j1-2 <= (j-2)/2|^(n-'m) by XREAL_1:20;
then (j1-2)/2|^m <= (j-2)/2|^(n-'m)/2|^m by XREAL_1:72;
then (j1-2)/2|^m <= (j-2)/(2|^(n-'m)*2|^m) by XCMPLX_1:78;
then (j1-2)/2|^m <= (j-2)/2|^(n-'m+m) by NEWTON:8;
then (j1-2)/2|^m <= (j-2)/2|^n by A1,XREAL_1:235;
then
A24: ((N-bound C)-(S-bound C)) *((j1-2)/(2|^m)) <= (((N-bound C)-(S-bound C)
))*((j-2)/(2|^n)) by A21,XREAL_1:64;
(j-2)/2|^(n-'m)+2-1 = (j-2)/2|^(n-'m)+(2-1);
then
A25: (j-2)/2|^(n-'m)+1 < j1 by INT_1:def 6;
1-2 <= j-2 by A4,XREAL_1:9;
then (-1)/2|^(n-'m) <= (j-2)/2|^(n-'m) by XREAL_1:72;
then -1 <= (j-2)/2|^(n-'m) by A16,XXREAL_0:2;
then -1 + 1 <= (j-2)/2|^(n-'m) + 1 by XREAL_1:6;
then
A26: j1 >= 1+(0 qua Nat) by A25,INT_1:7;
(j-2)/2|^(n-'m)+2-1 < j1 by INT_1:def 6;
then (j-2)/2|^(n-'m)+2 < j1+1 by XREAL_1:19;
then (j-2)/2|^(n-'m) < j1+1-2 by XREAL_1:20;
then (j-2) + 1 <= (j1+1-2)*2|^(n-'m) by A6,INT_1:7,XREAL_1:77;
then (j+1-2)/2|^(n-'m) <= j1+1-2 by A6,XREAL_1:79;
then (j+1-2)/2|^(n-'m)/2|^m <= (j1+1-2)/2|^m by XREAL_1:72;
then (j+1-2)/(2|^(n-'m)*2|^m) <= (j1+1-2)/2|^m by XCMPLX_1:78;
then (j+1-2)/2|^(n-'m+m) <= (j1+1-2)/2|^m by NEWTON:8;
then (j+1-2)/2|^n <= (j1+1-2)/2|^m by A1,XREAL_1:235;
then
A27: ((N-bound C)-(S-bound C)) *((j+1-2)/(2|^n)) <= (((N-bound C)-(S-bound
C)))*((j1+1-2)/(2|^m)) by A21,XREAL_1:64;
len Gauge(C,m) = width Gauge(C,m) & len Gauge(C,n) = width Gauge(C,n) by
JORDAN8:def 1;
then
A28: j1+1 <= width Gauge(C,m) by A1,A4,A5,Th36;
then
A29: j1 <= width Gauge(C,m) by NAT_1:13;
A30: i1+1 <= len Gauge(C,m) by A1,A2,A3,Th36;
then 1 <= j1+1 & i1 <= len Gauge(C,m) by NAT_1:11,13;
then [i1,j1+1] in Indices Gm by A20,A28,MATRIX_0:30;
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
Gm*(i1,j1+1)`2 =(S-bound C)+(((N-bound C)-(S-bound C))/(2|^m))*((j1+1-2
)/1)
.= (S-bound C)+(((N-bound C)-(S-bound C))/1)*((j1+1-2)/(2|^m)) by
XCMPLX_1:85;
then Gn*(i,j+1)`2 <= Gm*(i1,j1+1)`2 by A15,A27,XREAL_1:6;
then
A31: p`2 <= Gm*(i1,j1+1)`2 by A8,XXREAL_0:2;
i1 <= len Gauge(C,m) by A30,NAT_1:13;
then [i1,j1] in Indices Gm by A20,A26,A29,MATRIX_0:30;
then
A32: 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
Gm*(i1,j1)`1 =(W-bound C)+(((E-bound C)-(W-bound C))/(2|^m))*((i1 - 2)/
1)
.= (W-bound C)+(((E-bound C)-(W-bound C))/1)*((i1-2)/(2|^m)) by XCMPLX_1:85
;
then Gm*(i1,j1)`1 <= Gn*(i,j)`1 by A10,A23,XREAL_1:6;
then
A33: Gm*(i1,j1)`1 <= p`1 by A11,XXREAL_0:2;
Gm*(i1,j1)`2 =(S-bound C)+(((N-bound C)-(S-bound C))/(2|^m))*((j1-2)/1)
by A32
.= (S-bound C)+(((N-bound C)-(S-bound C))/1)*((j1-2)/(2|^m)) by XCMPLX_1:85
;
then Gm*(i1,j1)`2 <= Gn*(i,j)`2 by A12,A24,XREAL_1:6;
then
A34: Gm*(i1,j1)`2 <= p`2 by A17,XXREAL_0:2;
1 <= i1+1 & j1 <= width Gauge(C,m) by A28,NAT_1:11,13;
then [i1+1,j1] in Indices Gm by A26,A30,MATRIX_0:30;
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
Gm*(i1+1,j1)`1 =(W-bound C)+(((E-bound C)-(W-bound C))/(2|^m))*((i1+1-2
)/1)
.= (W-bound C)+(((E-bound C)-(W-bound C))/1)*((i1+1-2)/(2|^m)) by
XCMPLX_1:85;
then Gn*(i+1,j)`1 <= Gm*(i1+1,j1)`1 by A18,A22,XREAL_1:6;
then p`1 <= Gm*(i1+1,j1)`1 by A13,XXREAL_0:2;
hence thesis by A20,A26,A30,A28,A33,A34,A31,JORDAN9:17;
end;
theorem Th38:
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,Th37;
take i1,j1;
thus 1 <= i1 & i1+1 <= len Gauge(C,m) by A1,A2,A4,Th36;
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,Th36;
thus thesis by A6;
end;
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 UBD P is_outside_component_of P by JORDAN2C:68;
hence thesis by JORDAN2C:def 3;
end;
theorem Th40:
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:36;
then f = Rotate(g,f/.1) by FINSEQ_6:181;
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);
assume not thesis;
then g is not clockwise_oriented by Th40;
then
A2: Rev g is clockwise_oriented by REVROT_1:38;
L~f = L~g by REVROT_1:33;
then UBD L~f = UBD L~Rev g by SPPOL_2:22
.= LeftComp Rev g by A2,GOBRD14:36
.= RightComp g by GOBOARD9:23
.= RightComp f by REVROT_1:37;
hence contradiction by A1,SPRECT_4:6;
end;
begin :: More about cages
theorem Th42:
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))` misses Cl LeftComp(f) by SUBSET_1:24;
Cl LeftComp f \/ RightComp f = L~f \/ LeftComp f \/ RightComp f by GOBRD14:22
.= L~f \/ RightComp f \/ LeftComp f by XBOOLE_1:4
.= the carrier of TOP-REAL 2 by GOBRD14:15;
hence (Cl LeftComp(f))` c= RightComp(f) by A1,XBOOLE_1:73;
A2: RightComp f misses LeftComp f by GOBRD14:14;
Cl LeftComp f = (LeftComp f) \/ L~f & L~f misses RightComp(f) by GOBRD14:22
,SPRECT_3:25;
then Cl LeftComp(f) misses RightComp(f) by A2,XBOOLE_1:70;
hence thesis by SUBSET_1:23;
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))` misses Cl RightComp(f) by SUBSET_1:24;
Cl RightComp f \/ LeftComp f = L~f \/ RightComp f \/ LeftComp f by GOBRD14:21
.= the carrier of TOP-REAL 2 by GOBRD14:15;
hence (Cl RightComp(f))` c= LeftComp(f) by A1,XBOOLE_1:73;
A2: LeftComp f misses RightComp f by GOBRD14:14;
Cl RightComp f = (RightComp f) \/ L~f & L~f misses LeftComp(f) by GOBRD14:21
,SPRECT_3:26;
then Cl RightComp(f) misses LeftComp(f) by A2,XBOOLE_1:70;
hence thesis by SUBSET_1:23;
end;
theorem Th44:
C is connected implies GoB Cage(C,n) = Gauge(C,n)
proof
A1: S-max L~Cage(C,n) in rng Cage(C,n) & E-max L~Cage(C,n) in rng Cage(C,n)
by SPRECT_2:42,46;
assume
A2: C is connected;
then 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 JORDAN1D:30;
A5: N-min L~Cage(C,n) in rng Cage(C,n) & Cage(C,n) is_sequence_on Gauge(C,n
) by A2,JORDAN9:def 1,SPRECT_2:39;
consider ie being Nat such that
A6: 1 <= ie & ie <= width Gauge(C,n) and
A7: Gauge(C,n)*(len Gauge(C,n),ie) = E-max L~Cage(C,n) by A2,JORDAN1D:25;
A8: 1 <= len Gauge(C,n) by GOBRD11:34;
then
A9: [len Gauge(C,n),ie] in Indices Gauge(C,n) by A6,MATRIX_0:30;
consider iS being Nat such that
A10: 1 <= iS & iS <= len Gauge(C,n) and
A11: Gauge(C,n)*(iS,1) = S-max L~Cage(C,n) by A2,JORDAN1D:28;
A12: 1 <= width Gauge(C,n) by GOBRD11:34;
then
A13: [iS,1] in Indices Gauge(C,n) by A10,MATRIX_0:30;
consider IN being Nat such that
A14: 1 <= IN & IN <= len Gauge(C,n) and
A15: Gauge(C,n)*(IN,width Gauge(C,n)) = N-min L~Cage(C,n) by A2,JORDAN1D:21;
A16: [IN,width Gauge(C,n)] in Indices Gauge(C,n) by A12,A14,MATRIX_0:30;
[1,iw] in Indices Gauge(C,n) by A8,A3,MATRIX_0:30;
hence thesis by A4,A11,A13,A7,A9,A1,A15,A16,A5,Th34,SPRECT_2:43;
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 and
A3: i+1 <= len Gauge(C,n) and
A4: Cage(C,n)/.1 = Gauge(C,n)*(i,width Gauge(C,n)) and
A5: Cage(C,n)/.2 = Gauge(C,n)*(i+1,width Gauge(C,n)) and
A6: 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;
A7: 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
0 <> width Gauge(C,n) by MATRIX_0:def 10;
then
A8: 1 <= width Gauge(C,n) by NAT_1:14;
A9: GoB Cage(C,n) = Gauge(C,n) by A1,Th44;
let i1,j1,i2,j2 be Nat such that
A10: [i1,j1] in Indices GoB Cage(C,n) and
A11: [i2,j2] in Indices GoB Cage(C,n) and
A12: Cage(C,n)/.1 = (GoB Cage(C,n))*(i1,j1) and
A13: Cage(C,n)/.(1+1) = (GoB Cage(C,n))*(i2,j2);
1 <= i+1 by NAT_1:11;
then
A14: [i+1,width Gauge(C,n)] in Indices Gauge(C,n) by A3,A8,MATRIX_0:30;
then
A15: i2 = i+1 by A5,A11,A13,A9,GOBOARD1:5;
i < len Gauge(C,n) by A3,NAT_1:13;
then
A16: [i,width Gauge(C,n)] in Indices Gauge(C,n) by A2,A8,MATRIX_0:30;
then
A17: i1 = i by A4,A10,A12,A9,GOBOARD1:5;
A18: j2 = width Gauge(C,n) by A5,A11,A13,A9,A14,GOBOARD1:5;
per cases by A4,A10,A12,A9,A16,A15,A18,GOBOARD1:5;
case
i1 = i2 & j1+1 = j2;
hence thesis by A17,A15;
end;
case
i1+1 = i2 & j1 = j2;
thus thesis by A4,A10,A12,A9,A16,A17,GOBOARD1:5;
end;
case
i1 = i2+1 & j1 = j2;
hence thesis by A17,A15;
end;
case
i1 = i2 & j1 = j2+1;
hence thesis by A17,A15;
end;
end;
1+1 <= len Cage(C,n) by GOBOARD7:34,XXREAL_0:2;
hence thesis by A6,A7,GOBOARD5:def 6;
end;
theorem Th46:
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;
A5: GoB Cage(C,i) = Gauge(C,i) by A1,Th44;
consider p being Point of TOP-REAL 2 such that
A6: p in L~Cage(C,j) and
A7: not p in Cl RightComp(Cage(C,i)) by A3;
consider i1 such that
A8: 1 <= i1 and
A9: i1+1 <= len Cage(C,j) and
A10: p in LSeg(Cage(C,j),i1) by A6,SPPOL_2:13;
A11: GoB Cage(C,j) = Gauge(C,j) by A1,Th44;
then
A12: right_cell(Cage(C,j),i1,Gauge(C,j)) = right_cell(Cage(C,j),i1) by A8,A9
,Th23;
A13: i1 < len Cage(C,j) by A9,NAT_1:13;
now
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);
A14: i1 in dom f by A8,A13,FINSEQ_3:25;
then consider i4,j4 being Nat such that
A15: [i4,j4] in Indices Gauge(C,j) and
A16: f/.i1 = (Gauge(C,j))*(i4,j4) by A4,GOBOARD1:def 9;
A17: 1 <= i4 by A15,MATRIX_0:32;
A18: j4 <= width Gauge(C,j) by A15,MATRIX_0:32;
A19: 1 <= j4 by A15,MATRIX_0:32;
A20: i4 <= len Gauge(C,j) by A15,MATRIX_0:32;
1 <= i1+1 by NAT_1:11;
then
A21: i1+1 in dom f by A9,FINSEQ_3:25;
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 9;
A24: 1 <= i5 by A22,MATRIX_0:32;
right_cell(f,i1) = right_cell(f,i1);
then
A25: 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 A8,A9,A11,A15,A16,A22,A23,GOBOARD5:def 6;
|.i4-i5.|+|.j4-j5.| = 1 by A4,A14,A15,A16,A21,A22,A23,GOBOARD1:def 9;
then
A26: |.i4-i5.|=1 & j4=j5 or |.j4-j5.|=1 & i4=i5 by SEQM_3:42;
A27: j5 <= width Gauge(C,j) by A22,MATRIX_0:32;
A28: i5 <= len Gauge(C,j) by A22,MATRIX_0:32;
A29: 1 <= j5 by A22,MATRIX_0:32;
per cases by A26,SEQM_3:41;
suppose
A30: i4 = i5 & j4+1 = j5;
then i4 < len Gauge(C,j) by A1,A8,A9,A15,A16,A22,A23,JORDAN10:1;
then i4+1 <= len Gauge(C,j) by NAT_1:13;
hence thesis by A2,A11,A17,A19,A27,A25,A30,Th38;
end;
suppose
A31: i4+1 = i5 & j4 = j5;
then 1 < j4 by A1,A8,A9,A15,A16,A22,A23,JORDAN10:3;
then 1+1 <= j4 by NAT_1:13;
then
A32: 1 <= j4-'1 by JORDAN5B:2;
j4-'1+1 = j4 by A19,XREAL_1:235;
hence thesis by A2,A11,A17,A18,A28,A25,A31,A32,Th38;
end;
suppose
A33: i4 = i5+1 & j4 = j5;
then j5 < width Gauge(C,j) by A1,A8,A9,A15,A16,A22,A23,JORDAN10:4;
then j5+1 <= width Gauge(C,j) by NAT_1:13;
hence thesis by A2,A11,A20,A24,A29,A25,A33,Th38;
end;
suppose
A34: i4 = i5 & j4 = j5+1;
then 1 < i4 by A1,A8,A9,A15,A16,A22,A23,JORDAN10:2;
then 1+1 <= i4 by NAT_1:13;
then
A35: 1 <= i4-'1 by JORDAN5B:2;
i4-'1+1 = i4 by A17,XREAL_1:235;
hence thesis by A2,A11,A20,A18,A29,A25,A34,A35,Th38;
end;
end;
then consider i2,j2 being Nat such that
1 <= i2 and
A36: i2+1 <= len Gauge(C,i) and
1 <= j2 and
A37: j2+1 <= width Gauge(C,i) and
A38: right_cell(Cage(C,j),i1) c= cell(Gauge(C,i),i2,j2);
A39: Int right_cell(Cage(C,j),i1) c= Int cell(Gauge(C,i),i2,j2) by A38,
TOPS_1:19;
A40: RightComp Cage(C,i) is_a_component_of (L~Cage(C,i))` by GOBOARD9:def 2;
A41: Cl LeftComp Cage(C,i) \/ RightComp Cage(C,i) = L~Cage(C,i) \/
LeftComp Cage(C,i) \/ RightComp Cage(C,i) by GOBRD14:22
.= L~Cage(C,i) \/ RightComp Cage(C,i) \/ LeftComp Cage(C,i) by XBOOLE_1:4
.= the carrier of TOP-REAL 2 by GOBRD14:15;
assume not right_cell(Cage(C,j),i1) c= Cl LeftComp Cage(C,i);
then not cell(Gauge(C,i),i2,j2) c= Cl LeftComp Cage(C,i) by A38;
then
A42: cell(Gauge(C,i),i2,j2) meets RightComp Cage(C,i) by A41,XBOOLE_1:73;
A43: i2< len Gauge(C,i) & j2 < width Gauge(C,i) by A36,A37,NAT_1:13;
then cell(Gauge(C,i),i2,j2) = Cl Int cell(Gauge(C,i),i2,j2) by GOBRD11:35;
then
A44: Int cell(Gauge(C,i),i2,j2) meets RightComp Cage(C,i) by A42,TSEP_1:36;
A45: Int cell(Gauge(C,i),i2,j2) is convex
by A43,GOBOARD9:17;
Int cell(Gauge(C,i),i2,j2) c= (L~Cage(C,i))` by A5,A43,GOBRD12:1;
then Int cell(Gauge(C,i),i2,j2) c= RightComp Cage(C,i)
by A44,A40,A45,GOBOARD9:4;
then Int right_cell(Cage(C,j),i1) c= RightComp Cage(C,i) by A39;
then Cl Int right_cell(Cage(C,j),i1) c= Cl RightComp Cage(C,i) by
PRE_TOPC:19;
then
A46: right_cell(Cage(C,j),i1) c= Cl RightComp Cage(C,i) by A4,A8,A9,A12,
JORDAN9:11;
LSeg(Cage(C,j),i1) c= right_cell(Cage(C,j),i1,Gauge(C,j)) &
right_cell(Cage( C,j),i1,Gauge(C,j)) c= right_cell(Cage(C,j),i1) by A4,A8,A9
,Th22,GOBRD13:33;
then LSeg(Cage(C,j),i1) c= right_cell(Cage(C,j),i1);
then LSeg(Cage(C,j),i1) c= Cl RightComp Cage(C,i) by A46;
hence contradiction by A7,A10;
end;
then
A47: C meets Cl LeftComp Cage(C,i) by A1,A8,A9,A12,JORDAN9:31,XBOOLE_1:63;
Cl LeftComp Cage(C,i) = LeftComp Cage(C,i) \/ L~Cage(C,i) & C misses L~
Cage( C,i) by A1,GOBRD14:22,JORDAN10:5;
then
A48: C meets LeftComp Cage(C,i) by A47,XBOOLE_1:70;
reconsider D = (L~Cage(C,i))` as Subset of TOP-REAL 2;
D = LeftComp Cage(C,i) \/ RightComp Cage(C,i) by GOBRD12:10;
then
A49: RightComp Cage(C,i) c= D by XBOOLE_1:7;
C c= RightComp Cage(C,i) by A1,JORDAN10:11;
then
A50: C c= D by A49;
C meets C;
then
A51: C meets RightComp Cage(C,i) by A1,JORDAN10:11,XBOOLE_1:63;
LeftComp Cage(C,i) is_a_component_of D & RightComp Cage(C,i)
is_a_component_of D by GOBOARD9:def 1,def 2;
hence contradiction by A1,A48,A50,A51,JORDAN9:1,SPRECT_4:6;
end;
theorem Th47:
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;
A3: Cage(C,j)/.1 = N-min L~Cage(C,j) by A1,JORDAN9:32;
i < j or i = j by A2,XXREAL_0:1;
then
A4: 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:67;
set p = |[E-bound L~Cage(C,i) + 1,0]|;
A5: LeftComp Cage(C,i) misses RightComp Cage(C,i) by GOBRD14:14;
A6: p`1 = E-bound L~Cage(C,i) + 1;
p`1 > E-bound (L~Cage(C,i)) by XREAL_1:29;
then p`1 > E-bound (L~Cage(C,j)) by A4,XXREAL_0:2;
then
A7: p in LeftComp Cage(C,j) by A3,JORDAN2C:111;
Cage(C,i)/.1 = N-min L~Cage(C,i) by A1,JORDAN9:32;
then p in LeftComp Cage(C,i) by A6,JORDAN2C:111,XREAL_1:29;
then
A8: LeftComp(Cage(C,i)) meets LeftComp(Cage(C,j)) by A7,XBOOLE_0:3;
Cl RightComp Cage(C,i) = (RightComp Cage(C,i)) \/ L~Cage(C,i) & L~Cage(
C,i) misses LeftComp(Cage(C,i)) by GOBRD14:21,SPRECT_3:26;
then Cl RightComp(Cage(C,i)) misses LeftComp(Cage(C,i)) by A5,XBOOLE_1:70;
then L~Cage(C,j) misses LeftComp(Cage(C,i)) by A1,A2,Th46,XBOOLE_1:63;
then
LeftComp(Cage(C,j)) is_a_component_of (L~Cage(C,j))` & LeftComp(Cage(C,
i)) c= (L~Cage(C,j))` by GOBOARD9:def 1,SUBSET_1:23;
hence thesis by A8,GOBOARD9:4;
end;
theorem
C is connected & i <= j implies RightComp(Cage(C,j)) c= RightComp(Cage
(C, i ) )
proof
assume C is connected & i <= j;
then
A1: Cl LeftComp(Cage(C,i)) c= Cl LeftComp(Cage(C,j)) by Th47,PRE_TOPC:19;
(Cl LeftComp(Cage(C,i)))` = RightComp(Cage(C,i)) & (Cl LeftComp(Cage(C,j
)))` = RightComp(Cage(C,j)) by Th42;
hence thesis by A1,SUBSET_1:12;
end;
begin :: Preparing the Internal Approximation
definition
let C,n;
func X-SpanStart(C,n) -> Nat equals
2|^(n-'1) + 2;
correctness;
end;
theorem Th49:
2 < X-SpanStart(C,n) & X-SpanStart(C,n) < len Gauge(C,n)
proof
2|^(n-'1) > 0 by NEWTON:83;
then 2|^(n-'1) + 2 > 0 qua Nat+2 by XREAL_1:6;
hence 2 < X-SpanStart(C,n);
n-'1 <= n by NAT_D:44;
then len Gauge(C,n) = 2|^n + 3 & 2|^(n-'1) <= 2|^n by JORDAN8:def 1
,PREPOWER:93;
hence thesis by XREAL_1:8;
end;
theorem Th50:
1 <= X-SpanStart(C,n)-'1 & X-SpanStart(C,n)-'1 < len Gauge(C,n)
proof
2 < X-SpanStart(C,n) by Th49;
then
A1: X-SpanStart(C,n)-'1+1 = X-SpanStart(C,n) by XREAL_1:235,XXREAL_0:2;
1 < X-SpanStart(C,n) by Th49,XXREAL_0:2;
hence 1 <= X-SpanStart(C,n)-'1 by A1,NAT_1:13;
X-SpanStart(C,n) < len Gauge(C,n) & X-SpanStart(C,n)-'1 <= X-SpanStart(C
,n) by Th49,NAT_D:44;
hence thesis by XXREAL_0:2;
end;
definition
let C,n;
pred n is_sufficiently_large_for C means
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
A1: 2|^0 = 1 by NEWTON:4;
assume n is_sufficiently_large_for C;
then consider j such that
A2: j < width Gauge(C,n) and
A3: cell(Gauge(C,n),X-SpanStart(C,n)-'1,j) c= BDD C;
assume n < 1;
then
A4: n = 0 by NAT_1:14;
A5: j > 1
proof
A6: X-SpanStart(C,n)-'1 <= len Gauge(C,n) by Th50;
assume
A7: j <= 1;
per cases by A7,NAT_1:25;
suppose
A8: j = 0;
0 <= width Gauge(C,n);
then
A9: cell(Gauge(C,n),X-SpanStart(C,n)-'1,0) is non empty by A6,JORDAN1A:24;
cell(Gauge(C,n),X-SpanStart(C,n)-'1,0) c= UBD C by A6,JORDAN1A:49;
hence contradiction by A3,A8,A9,JORDAN2C:24,XBOOLE_1:68;
end;
suppose
A10: j = 1;
set i1 = X-SpanStart(C,n);
UBD C is_outside_component_of C by JORDAN2C:68;
then
A11: UBD C is_a_component_of C` by JORDAN2C:def 3;
i1 < len Gauge(C,n) & i1-'1 <= i1 by Th49,NAT_D:44;
then
A12: i1-'1 < len Gauge(C,n) by XXREAL_0:2;
BDD C c= C` by JORDAN2C:25;
then
A13: cell(Gauge(C,n),X-SpanStart(C,n)-'1,1) c= C` by A3,A10;
A14: width Gauge(C,n) <> 0 by MATRIX_0:def 10;
then
A15: 0 qua Nat+1 <= width Gauge(C,n) by NAT_1:14;
then
A16: cell(Gauge(C,n),X-SpanStart(C,n)-'1,1) is non empty by A6,JORDAN1A:24;
1 <= i1-'1 by Th50;
then cell(Gauge(C,n),i1-'1,0) /\ cell(Gauge(C,n),i1-'1,0 qua Nat+1) =
LSeg(Gauge(C,n)*(i1-'1,0 qua Nat+1),Gauge(C,n)*(i1-'1+1,0 qua Nat+1)) by A14
,A12,GOBOARD5:26;
then
A17: cell(Gauge(C,n),i1-'1,0) meets cell(Gauge(C,n),i1-'1,0 qua Nat +1);
cell(Gauge(C,n),X-SpanStart(C,n)-'1,0) c= UBD C by A6,JORDAN1A:49;
then cell(Gauge(C,n),X-SpanStart(C,n)-'1,1) c= UBD C by A15,A12,A17,A11
,A13,GOBOARD9:4,JORDAN1A:25;
hence contradiction by A3,A10,A16,JORDAN2C:24,XBOOLE_1:68;
end;
end;
A18: width Gauge(C,n) = 2|^n + 3 by JORDAN1A:28;
then
A19: j <= 3+1 by A2,A4,NEWTON:4;
A20: j + 1 < width Gauge(C,n)
proof
assume j + 1 >= width Gauge(C,n);
then
A21: j + 1 > width Gauge(C,n) or j + 1 = width Gauge(C,n) by XXREAL_0:1;
A22: X-SpanStart(C,n)-'1 <= len Gauge(C,n) by Th50;
per cases by A2,A21,NAT_1:13;
suppose
A23: j = width Gauge(C,n);
cell(Gauge(C,n),X-SpanStart(C,n)-'1,width Gauge(C,n)) is non empty
& cell( Gauge(C,n),X-SpanStart(C,n)-'1,width Gauge(C,n)) c= UBD C by A22,
JORDAN1A:24,50;
hence contradiction by A3,A23,JORDAN2C:24,XBOOLE_1:68;
end;
suppose
j + 1 = width Gauge(C,n);
then
A24: cell(Gauge(C,n),X-SpanStart(C,n)-'1,width Gauge(C,n)-'1) c= BDD C
by A3,NAT_D:34;
BDD C c= C` by JORDAN2C:25;
then
A25: cell(Gauge(C,n),X-SpanStart(C,n)-'1,width Gauge(C,n)-'1) c= C` by A24;
set i1 = X-SpanStart(C,n);
A26: width Gauge(C,n)-1 < width Gauge(C,n) by XREAL_1:146;
UBD C is_outside_component_of C by JORDAN2C:68;
then
A27: UBD C is_a_component_of C` by JORDAN2C:def 3;
width Gauge(C,n)-'1 <= width Gauge(C,n) by NAT_D:44;
then
A28: cell(Gauge(C,n),X-SpanStart(C,n)-'1,width Gauge(C,n)-'1) is non
empty by A22,JORDAN1A:24;
A29: cell(Gauge(C,n),X-SpanStart(C,n)-'1,width Gauge(C,n)) c= UBD C by A22,
JORDAN1A:50;
A30: 1 <= i1-'1 by Th50;
i1 < len Gauge(C,n) & i1-'1 <= i1 by Th49,NAT_D:44;
then
A31: i1-'1 < len Gauge(C,n) by XXREAL_0:2;
A32: width Gauge(C,n) <> 0 by MATRIX_0:def 10;
then width Gauge(C,n)-'1+1 = width Gauge(C,n) by NAT_1:14,XREAL_1:235;
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,A26,A30,GOBOARD5:26;
then
A33: cell(Gauge(C,n),i1-'1,width Gauge(C,n)) meets cell(Gauge(C,n),i1-'1
,width Gauge(C,n)-'1);
width Gauge(C,n)-'1 < width Gauge(C,n) by A32,A26,NAT_1:14,XREAL_1:233;
then cell(Gauge(C,n),X-SpanStart(C,n)-'1,width Gauge(C,n)-'1) c= UBD C
by A29,A31,A33,A27,A25,GOBOARD9:4,JORDAN1A:25;
hence contradiction by A24,A28,JORDAN2C:24,XBOOLE_1:68;
end;
end;
j = 0 or ... or j = 4 by A19;
then per cases;
suppose
j= 0 or j=1;
hence thesis by A5;
end;
suppose
A34: j=2;
A35: X-SpanStart(C,0) = 1 + 2 by A1,NAT_2:8;
then X-SpanStart(C,0)-'1 = X-SpanStart(C,0)-1 by NAT_D:39
.= 2 by A35;
hence contradiction by A3,A4,A34,JORDAN1B:18;
end;
suppose
j=3 or j=4;
hence thesis by A18,A20,A1,A4;
end;
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);
let f be FinSequence of TOP-REAL 2 such that
A1: f is_sequence_on G and
A2: len f > 1;
A3: 1 <= (len f)-'1 & (len f) -'1 +1 = len f by A2,NAT_D:49,XREAL_1:235;
let i1,j1 being Nat such that
A4: left_cell(f,(len f)-'1,G) meets C and
A5: [i1,j1] in Indices G and
A6: f/.((len f) -'1) = G*(i1,j1) and
A7: [i1,j1+1] in Indices G and
A8: f/.len f = G*(i1,j1+1);
A9: 1 <= i1 by A7,MATRIX_0:32;
A10: len G = width G & j1 <= width G by A5,JORDAN8:def 1,MATRIX_0:32;
A11: now
assume i1-'1 < 1;
then i1 <= 1 by NAT_1:14,NAT_D:36;
then i1 = 1 by A9,XXREAL_0:1;
then cell(G,1-'1,j1) meets C by A1,A4,A5,A6,A7,A8,A3,GOBRD13:21;
then cell(G,0,j1) meets C by XREAL_1:232;
hence contradiction by A10,JORDAN8:18;
end;
A12: i1-'1 <= i1 by NAT_D:35;
i1 <= len G by A5,MATRIX_0:32;
then
A13: i1-'1 <= len G by A12,XXREAL_0:2;
1 <= j1+1 & j1+1 <= width G by A7,MATRIX_0:32;
hence thesis by A13,A11,MATRIX_0:30;
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: 1 <= (len f)-'1 & (len f) -'1 +1 = len f by A2,NAT_D:49,XREAL_1:235;
A4: len G = width G by JORDAN8:def 1;
let i1,j1 being Nat such that
A5: left_cell(f,(len f)-'1,G) meets C and
A6: [i1,j1] in Indices G and
A7: f/.((len f) -'1) = G*(i1,j1) and
A8: [i1+1,j1] in Indices G and
A9: f/.len f = G*(i1+1,j1);
A10: j1 <= width G by A8,MATRIX_0:32;
A11: i1 <= len G by A6,MATRIX_0:32;
A12: now
assume j1+1 > len G;
then
A13: (len G)+1 <= j1+1 by NAT_1:13;
j1+1 <= (len G)+1 by A4,A10,XREAL_1:6;
then j1+1 = (len G)+1 by A13,XXREAL_0:1;
then cell(G,i1,len G) meets C by A1,A5,A6,A7,A8,A9,A3,GOBRD13:23;
hence contradiction by A11,JORDAN8:15;
end;
A14: 1 <= j1+1 by NAT_1:11;
1 <= i1+1 & i1+1 <= len G by A8,MATRIX_0:32;
hence thesis by A4,A14,A12,MATRIX_0:30;
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;
A3: 1 <= (len f)-'1 & (len f) -'1 +1 = len f by A2,NAT_D:49,XREAL_1:235;
let j1,i2 being Nat such that
A4: left_cell(f,(len f)-'1,G) meets C & [i2+1,j1] in Indices G & f/.((
len f) -'1) = G*(i2+1,j1) and
A5: [i2,j1] in Indices G and
A6: f/.len f = G*(i2,j1);
A7: i2 <= len G by A5,MATRIX_0:32;
A8: 1 <= j1 by A5,MATRIX_0:32;
A9: now
assume j1-'1 < 1;
then j1 <= 1 by NAT_1:14,NAT_D:36;
then j1 = 1 by A8,XXREAL_0:1;
then cell(G,i2,1-'1) meets C by A1,A4,A5,A6,A3,GOBRD13:25;
then cell(G,i2,0) meets C by XREAL_1:232;
hence contradiction by A7,JORDAN8:17;
end;
A10: j1-'1 <= j1 by NAT_D:35;
j1 <= width G by A5,MATRIX_0:32;
then
A11: j1-'1 <= width G by A10,XXREAL_0:2;
1 <= i2 by A5,MATRIX_0:32;
hence thesis by A7,A11,A9,MATRIX_0:30;
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;
A4: 1 <= (len f)-'1 & (len f) -'1 +1 = len f by A3,NAT_D:49,XREAL_1:235;
let i1,j2 being Nat such that
A5: left_cell(f,(len f)-'1,G) meets C & [i1,j2+1] in Indices G & f/.((
len f) -'1) = G*(i1,j2+1) and
A6: [i1,j2] in Indices G and
A7: f/.len f = G*(i1,j2);
A8: j2 <= width G by A6,MATRIX_0:32;
A9: i1 <= len G by A6,MATRIX_0:32;
A10: now
assume i1+1 > len G;
then
A11: (len G)+1 <= i1+1 by NAT_1:13;
i1+1 <= (len G)+1 by A9,XREAL_1:6;
then i1+1 = (len G)+1 by A11,XXREAL_0:1;
then cell(G,len G,j2) meets C by A2,A5,A6,A7,A4,GOBRD13:27;
hence contradiction by A1,A8,JORDAN8:16;
end;
A12: 1 <= i1+1 by NAT_1:11;
1 <= j2 by A6,MATRIX_0:32;
hence thesis by A8,A12,A10,MATRIX_0:30;
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;
A4: 1 <= (len f)-'1 & (len f) -'1 +1 = len f by A3,NAT_D:49,XREAL_1:235;
let i1,j1 being Nat such that
A5: front_left_cell(f,(len f)-'1,G) meets C & [i1,j1] in Indices G & f/.
(( len f) -'1) = G*(i1,j1) and
A6: [i1,j1+1] in Indices G and
A7: f/.len f = G*(i1,j1+1);
A8: i1 <= len G by A6,MATRIX_0:32;
A9: i1-'1 <= i1 by NAT_D:35;
A10: j1+1 <= width G by A6,MATRIX_0:32;
A11: now
assume j1+1+1 > len G;
then
A12: (len G)+1 <= j1+1+1 by NAT_1:13;
j1+1+1 <= (len G)+1 by A1,A10,XREAL_1:6;
then j1+1+1 = (len G)+1 by A12,XXREAL_0:1;
then cell(G,i1-'1,len G) meets C by A2,A5,A6,A7,A4,GOBRD13:34;
hence contradiction by A8,A9,JORDAN8:15,XXREAL_0:2;
end;
A13: 1 <= j1+1+1 by NAT_1:12;
1 <= i1 by A6,MATRIX_0:32;
hence thesis by A1,A8,A13,A11,MATRIX_0:30;
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;
A4: 1 <= (len f)-'1 & (len f) -'1 +1 = len f by A3,NAT_D:49,XREAL_1:235;
let i1,j1 being Nat such that
A5: front_left_cell(f,(len f)-'1,G) meets C & [i1,j1] in Indices G & f/.
(( len f) -'1) = G*(i1,j1) and
A6: [i1+1,j1] in Indices G and
A7: f/.len f = G*(i1+1,j1);
A8: j1 <= width G by A6,MATRIX_0:32;
A9: i1+1 <= len G by A6,MATRIX_0:32;
A10: now
assume i1+1+1 > len G;
then
A11: (len G)+1 <= i1+1+1 by NAT_1:13;
i1+1+1 <= (len G)+1 by A9,XREAL_1:6;
then i1+1+1 = (len G)+1 by A11,XXREAL_0:1;
then cell(G,len G,j1) meets C by A2,A5,A6,A7,A4,GOBRD13:36;
hence contradiction by A1,A8,JORDAN8:16;
end;
A12: 1 <= i1+1+1 by NAT_1:12;
1 <= j1 by A6,MATRIX_0:32;
hence thesis by A8,A12,A10,MATRIX_0:30;
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;
A4: 1 <= (len f)-'1 & (len f) -'1 +1 = len f by A3,NAT_D:49,XREAL_1:235;
let j1,i2 being Nat such that
A5: front_left_cell(f,(len f)-'1,G) meets C & [i2+1,j1] in Indices G & f
/.(( len f) -'1) = G*(i2+1,j1) and
A6: [i2,j1] in Indices G and
A7: f/.len f = G*(i2,j1);
A8: j1 <= width G by A6,MATRIX_0:32;
A9: 1 <= i2 by A6,MATRIX_0:32;
A10: now
assume i2-'1 < 1;
then i2 <= 1 by NAT_1:14,NAT_D:36;
then i2 = 1 by A9,XXREAL_0:1;
then cell(G,1-'1,j1-'1) meets C by A2,A5,A6,A7,A4,GOBRD13:38;
then cell(G,0,j1-'1) meets C by XREAL_1:232;
hence contradiction by A1,A8,JORDAN8:18,NAT_D:44;
end;
i2 <= len G by A6,MATRIX_0:32;
then
A11: i2-'1 <= len G by NAT_D:44;
1 <= j1 by A6,MATRIX_0:32;
hence thesis by A8,A11,A10,MATRIX_0:30;
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;
A3: 1 <= (len f)-'1 & (len f) -'1 +1 = len f by A2,NAT_D:49,XREAL_1:235;
let i1,j2 being Nat such that
A4: front_left_cell(f,(len f)-'1,G) meets C and
A5: [i1,j2+1] in Indices G and
A6: f/.((len f) -'1) = G*(i1,j2+1) and
A7: [i1,j2] in Indices G and
A8: f/.len f = G*(i1,j2);
A9: 1 <= j2 by A7,MATRIX_0:32;
A10: i1 <= len G by A5,MATRIX_0:32;
A11: now
assume j2-'1 < 1;
then j2 <= 1 by NAT_1:14,NAT_D:36;
then j2 = 1 by A9,XXREAL_0:1;
then cell(G,i1,1-'1) meets C by A1,A4,A5,A6,A7,A8,A3,GOBRD13:40;
then cell(G,i1,0) meets C by XREAL_1:232;
hence contradiction by A10,JORDAN8:17;
end;
j2 <= width G by A7,MATRIX_0:32;
then
A12: j2-'1 <= width G by NAT_D:44;
1 <= i1 & i1 <= len G by A7,MATRIX_0:32;
hence thesis by A12,A11,MATRIX_0:30;
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;
A4: 1 <= (len f)-'1 & (len f) -'1 +1 = len f by A3,NAT_D:49,XREAL_1:235;
let i1,j1 being Nat such that
A5: front_right_cell(f,(len f)-'1,G) meets C & [i1,j1] in Indices G & f
/.(( len f) -'1) = G*(i1,j1) and
A6: [i1,j1+1] in Indices G and
A7: f/.len f = G*(i1,j1+1);
A8: j1+1 <= width G by A6,MATRIX_0:32;
A9: i1 <= len G by A6,MATRIX_0:32;
A10: now
assume i1+1 > len G;
then
A11: (len G)+1 <= i1+1 by NAT_1:13;
i1+1 <= (len G)+1 by A9,XREAL_1:6;
then i1+1 = (len G)+1 by A11,XXREAL_0:1;
then cell(G,len G,j1+1) meets C by A2,A5,A6,A7,A4,GOBRD13:35;
hence contradiction by A1,A8,JORDAN8:16;
end;
A12: 1 <= i1+1 by NAT_1:11;
1 <= j1+1 by A6,MATRIX_0:32;
hence thesis by A8,A12,A10,MATRIX_0:30;
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;
A3: 1 <= (len f)-'1 & (len f) -'1 +1 = len f by A2,NAT_D:49,XREAL_1:235;
let i1,j1 being Nat such that
A4: front_right_cell(f,(len f)-'1,G) meets C & [i1,j1] in Indices G & f
/.(( len f) -'1) = G*(i1,j1) and
A5: [i1+1,j1] in Indices G and
A6: f/.len f = G*(i1+1,j1);
A7: i1+1 <= len G by A5,MATRIX_0:32;
A8: 1 <= j1 by A5,MATRIX_0:32;
A9: now
assume j1-'1 < 1;
then j1 <= 1 by NAT_1:14,NAT_D:36;
then j1 = 1 by A8,XXREAL_0:1;
then cell(G,i1+1,1-'1) meets C by A1,A4,A5,A6,A3,GOBRD13:37;
then cell(G,i1+1,0) meets C by XREAL_1:232;
hence contradiction by A7,JORDAN8:17;
end;
A10: j1-'1 <= j1 by NAT_D:35;
j1 <= width G by A5,MATRIX_0:32;
then
A11: j1-'1 <= width G by A10,XXREAL_0:2;
1 <= i1+1 by A5,MATRIX_0:32;
hence thesis by A7,A11,A9,MATRIX_0:30;
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;
A3: 1 <= (len f)-'1 & (len f) -'1 +1 = len f by A2,NAT_D:49,XREAL_1:235;
A4: len G = width G by JORDAN8:def 1;
let j1,i2 being Nat such that
A5: front_right_cell(f,(len f)-'1,G) meets C & [i2+1,j1] in Indices G &
f/.( (len f) -'1) = G*(i2+1,j1) and
A6: [i2,j1] in Indices G and
A7: f/.len f = G*(i2,j1);
A8: i2 <= len G by A6,MATRIX_0:32;
A9: j1 <= width G by A6,MATRIX_0:32;
A10: now
assume j1+1 > len G;
then
A11: (len G)+1 <= j1+1 by NAT_1:13;
j1+1 <= (len G)+1 by A9,A4,XREAL_1:6;
then j1+1 = (len G)+1 by A11,XXREAL_0:1;
then cell(G,i2-'1,len G) meets C by A1,A5,A6,A7,A3,GOBRD13:39;
hence contradiction by A8,JORDAN8:15,NAT_D:44;
end;
A12: 1 <= j1+1 by NAT_1:11;
1 <= i2 by A6,MATRIX_0:32;
hence thesis by A8,A12,A4,A10,MATRIX_0:30;
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;
A4: 1 <= (len f)-'1 & (len f) -'1 +1 = len f by A3,NAT_D:49,XREAL_1:235;
let i1,j2 being Nat such that
A5: front_right_cell(f,(len f)-'1,G) meets C & [i1,j2+1] in Indices G &
f/.( (len f) -'1) = G*(i1,j2+1) and
A6: [i1,j2] in Indices G and
A7: f/.len f = G*(i1,j2);
A8: j2 <= width G by A6,MATRIX_0:32;
A9: 1 <= i1 by A6,MATRIX_0:32;
A10: now
assume i1-'1 < 1;
then i1 <= 1 by NAT_1:14,NAT_D:36;
then i1 = 1 by A9,XXREAL_0:1;
then cell(G,1-'1,j2-'1) meets C by A2,A5,A6,A7,A4,GOBRD13:41;
then cell(G,0,j2-'1) meets C by XREAL_1:232;
hence contradiction by A1,A8,JORDAN8:18,NAT_D:44;
end;
i1 <= len G by A6,MATRIX_0:32;
then
A11: i1-'1 <= len G by NAT_D:44;
1 <= j2 by A6,MATRIX_0:32;
hence thesis by A8,A11,A10,MATRIX_0:30;
end;