:: Some Topological Properties of Cells in $R^2$
:: by Yatsuka Nakamura and Andrzej Trybulec
::
:: Received July 22, 1996
:: Copyright (c) 1996-2016 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, XBOOLE_0, PRE_TOPC, SQUARE_1,
XXREAL_0, CARD_1, RELAT_2, TARSKI, CONNSP_1, SETFAM_1, RCOMP_1, CONNSP_3,
ZFMISC_1, STRUCT_0, FUNCT_1, GOBOARD5, RELAT_1, MATRIX_1, EUCLID,
TOPREAL1, RLTOPSP1, ARYTM_3, GOBOARD2, TREES_1, ARYTM_1, FINSEQ_1,
MCART_1, GOBOARD1, TOPS_1, PCOMPS_1, METRIC_1, NAT_1;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, SEQM_3, TOPREAL1, GOBOARD1,
ORDINAL1, XXREAL_0, NUMBERS, BINOP_1, XCMPLX_0, XREAL_0, REAL_1, NAT_1,
NAT_D, SQUARE_1, MATRIX_0, STRUCT_0, PRE_TOPC, FINSEQ_1, MATRIX_1,
METRIC_1, TOPS_1, CONNSP_1, PCOMPS_1, RLVECT_1, RLTOPSP1, EUCLID,
GOBOARD2, GOBOARD5, CONNSP_3;
constructors SETFAM_1, REAL_1, SQUARE_1, TOPS_1, CONNSP_1, PCOMPS_1, GOBOARD2,
GOBOARD5, CONNSP_3, GOBOARD1, NAT_D, FUNCSDOM, CONVEX1;
registrations SUBSET_1, RELSET_1, XXREAL_0, XREAL_0, STRUCT_0, PRE_TOPC,
EUCLID, GOBOARD1, GOBOARD2, GOBOARD5, RLTOPSP1, SQUARE_1, ORDINAL1,
NAT_1;
requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM;
definitions TARSKI, XBOOLE_0;
equalities XBOOLE_0, EUCLID, SQUARE_1;
expansions TARSKI, XBOOLE_0;
theorems TARSKI, NAT_1, SPPOL_1, GOBOARD7, GOBOARD8, PRE_TOPC, CONNSP_1,
SUBSET_1, EUCLID, CONNSP_3, GOBOARD5, TOPS_1, TOPMETR, SPPOL_2, SQUARE_1,
METRIC_1, GOBOARD6, TOPREAL3, JORDAN1, ZFMISC_1, XBOOLE_0, XBOOLE_1,
XREAL_1, XXREAL_0, MATRIX_0;
schemes NAT_1;
begin
reserve i,j,k for Nat,
r,s,r1,r2,s1,s2,sb,tb for Real,
x for set,
GX for non empty TopSpace;
Lm1: sqrt 2>0 by SQUARE_1:25;
theorem Th1:
for A being Subset of GX, p being Point of GX st p in A & A is
connected holds A c= Component_of p
proof
let A be Subset of GX, p be Point of GX;
consider F being Subset-Family of GX such that
A1: for B being Subset of GX holds B in F iff B is connected & p in B and
A2: union F = Component_of p by CONNSP_1:def 7;
assume p in A & A is connected;
then
A3: A in F by A1;
A c= union F
by A3,TARSKI:def 4;
hence thesis by A2;
end;
theorem
for A,B,C being Subset of GX st C is a_component & A c= C & B is
connected & Cl A meets Cl B holds B c= C
proof
let A,B,C be Subset of GX;
assume that
A1: C is a_component and
A2: A c= C and
A3: B is connected and
A4: (Cl A) /\ (Cl B) <>{};
consider p being Point of GX such that
A5: p in (Cl A) /\ (Cl B) by A4,SUBSET_1:4;
reconsider C9 = C as Subset of GX;
C9 is closed by A1,CONNSP_1:33;
then Cl C = C by PRE_TOPC:22;
then
A6: Cl A c= C by A2,PRE_TOPC:19;
p in (Cl A) by A5,XBOOLE_0:def 4;
then
A7: Component_of p=C9 by A1,A6,CONNSP_1:41;
p in (Cl B) by A5,XBOOLE_0:def 4;
then
A8: Cl B c= Component_of p by A3,Th1,CONNSP_1:19;
B c= Cl B by PRE_TOPC:18;
hence thesis by A7,A8;
end;
reserve GZ for non empty TopSpace;
theorem
for A,B being Subset of GZ st A is a_component & B
is a_component holds A \/ B is a_union_of_components of GZ
proof
let A,B be Subset of GZ;
{A,B} c= bool (the carrier of GZ)
proof
let x be object;
assume x in {A,B};
then x=A or x=B by TARSKI:def 2;
hence thesis;
end;
then reconsider F2={A,B} as Subset-Family of GZ;
reconsider F=F2 as Subset-Family of GZ;
assume A is a_component & B is a_component;
then
A1: for B1 being Subset of GZ st B1 in F holds B1 is a_component by
TARSKI:def 2;
A \/ B=union F by ZFMISC_1:75;
hence thesis by A1,CONNSP_3:def 2;
end;
theorem
for B1,B2,V being Subset of GX holds Down(B1 \/ B2,V)=Down(B1,V) \/
Down(B2,V)
proof
let B1,B2,V be Subset of GX;
A1: Down(B2,V)=B2 /\ V by CONNSP_3:def 5;
Down(B1 \/ B2,V)=(B1 \/ B2)/\ V & Down(B1,V)=B1 /\ V by CONNSP_3:def 5;
hence thesis by A1,XBOOLE_1:23;
end;
theorem
for B1,B2,V being Subset of GX holds Down(B1 /\ B2,V)=Down(B1,V) /\
Down(B2,V)
proof
let B1,B2,V be Subset of GX;
Down(B1 /\ B2,V)=(B1 /\ B2)/\ V by CONNSP_3:def 5;
then
A1: Down(B1 /\ B2,V)=B1 /\(B2 /\ (V /\ V)) by XBOOLE_1:16
.=B1 /\(B2 /\ V /\ V) by XBOOLE_1:16
.= (B1 /\ V)/\ (B2 /\ V) by XBOOLE_1:16;
Down(B1,V)=B1 /\ V by CONNSP_3:def 5;
hence thesis by A1,CONNSP_3:def 5;
end;
reserve f for non constant standard special_circular_sequence,
G for non empty-yielding Matrix of TOP-REAL 2;
theorem Th6:
(L~f)` <> {}
proof
LSeg(1/2*((GoB f)*(1,width GoB f -' 1)+(GoB f)*(1,width GoB f))-|[1,0 ]|
, (GoB f)*(1,width GoB f)+|[-1,1]|) misses (L~f) by GOBOARD8:33;
then
LSeg(1/2*((GoB f)*(1,width GoB f -' 1)+(GoB f)*(1,width GoB f))-|[1,0 ]|
, (GoB f)*(1,width GoB f)+|[-1,1]|) c= (L~f)` by SUBSET_1:23;
hence thesis;
end;
registration
let f;
cluster (L~f)` -> non empty;
coherence by Th6;
end;
Lm2: the carrier of TOP-REAL 2 = REAL 2 by EUCLID:22;
theorem
for f holds the carrier of TOP-REAL 2 = union {cell(GoB f,i,j):i<=len
GoB f & j<=width GoB f}
proof
let f;
set j1=len GoB f, j2=width GoB f;
thus the carrier of TOP-REAL 2 c= union {cell(GoB f,i,j):i<=j1 & j<=j2}
proof
let x be object;
assume x in (the carrier of TOP-REAL 2);
then reconsider p=x as Point of TOP-REAL 2;
set r=p`1;
A1: now
assume that
A2: not r<(GoB f)*(1,1)`1 and
A3: not (GoB f)*(len GoB f,1)`1 <=r;
now
reconsider l=len GoB f as Nat;
defpred P[Nat] means $1=0 or(1<=$1 & $10 by A2,A5,GOBOARD7:32;
then 0+1<=k by NAT_1:13;
hence contradiction by A5,A7,A8,A9,XREAL_1:145;
end;
hence thesis;
end;
hence thesis;
end;
A10: P[0];
A11: for j holds P[j] from NAT_1:sch 2(A10,A6);
A12: l-10 by A25,A28,GOBOARD7:33;
then 0+1<=k by NAT_1:13;
hence contradiction by A28,A30,A31,A32,XREAL_1:145;
end;
hence thesis;
end;
hence thesis;
end;
A33: P[0];
A34: for j holds P[j] from NAT_1:sch 2(A33,A29);
A35: l-1=s1}
is Subset of TOP-REAL 2
proof
let s1;
{ |[ tb,sb ]| where tb,sb is Real:sb>=s1} c= REAL 2
proof
let y be object;
assume y in { |[ tb,sb ]| where tb,sb is Real:sb>=s1};
then ex t7,s7 being Real st |[ t7,s7 ]|=y & s7>=s1;
hence thesis by Lm2;
end;
hence thesis by EUCLID:22;
end;
Lm4: for s1 holds { |[ tb,sb ]| where tb,sb is Real:sb>s1}
is Subset of TOP-REAL 2
proof
let s1;
{ |[ tb,sb ]| where tb,sb is Real:sb>s1} c= REAL 2
proof
let y be object;
assume y in { |[ tb,sb ]|where tb,sb is Real:sb>s1};
then ex t7,s7 being Real st |[ t7,s7 ]|=y & s7>s1;
hence thesis by Lm2;
end;
hence thesis by EUCLID:22;
end;
Lm5: for s1 holds { |[ tb,sb ]| where tb,sb is Real:sb<=s1}
is Subset of TOP-REAL 2
proof
let s1;
{ |[ tb,sb ]| where tb,sb is Real:sb<=s1} c= REAL 2
proof
let y be object;
assume y in { |[ tb,sb ]| where tb,sb is Real:sb<=s1};
then ex t7,s7 being Real st |[ t7,s7 ]|=y & s7<=s1;
hence thesis by Lm2;
end;
hence thesis by EUCLID:22;
end;
Lm6: for s1 holds { |[ tb,sb ]| where tb,sb is Real:sb=s1} is Subset of TOP-REAL 2
proof
let s1;
{ |[ sb,tb ]|:sb>=s1} c= REAL 2
proof
let y be object;
assume y in { |[ sb,tb ]|:sb>=s1};
then ex s7,t7 being Real st |[ s7,t7 ]|=y & s7>=s1;
hence thesis by Lm2;
end;
hence thesis by EUCLID:22;
end;
Lm10: for s1 holds { |[ sb,tb ]| where sb,tb is Real:sb>s1}
is Subset of TOP-REAL 2
proof
let s1;
{ |[ sb,tb ]| where sb,tb is Real:sb>s1} c= REAL 2
proof
let y be object;
assume y in { |[ sb,tb ]| where sb,tb is Real:sb>s1};
then ex s7,t7 being Real st |[ s7,t7 ]|=y & s7>s1;
hence thesis by Lm2;
end;
hence thesis by EUCLID:22;
end;
theorem Th8:
for P1,P2 being Subset of TOP-REAL 2 st P1={ |[r,s]| : s <= s1 }
& P2={ |[r2,s2]| : s2 > s1 } holds P1=P2`
proof
let P1,P2 be Subset of TOP-REAL 2;
assume
A1: P1={ |[r,s]| : s <= s1 } & P2={ |[r2,s2]| : s2 > s1 };
A2: P2` c= P1
proof
let x be object;
assume
A3: x in P2`;
then reconsider p=x as Point of TOP-REAL 2;
A4: p=|[p`1,p`2]| by EUCLID:53;
x in (the carrier of TOP-REAL 2) \ P2 by A3,SUBSET_1:def 4;
then not x in P2 by XBOOLE_0:def 5;
then p`2 <= s1 by A1,A4;
hence thesis by A1,A4;
end;
P1 c= P2`
proof
let x be object;
assume
A5: x in P1;
then ex r,s st |[r,s]|=x & s <= s1 by A1;
then for r2,s2 holds not (|[r2,s2]|=x & s2 > s1) by SPPOL_2:1;
then not x in P2 by A1;
then x in (the carrier of TOP-REAL 2) \ P2 by A5,XBOOLE_0:def 5;
hence thesis by SUBSET_1:def 4;
end;
hence thesis by A2;
end;
theorem Th9:
for P1,P2 being Subset of TOP-REAL 2 st P1={ |[r,s]| : s >= s1 }
& P2={ |[r2,s2]| : s2 < s1 } holds P1=P2`
proof
let P1,P2 be Subset of TOP-REAL 2;
assume
A1: P1={ |[r,s]| : s >= s1 } & P2={ |[r2,s2]| : s2 < s1 };
A2: P2` c= P1
proof
let x be object;
assume
A3: x in P2`;
then reconsider p=x as Point of TOP-REAL 2;
A4: p=|[p`1,p`2]| by EUCLID:53;
x in (the carrier of TOP-REAL 2) \ P2 by A3,SUBSET_1:def 4;
then not x in P2 by XBOOLE_0:def 5;
then p`2 >= s1 by A1,A4;
hence thesis by A1,A4;
end;
P1 c= P2`
proof
let x be object;
assume
A5: x in P1;
then ex r,s st |[r,s]|=x & s >= s1 by A1;
then not ex r2,s2 st |[r2,s2]|=x & s2 < s1 by SPPOL_2:1;
then not x in P2 by A1;
then x in (the carrier of TOP-REAL 2) \ P2 by A5,XBOOLE_0:def 5;
hence thesis by SUBSET_1:def 4;
end;
hence thesis by A2;
end;
theorem Th10:
for P1,P2 being Subset of TOP-REAL 2 st
P1={ |[s,r]| where s,r is Real: s >= s1 }
& P2={ |[s2,r2]| where s2,r2 is Real: s2 < s1 } holds P1=P2`
proof
let P1,P2 be Subset of TOP-REAL 2;
assume
A1: P1={ |[s,r]| where s,r is Real: s >= s1 } &
P2={ |[s2,r2]| where s2,r2 is Real: s2 < s1 };
A2: P2` c= P1
proof
let x be object;
assume
A3: x in P2`;
then reconsider p=x as Point of TOP-REAL 2;
A4: p=|[p`1,p`2]| by EUCLID:53;
x in (the carrier of TOP-REAL 2) \ P2 by A3,SUBSET_1:def 4;
then not x in P2 by XBOOLE_0:def 5;
then p`1 >= s1 by A1,A4;
hence thesis by A1,A4;
end;
P1 c= P2`
proof
let x be object;
assume
A5: x in P1;
then ex s,r st |[s,r]|=x & s >= s1 by A1;
then not ex s2,r2 st |[s2,r2]|=x & s2 < s1 by SPPOL_2:1;
then not x in P2 by A1;
then x in (the carrier of TOP-REAL 2) \ P2 by A5,XBOOLE_0:def 5;
hence thesis by SUBSET_1:def 4;
end;
hence thesis by A2;
end;
theorem Th11:
for P1,P2 being Subset of TOP-REAL 2 st
P1={ |[s,r]| where s,r is Real: s <= s1 }
& P2={ |[s2,r2]| where s2,r2 is Real: s2 > s1 } holds P1=P2`
proof
let P1,P2 be Subset of TOP-REAL 2;
assume
A1: P1={ |[s,r]| where s,r is Real : s <= s1 } &
P2={ |[s2,r2]| where s2,r2 is Real: s2 > s1 };
A2: P2` c= P1
proof
let x be object;
assume
A3: x in P2`;
then reconsider p=x as Point of TOP-REAL 2;
A4: p=|[p`1,p`2]| by EUCLID:53;
x in (the carrier of TOP-REAL 2) \ P2 by A3,SUBSET_1:def 4;
then not x in P2 by XBOOLE_0:def 5;
then p`1 <= s1 by A1,A4;
hence thesis by A1,A4;
end;
P1 c= P2`
proof
let x be object;
assume
A5: x in P1;
then ex s,r st |[s,r]|=x & s <= s1 by A1;
then not ex s2,r2 st |[s2,r2]|=x & s2 > s1 by SPPOL_2:1;
then not x in { |[s2,r2]| where s2,r2 is Real: s2 > s1 };
then x in (the carrier of TOP-REAL 2) \ P2 by A1,A5,XBOOLE_0:def 5;
hence thesis by SUBSET_1:def 4;
end;
hence thesis by A2;
end;
theorem Th12:
for P being Subset of TOP-REAL 2, s1 st P= { |[r,s]| : s <= s1 }
holds P is closed
proof
let P be Subset of TOP-REAL 2, s1;
reconsider P1= { |[r,s]| where r,s is Real: s > s1 } as Subset of TOP-REAL 2
by Lm4;
assume P= { |[r,s]| : s <= s1 };
then
A1: P=P1` by Th8;
P1 is open by JORDAN1:22;
hence thesis by A1,TOPS_1:4;
end;
theorem Th13:
for P being Subset of TOP-REAL 2,s1 st P={ |[r,s]| : s1 <= s }
holds P is closed
proof
let P be Subset of TOP-REAL 2, s1;
reconsider P1= { |[r,s]| : s1 > s } as Subset of TOP-REAL 2 by Lm6;
assume P= { |[r,s]| : s1 <= s };
then
A1: P=P1` by Th9;
P1 is open by JORDAN1:23;
hence thesis by A1,TOPS_1:4;
end;
theorem Th14:
for P being Subset of TOP-REAL 2, s1 st
P= { |[s,r]| where s,r is Real: s <= s1 }
holds P is closed
proof
let P be Subset of TOP-REAL 2, s1;
reconsider P1= { |[s,r]| where s,r is Real : s > s1 }
as Subset of TOP-REAL 2 by Lm10;
assume P= { |[s,r]| where s,r is Real: s <= s1 };
then
A1: P=P1` by Th11;
P1 is open by JORDAN1:20;
hence thesis by A1,TOPS_1:4;
end;
theorem Th15:
for P being Subset of TOP-REAL 2,s1 st
P={ |[s,r]| where s,r is Real: s1 <= s }
holds P is closed
proof
let P be Subset of TOP-REAL 2, s1;
reconsider P1= { |[s,r]| where s,r is Real : s < s1 }
as Subset of TOP-REAL 2 by Lm8;
assume P= { |[s,r]| where s,r is Real: s >= s1 };
then
A1: P=P1` by Th10;
P1 is open by JORDAN1:21;
hence thesis by A1,TOPS_1:4;
end;
theorem Th16:
for G being Matrix of TOP-REAL 2 holds h_strip(G,j) is closed
proof
let G be Matrix of TOP-REAL 2;
now
per cases;
case
A1: j<1;
A2: now
assume j >= width G;
then h_strip(G,j)={ |[r,s]| : G*(1,j)`2 <= s } by GOBOARD5:def 2;
hence thesis by Th13;
end;
now
assume j= width G;
then h_strip(G,j) = { |[r,s]| : G*(1,j)`2 <= s } by GOBOARD5:def 2;
hence thesis by Th13;
end;
end;
hence thesis;
end;
theorem Th17:
for G being Matrix of TOP-REAL 2 holds v_strip(G,j) is closed
proof
let G be Matrix of TOP-REAL 2;
now
per cases;
case
A1: j<1;
A2: now
assume j >= len G;
then v_strip(G,j)={ |[s,r]| where s,r is Real: G*(j,1)`1 <= s }
by GOBOARD5:def 1;
hence thesis by Th15;
end;
now
assume j= len G;
then v_strip(G,j) = { |[s,r]| where s,r is Real:
G*(j,1)`1 <= s } by GOBOARD5:def 1;
hence thesis by Th15;
end;
end;
hence thesis;
end;
theorem Th18:
G is X_equal-in-line implies v_strip(G,0) = { |[r,s]| : r <= G*( 1,1)`1 }
proof
0 <> width G by MATRIX_0:def 10;
then
A1: 1 <= width G by NAT_1:14;
assume G is X_equal-in-line;
hence thesis by A1,GOBOARD5:10;
end;
theorem Th19:
G is X_equal-in-line implies v_strip(G,len G) = { |[r,s]| : G*(
len G,1)`1 <= r }
proof
0 <> width G by MATRIX_0:def 10;
then
A1: 1 <= width G by NAT_1:14;
assume G is X_equal-in-line;
hence thesis by A1,GOBOARD5:9;
end;
theorem Th20:
G is X_equal-in-line & 1 <= i & i < len G implies v_strip(G,i) =
{ |[r,s]| : G*(i,1)`1 <= r & r <= G*(i+1,1)`1 }
proof
assume
A1: G is X_equal-in-line;
0 <> width G by MATRIX_0:def 10;
then
A2: 1 <= width G by NAT_1:14;
assume 1 <= i & i < len G;
hence thesis by A1,A2,GOBOARD5:8;
end;
theorem Th21:
G is Y_equal-in-column implies h_strip(G,0) = { |[r,s]| : s <= G *(1,1)`2 }
proof
0 <> len G by MATRIX_0:def 10;
then
A1: 1 <= len G by NAT_1:14;
assume G is Y_equal-in-column;
hence thesis by A1,GOBOARD5:7;
end;
theorem Th22:
G is Y_equal-in-column implies h_strip(G,width G) = { |[r,s]| :
G*(1,width G)`2 <= s }
proof
0 <> len G by MATRIX_0:def 10;
then
A1: 1 <= len G by NAT_1:14;
assume G is Y_equal-in-column;
hence thesis by A1,GOBOARD5:6;
end;
theorem Th23:
G is Y_equal-in-column & 1 <= j & j < width G implies h_strip(G,
j) = { |[r,s]| : G*(1,j)`2 <= s & s <= G*(1,j+1)`2 }
proof
assume
A1: G is Y_equal-in-column;
0 <> len G by MATRIX_0:def 10;
then
A2: 1 <= len G by NAT_1:14;
assume 1 <= j & j < width G;
hence thesis by A1,A2,GOBOARD5:5;
end;
reserve G for non empty-yielding X_equal-in-line Y_equal-in-column Matrix of
TOP-REAL 2;
theorem Th24:
cell(G,0,0) = { |[r,s]| : r <= G*(1,1)`1 & s <= G*(1,1)`2 }
proof
A1: cell(G,0,0) = v_strip(G,0) /\ h_strip(G,0) by GOBOARD5:def 3;
A2: h_strip(G,0) = { |[r,s]| : s <= G*(1,1)`2 } by Th21;
A3: v_strip(G,0) = { |[r,s]| : r <= G*(1,1)`1 } by Th18;
thus cell(G,0,0) c= { |[r,s]| : r <= G*(1,1)`1 & s <= G*(1,1)`2 }
proof
let x be object;
assume
A4: x in cell(G,0,0);
then x in v_strip(G,0) by A1,XBOOLE_0:def 4;
then consider r1,s1 such that
A5: x = |[r1,s1]| and
A6: r1 <= G*(1,1)`1 by A3;
x in h_strip(G,0) by A1,A4,XBOOLE_0:def 4;
then consider r2,s2 such that
A7: x = |[r2,s2]| and
A8: s2 <= G*(1,1)`2 by A2;
s1 = s2 by A5,A7,SPPOL_2:1;
hence thesis by A5,A6,A8;
end;
let x be object;
assume x in { |[r,s]| : r <= G*(1,1)`1 & s <= G*(1,1)`2 };
then
A9: ex r,s st x = |[r,s]| & r <= G*(1,1)`1 & s <= G*(1,1)`2;
then
A10: x in h_strip(G,0) by A2;
x in v_strip(G,0) by A3,A9;
hence thesis by A1,A10,XBOOLE_0:def 4;
end;
theorem Th25:
cell(G,0,width G) = { |[r,s]| : r <= G*(1,1)`1 & G*(1,width G)`2 <= s }
proof
A1: cell(G,0,width G) = v_strip(G,0) /\ h_strip(G,width G) by GOBOARD5:def 3;
A2: h_strip(G,width G) = { |[r,s]| : G*(1,width G)`2 <= s } by Th22;
A3: v_strip(G,0) = { |[r,s]| : r <= G*(1,1)`1 } by Th18;
thus cell(G,0,width G) c= { |[r,s]| : r <= G*(1,1)`1 & G*(1,width G)`2 <= s }
proof
let x be object;
assume
A4: x in cell(G,0,width G);
then x in v_strip(G,0) by A1,XBOOLE_0:def 4;
then consider r1,s1 such that
A5: x = |[r1,s1]| and
A6: r1 <= G*(1,1)`1 by A3;
x in h_strip(G,width G) by A1,A4,XBOOLE_0:def 4;
then consider r2,s2 such that
A7: x = |[r2,s2]| and
A8: G*(1,width G)`2 <= s2 by A2;
s1 = s2 by A5,A7,SPPOL_2:1;
hence thesis by A5,A6,A8;
end;
let x be object;
assume x in { |[r,s]| : r <= G*(1,1)`1 & G*(1,width G)`2 <= s };
then
A9: ex r,s st x = |[r,s]| & r <= G*(1,1)`1 & G*(1,width G)`2 <= s;
then
A10: x in h_strip(G,width G) by A2;
x in v_strip(G,0) by A3,A9;
hence thesis by A1,A10,XBOOLE_0:def 4;
end;
theorem Th26:
1 <= j & j < width G implies cell(G,0,j) = { |[r,s]| : r <= G*(1
,1)`1 & G*(1,j)`2 <= s & s <= G*(1,j+1)`2 }
proof
A1: cell(G,0,j) = v_strip(G,0) /\ h_strip(G,j) by GOBOARD5:def 3;
assume 1 <= j & j < width G;
then
A2: h_strip(G,j) = { |[r,s]| : G*(1,j)`2 <= s & s <= G*(1,j+1)`2 } by Th23;
A3: v_strip(G,0) = { |[r,s]| : r <= G*(1,1)`1 } by Th18;
thus cell(G,0,j) c= { |[r,s]| : r <= G*(1,1)`1 & G*(1,j)`2 <= s & s <= G*(1,
j+1)`2 }
proof
let x be object;
assume
A4: x in cell(G,0,j);
then x in v_strip(G,0) by A1,XBOOLE_0:def 4;
then consider r1,s1 such that
A5: x = |[r1,s1]| and
A6: r1 <= G*(1,1)`1 by A3;
x in h_strip(G,j) by A1,A4,XBOOLE_0:def 4;
then consider r2,s2 such that
A7: x = |[r2,s2]| and
A8: G*(1,j)`2 <= s2 & s2 <= G*(1,j+1)`2 by A2;
s1 = s2 by A5,A7,SPPOL_2:1;
hence thesis by A5,A6,A8;
end;
let x be object;
assume
x in { |[r,s]| : r <= G*(1,1)`1 & G*(1,j)`2 <= s & s <= G* (1,j+1) `2 };
then
A9: ex r,s st x = |[r,s]| & r <= G*(1,1)`1 & G*(1,j)`2 <= s & s <= G*(1,j+1
)`2;
then
A10: x in h_strip(G,j) by A2;
x in v_strip(G,0) by A3,A9;
hence thesis by A1,A10,XBOOLE_0:def 4;
end;
theorem Th27:
cell(G,len G,0) = { |[r,s]| : G*(len G,1)`1 <= r & s <= G*(1,1) `2 }
proof
A1: cell(G,len G,0) = v_strip(G,len G) /\ h_strip(G,0) by GOBOARD5:def 3;
A2: h_strip(G,0) = { |[r,s]| : s <= G*(1,1)`2 } by Th21;
A3: v_strip(G,len G) = { |[r,s]| : G*(len G,1)`1 <= r } by Th19;
thus cell(G,len G,0) c= { |[r,s]| : G*(len G,1)`1 <= r & s <= G*(1,1)`2 }
proof
let x be object;
assume
A4: x in cell(G,len G,0);
then x in v_strip(G,len G) by A1,XBOOLE_0:def 4;
then consider r1,s1 such that
A5: x = |[r1,s1]| and
A6: G*(len G,1)`1 <= r1 by A3;
x in h_strip(G,0) by A1,A4,XBOOLE_0:def 4;
then consider r2,s2 such that
A7: x = |[r2,s2]| and
A8: s2 <= G*(1,1)`2 by A2;
s1 = s2 by A5,A7,SPPOL_2:1;
hence thesis by A5,A6,A8;
end;
let x be object;
assume x in { |[r,s]| : G*(len G,1)`1 <= r & s <= G*(1,1)`2 };
then
A9: ex r,s st x = |[r,s]| & G*(len G,1)`1 <= r & s <= G*(1,1)`2;
then
A10: x in h_strip(G,0) by A2;
x in v_strip(G,len G) by A3,A9;
hence thesis by A1,A10,XBOOLE_0:def 4;
end;
theorem Th28:
cell(G,len G,width G) = { |[r,s]| : G*(len G,1)`1 <= r & G*(1,
width G)`2 <= s }
proof
A1: cell(G,len G,width G) = v_strip(G,len G) /\ h_strip(G,width G) by
GOBOARD5:def 3;
A2: h_strip(G,width G) = { |[r,s]| : G*(1,width G)`2 <= s } by Th22;
A3: v_strip(G,len G) = { |[r,s]| : G*(len G,1)`1 <= r } by Th19;
thus cell(G,len G,width G) c= { |[r,s]| : G*(len G,1)`1 <= r & G*(1,width G)
`2 <= s }
proof
let x be object;
assume
A4: x in cell(G,len G,width G);
then x in v_strip(G,len G) by A1,XBOOLE_0:def 4;
then consider r1,s1 such that
A5: x = |[r1,s1]| and
A6: G*(len G,1)`1 <= r1 by A3;
x in h_strip(G,width G) by A1,A4,XBOOLE_0:def 4;
then consider r2,s2 such that
A7: x = |[r2,s2]| and
A8: G*(1,width G)`2 <= s2 by A2;
s1 = s2 by A5,A7,SPPOL_2:1;
hence thesis by A5,A6,A8;
end;
let x be object;
assume x in { |[r,s]| : G*(len G,1)`1 <= r & G*(1,width G)`2 <= s };
then
A9: ex r,s st x = |[r,s]| & G*(len G,1)`1 <= r & G*(1,width G)`2 <= s;
then
A10: x in h_strip(G,width G) by A2;
x in v_strip(G,len G) by A3,A9;
hence thesis by A1,A10,XBOOLE_0:def 4;
end;
theorem Th29:
1 <= j & j < width G implies cell(G,len G,j) = { |[r,s]| : G*(
len G,1)`1 <= r & G*(1,j)`2 <= s & s <= G*(1,j+1)`2 }
proof
A1: cell(G,len G,j) = v_strip(G,len G) /\ h_strip(G,j) by GOBOARD5:def 3;
assume 1 <= j & j < width G;
then
A2: h_strip(G,j) = { |[r,s]| : G*(1,j)`2 <= s & s <= G* (1,j+1)`2 } by Th23;
A3: v_strip(G,len G) = { |[r,s]| : G*(len G,1)`1 <= r } by Th19;
thus cell(G,len G,j) c= { |[r,s]| : G*(len G,1)`1 <= r & G*(1,j)`2 <= s & s
<= G*(1,j+1)`2 }
proof
let x be object;
assume
A4: x in cell(G,len G,j);
then x in v_strip(G,len G) by A1,XBOOLE_0:def 4;
then consider r1,s1 such that
A5: x = |[r1,s1]| and
A6: G*(len G,1)`1 <= r1 by A3;
x in h_strip(G,j) by A1,A4,XBOOLE_0:def 4;
then consider r2,s2 such that
A7: x = |[r2,s2]| and
A8: G*(1,j)`2 <= s2 & s2 <= G*(1,j+1)`2 by A2;
s1 = s2 by A5,A7,SPPOL_2:1;
hence thesis by A5,A6,A8;
end;
let x be object;
assume
x in { |[r,s]| : G*(len G,1)`1 <= r & G*(1,j)`2 <= s & s <= G*(1,j+ 1)`2 };
then
A9: ex r,s st x = |[r,s]| & G*(len G,1)`1 <= r & G*(1,j)`2 <= s & s <= G*(1
,j+1)`2;
then
A10: x in h_strip(G,j) by A2;
x in v_strip(G,len G) by A3,A9;
hence thesis by A1,A10,XBOOLE_0:def 4;
end;
theorem Th30:
1 <= i & i < len G implies cell(G,i,0) = { |[r,s]|: G*(i,1)`1 <=
r & r <= G*(i+1,1)`1 & s <= G* (1,1)`2 }
proof
A1: cell(G,i,0) = v_strip(G,i) /\ h_strip(G,0) by GOBOARD5:def 3;
assume 1 <= i & i < len G;
then
A2: v_strip(G,i) = { |[r,s]| : G*(i,1)`1 <= r & r <= G* (i+1,1)`1 } by Th20;
A3: h_strip(G,0) = { |[r,s]| : s <= G*(1,1)`2 } by Th21;
thus cell(G,i,0) c= { |[r,s]| : G*(i,1)`1 <= r & r <= G*(i+1,1)`1 & s <= G*(
1,1)`2 }
proof
let x be object;
assume
A4: x in cell(G,i,0);
then x in v_strip(G,i) by A1,XBOOLE_0:def 4;
then consider r1,s1 such that
A5: x = |[r1,s1]| and
A6: G*(i,1)`1 <= r1 & r1 <= G*(i+1,1)`1 by A2;
x in h_strip(G,0) by A1,A4,XBOOLE_0:def 4;
then consider r2,s2 such that
A7: x = |[r2,s2]| and
A8: s2 <= G*(1,1)`2 by A3;
s1 = s2 by A5,A7,SPPOL_2:1;
hence thesis by A5,A6,A8;
end;
let x be object;
assume
x in { |[r,s]| : G*(i,1)`1 <= r & r <= G*(i+1,1)`1 & s <= G* (1,1) `2 };
then
A9: ex r,s st x = |[r,s]| & G*(i,1)`1 <= r & r <= G*(i+1,1)`1 & s <= G*(1,1
)`2;
then
A10: x in h_strip(G,0) by A3;
x in v_strip(G,i) by A2,A9;
hence thesis by A1,A10,XBOOLE_0:def 4;
end;
theorem Th31:
1 <= i & i < len G implies cell(G,i,width G) = { |[r,s]|: G*(i,1
)`1 <= r & r <= G*(i+1,1)`1 & G*(1,width G)`2 <= s }
proof
A1: cell(G,i,width G) = v_strip(G,i) /\ h_strip(G,width G) by GOBOARD5:def 3;
assume 1 <= i & i < len G;
then
A2: v_strip(G,i) = { |[r,s]| : G*(i,1)`1 <= r & r <= G* (i+1,1)`1 } by Th20;
A3: h_strip(G,width G) = { |[r,s]| : G*(1,width G)`2 <= s } by Th22;
thus cell(G,i,width G) c= { |[r,s]| : G*(i,1)`1 <= r & r <= G*(i+1,1)`1 & G*
(1,width G)`2 <= s }
proof
let x be object;
assume
A4: x in cell(G,i,width G);
then x in v_strip(G,i) by A1,XBOOLE_0:def 4;
then consider r1,s1 such that
A5: x = |[r1,s1]| and
A6: G*(i,1)`1 <= r1 & r1 <= G*(i+1,1)`1 by A2;
x in h_strip(G,width G) by A1,A4,XBOOLE_0:def 4;
then consider r2,s2 such that
A7: x = |[r2,s2]| and
A8: G*(1,width G)`2 <= s2 by A3;
s1 = s2 by A5,A7,SPPOL_2:1;
hence thesis by A5,A6,A8;
end;
let x be object;
assume x in { |[r,s]| : G*(i,1)`1 <= r & r <= G*(i+1,1)`1 & G* (1,width G)
`2 <= s };
then
A9: ex r,s st x = |[r,s]| & G*(i,1)`1 <= r & r <= G*(i+1,1)`1 & G*(1,width
G)`2 <= s;
then
A10: x in h_strip(G,width G) by A3;
x in v_strip(G,i) by A2,A9;
hence thesis by A1,A10,XBOOLE_0:def 4;
end;
theorem Th32:
1 <= i & i < len G & 1 <= j & j < width G implies cell(G,i,j) =
{ |[r,s]| : G*(i,1)`1 <= r & r <= G*(i+1,1)`1 & G*(1,j)`2 <= s & s <= G*(1,j+1)
`2 }
proof
assume that
A1: 1 <= i & i < len G and
A2: 1 <= j & j < width G;
A3: h_strip(G,j) = { |[r,s]| : G*(1,j)`2 <= s & s <= G* (1,j+1)`2 } by A2,Th23;
A4: cell(G,i,j) = v_strip(G,i) /\ h_strip(G,j) by GOBOARD5:def 3;
A5: v_strip(G,i) = { |[r,s]| : G*(i,1)`1 <= r & r <= G* (i+1,1)`1 } by A1,Th20;
thus cell(G,i,j) c= { |[r,s]| : G*(i,1)`1 <= r & r <= G*(i+1,1)`1 & G*(1,j)
`2 <= s & s <= G*(1,j+1)`2 }
proof
let x be object;
assume
A6: x in cell(G,i,j);
then x in v_strip(G,i) by A4,XBOOLE_0:def 4;
then consider r1,s1 such that
A7: x = |[r1,s1]| and
A8: G*(i,1)`1 <= r1 & r1 <= G*(i+1,1)`1 by A5;
x in h_strip(G,j) by A4,A6,XBOOLE_0:def 4;
then consider r2,s2 such that
A9: x = |[r2,s2]| and
A10: G*(1,j)`2 <= s2 & s2 <= G*(1,j+1)`2 by A3;
s1 = s2 by A7,A9,SPPOL_2:1;
hence thesis by A7,A8,A10;
end;
let x be object;
assume x in { |[r,s]| : G*(i,1)`1 <= r & r <= G*(i+1,1)`1 & G*(1,j)`2 <= s
& s <= G*(1,j+1)`2 };
then
A11: ex r,s st x = |[r,s]| & G*(i,1)`1 <= r & r <= G*(i+1,1)`1 & G*(1,j)`2
<= s & s <= G*(1,j+1)`2;
then
A12: x in h_strip(G,j) by A3;
x in v_strip(G,i) by A5,A11;
hence thesis by A4,A12,XBOOLE_0:def 4;
end;
theorem Th33:
for G being Matrix of TOP-REAL 2 holds cell(G,i,j) is closed
proof
let G be Matrix of TOP-REAL 2;
A1: v_strip(G,i) is closed by Th17;
cell(G,i,j)=h_strip(G,j) /\ v_strip(G,i) & h_strip(G,j) is closed by Th16,
GOBOARD5:def 3;
hence thesis by A1,TOPS_1:8;
end;
theorem Th34:
for G being non empty-yielding Matrix of TOP-REAL 2 holds 1<=len
G & 1<=width G
proof
let G be non empty-yielding Matrix of TOP-REAL 2;
( not len G=0)& not width G=0 by MATRIX_0:def 10;
hence thesis by NAT_1:14;
end;
theorem
for G being Go-board holds i<=len G & j<=width G implies cell(G,i,j)=
Cl Int cell(G,i,j)
proof
let G be Go-board;
set Y = Int cell(G,i,j);
assume
A1: i<=len G & j<=width G;
A2: cell(G,i,j) c= Cl Y
proof
let x be object;
assume
A3: x in cell(G,i,j);
then reconsider p=x as Point of TOP-REAL 2;
for G0 being Subset of TOP-REAL 2 st G0 is open holds p in G0 implies
Y meets G0
proof
let G0 be Subset of TOP-REAL 2;
assume
A4: G0 is open;
now
reconsider u=p as Point of Euclid 2 by EUCLID:22;
assume
A5: p in G0;
A6: j=0 or 0+1<=j by NAT_1:13;
reconsider v=u as Element of REAL 2;
A7: TopSpaceMetr Euclid 2 = the TopStruct of TOP-REAL 2 by EUCLID:def 8;
then reconsider G00=G0 as Subset of TopSpaceMetr Euclid 2;
G00 is open by A4,A7,PRE_TOPC:30;
then consider r be Real such that
A8: r>0 and
A9: Ball(u,r) c= G00 by A5,TOPMETR:15;
reconsider r as Real;
A10: i=0 or 0+1<=i by NAT_1:13;
now
per cases by A1,A10,A6,XXREAL_0:1;
case
A11: i=0 & j=0;
then
p in { |[r2,s2]| : r2 <= G*(1,1)`1 & s2 <= G*(1,1)`2 } by A3,Th24;
then consider r2,s2 such that
A12: p=|[r2,s2]| and
A13: r2 <= G*(1,1)`1 and
A14: s2 <= G*(1,1)`2;
set r3=r2-r/2 ,s3=s2-r/2;
A15: r*2">0 by A8,XREAL_1:129;
then s3 {}(TOP-REAL 2) by A9,A17,XBOOLE_0:def 4;
end;
case
A22: i=0 & j=width G;
then p in { |[r2,s2]| : r2 <= G*(1,1)`1 & G*(1,width G)`2 <=s2 }
by A3,Th25;
then consider r2,s2 such that
A23: p=|[r2,s2]| and
A24: r2 <= G*(1,1)`1 and
A25: G*(1,width G)`2<=s2;
set r3=r2-r/2,s3=s2+r/2;
A26: r*2">0 by A8,XREAL_1:129;
then s3>s2 by XREAL_1:29;
then
A27: s3>G*(1,width G)`2 by A25,XXREAL_0:2;
reconsider q0=|[r3,s3]| as Point of TOP-REAL 2;
reconsider u0=q0 as Point of Euclid 2 by EUCLID:22;
r3 {}(TOP-REAL 2) by A9,A28,XBOOLE_0:def 4;
end;
case
A32: i=0 & 1<=j & j0 by XREAL_1:50;
then
A44: rm>0 by A8,XXREAL_0:21;
then s3>s2 by XREAL_1:29,139;
then
A45: s3>G*(1,j)`2 by A35,XXREAL_0:2;
rm/2<=r/2 by XREAL_1:72,XXREAL_0:17;
then (rm/2)^2<=(r/2)^2 by A44,SQUARE_1:15;
then
A46: (r/2)^2+(rm/2)^2<=(r/2)^2+(r/2)^2 by XREAL_1:7;
0<=(rm/2)^2 & 0<=(r/2)^2 by XREAL_1:63;
then
sqrt((r/2)^2+(rm/2)^2)<=sqrt((r/2)^2+(r/2) ^2) by A46,SQUARE_1:26;
then dist(u,u0) = (Pitag_dist 2).(v,v0) & sqrt ((r2 - r3)^2 +
(s2 - s3)^2)0 by A8,XREAL_1:129;
then r3 {}(TOP-REAL 2) by A9,A47,XBOOLE_0:def 4;
end;
case
A50: G*(1,j)`2 0 by A8,XREAL_1:129;
then r3=0 by XREAL_1:63;
then (r/2)^2 + 0 <=(r/2)^2 + (r/2)^2 by XREAL_1:6;
then
A55: sqrt((r/2)^2 + 0^2)<=sqrt((r/2)^2 + (r/2)^2) by A54,SQUARE_1:26
;
A56: p`1=r2 & p`2=s2 by A33,EUCLID:52;
(r/2)^2 + (r/2)^2= 2*((r/2)^2)
.=(sqrt 2)^2*((r/2)^2) by SQUARE_1:def 2
.=(r/2*sqrt 2)^2;
then sqrt ((r/2)^2 + (r/2)^2) =r*((sqrt 2)/2) by A8,Lm1,
SQUARE_1:22;
then dist(u,u0) = (Pitag_dist 2).(v,v0) & sqrt((r2 - r3)^2 +
(s2 - s3)^2) {} by A9,A51,XBOOLE_0:def 4;
end;
case
A57: s2=G*(1,j+1)`2;
A58: p`1=r2 & p`2=s2 by A33,EUCLID:52;
sqrt 2/2<1 by Lm1,SQUARE_1:21,XREAL_1:189;
then
A59: r*(sqrt 2/2)0 by XREAL_1:50;
then
A64: rm>0 by A8,XXREAL_0:21;
then s3=G*(1,j+1)`2-rl/2 by XREAL_1:10;
r*2">0 by A8,XREAL_1:129;
then r3G*(1,j+1)`2-(G*(1
,j+1)`2-G*(1,j)`2)/2 -(G*(1,j+1)`2-G*(1,j)`2)/2 by A63,XREAL_1:44,139;
then s3>G*(1,j)`2 by A57,A68,XXREAL_0:2;
then u0 in { |[r1,s1]| : r1 < G*(1,1)`1 & G*(1,j)`2 {} by A9,A67,XBOOLE_0:def 4;
end;
end;
hence Y /\ G0 <> {}(TOP-REAL 2);
end;
case
A70: i=len G & j=0;
then p in { |[r2,s2]| : r2 >= G*(len G,1)`1 & G*(1,1)`2 >=s2 } by
A3,Th27;
then consider r2,s2 such that
A71: p=|[r2,s2]| and
A72: r2 >= G*(len G,1)`1 and
A73: G*(1,1)`2>=s2;
set r3=r2+r/2,s3=s2-r/2;
A74: r*2">0 by A8,XREAL_1:129;
then r3>r2 by XREAL_1:29;
then
A75: r3>G*(len G,1)`1 by A72,XXREAL_0:2;
reconsider q0=|[r3,s3]| as Point of TOP-REAL 2;
reconsider u0=q0 as Point of Euclid 2 by EUCLID:22;
s3 G*(len G,1)`1 & G*(1,1)`2>s1 } by A75
;
then
A76: u0 in Y by A70,GOBOARD6:21;
reconsider v0=u0 as Element of REAL 2;
A77: q0`1=r3 & q0`2=s3 by EUCLID:52;
sqrt 2/2<1 by Lm1,SQUARE_1:21,XREAL_1:189;
then
A78: r*(sqrt 2/2) {} by A9,A76,XBOOLE_0:def 4;
end;
case
A80: i=len G & j=width G;
sqrt 2/2<1 by Lm1,SQUARE_1:21,XREAL_1:189;
then
A81: r*(sqrt 2/2)0 by A8,XREAL_1:129;
then s2G*(1,width G)`2 by A85,XXREAL_0:2;
reconsider q0=|[r3,s3]| as Point of TOP-REAL 2;
reconsider u0=q0 as Point of Euclid 2 by EUCLID:22;
r2G*(len G,1)`1 by A84,XXREAL_0:2;
then u0 in { |[r1,s1]| : r1 > G*(len G,1)`1 & s1 > G*(1,width G)
`2 } by A87;
then
A88: u0 in Y by A80,GOBOARD6:22;
reconsider v0=u0 as Element of REAL 2;
A89: q0`1=r3 & q0`2=s3 by EUCLID:52;
A90: (-r/2)^2=(r/2)^2 & dist(u,u0) = (Pitag_dist 2).(v,v0) by
METRIC_1:def 1;
A91: r2-r3=-r/2 & s2-s3=-r/2;
p`1=r2 & p`2=s2 by A83,EUCLID:52;
then dist(u,u0) < r by A89,A91,A90,A81,A82,TOPREAL3:7;
then u0 in Ball(u,r) by METRIC_1:11;
hence Y /\ G0 <> {} by A9,A88,XBOOLE_0:def 4;
end;
case
A92: i=len G & 1<=j & j= G*(len G,1)`1 & G*(1,j)`2 <=s2 & s2
<=G*(1,j+1)`2} by A3,Th29;
then consider r2,s2 such that
A93: p=|[r2,s2]| and
A94: r2 >= G*(len G,1)`1 and
A95: G*(1,j)`2 <=s2 and
A96: s2<=G*(1,j+1)`2;
now
per cases by A95,A96,XXREAL_0:1;
case
A97: s2=G*(1,j)`2;
A98: p`1=r2 & p`2=s2 by A93,EUCLID:52;
sqrt 2/2<1 by Lm1,SQUARE_1:21,XREAL_1:189;
then
A99: r*(sqrt 2/2)0 by XREAL_1:50;
then
A104: rm>0 by A8,XXREAL_0:21;
then s3>s2 by XREAL_1:29,139;
then
A105: s3>G*(1,j)`2 by A95,XXREAL_0:2;
rm/2<=r/2 by XREAL_1:72,XXREAL_0:17;
then (rm/2)^2<=(r/2)^2 by A104,SQUARE_1:15;
then
A106: (r/2)^2+(rm/2)^2<=(r/2)^2+(r/2)^2 by XREAL_1:7;
0<=(rm/2)^2 & 0<=(r/2)^2 by XREAL_1:63;
then sqrt((r/2)^2+(rm/2)^2)<=sqrt((r/2)^2+(r/2) ^2 ) by A106,
SQUARE_1:26;
then dist(u,u0) = (Pitag_dist 2).(v,v0) & sqrt ((r2 - r3)^2 +
(s2 - s3)^2)0 by A8,XREAL_1:129;
then r2G*(len G,1)`1 by A94,XXREAL_0:2;
G*(1,j)`2+(G*(1,j+1)`2-G*(1,j)`2)/2 G*(len G,1)`1 & G*(1,j)`2 {} by A9,A107,XBOOLE_0:def 4;
end;
case
A110: G*(1,j)`2 0 by A8,XREAL_1:129;
then r2G*(len G,1)`1 by A94,XXREAL_0:2;
then u0 in { |[r1,s1]| : r1 > G*(len G,1)`1 & G*(1,j)`2=0 by XREAL_1:63;
then (r/2)^2 + 0 <=(r/2)^2 + (r/2)^2 by XREAL_1:6;
then
A115: sqrt((r/2)^2 + 0^2)<=sqrt((r/2)^2 + (r/2)^2) by A114,
SQUARE_1:26;
A116: p`1=r2 & p`2=s2 by A93,EUCLID:52;
(r/2)^2 + (r/2)^2= 2*((r/2)^2)
.=(sqrt 2)^2*((r/2)^2) by SQUARE_1:def 2
.=(r/2*sqrt 2)^2;
then sqrt ((r/2)^2 + (r/2)^2) =r*((sqrt 2)/2) by A8,Lm1,
SQUARE_1:22;
then dist(u,u0) = (Pitag_dist 2).(v,v0) & sqrt((r2 - r3)^2 +
(s2 - s3)^2) {} by A9,A111,XBOOLE_0:def 4;
end;
case
A117: s2=G*(1,j+1)`2;
A118: p`1=r2 & p`2=s2 by A93,EUCLID:52;
sqrt 2/2<1 by Lm1,SQUARE_1:21,XREAL_1:189;
then
A119: r*(sqrt 2/2)0 by XREAL_1:50;
then
A124: rm>0 by A8,XXREAL_0:21;
then s3=G*(1,j+1)`2-rl/2 by XREAL_1:10;
r*2">0 by A8,XREAL_1:129;
then r2G*(len G,1)`1 by A94,XXREAL_0:2;
G*(1,j+1)`2-(G*(1,j+1)`2-G*(1,j)`2)/2 >G*(1,j+1)`2-(G*(1
,j+1)`2-G*(1,j)`2)/2 -(G*(1,j+1)`2-G*(1,j)`2)/2 by A123,XREAL_1:44,139;
then s3>G*(1,j)`2 by A117,A128,XXREAL_0:2;
then u0 in { |[r1,s1]| : r1 > G*(len G,1)`1 & G*(1,j)`2 {}(TOP-REAL 2) by A9,A127,XBOOLE_0:def 4;
end;
end;
hence Y /\ G0 <> {}(TOP-REAL 2);
end;
case
A130: 1<=i & i0 by XREAL_1:50;
then
A140: sm>0 by A8,XXREAL_0:21;
then r3>r2 by XREAL_1:29,139;
then
A141: r3>G*(i,1)`1 by A132,XXREAL_0:2;
sqrt 2/2<1 by Lm1,SQUARE_1:21,XREAL_1:189;
then
A142: r*(sqrt 2/2)0 by A8,XREAL_1:129;
then s3 {}(TOP-REAL 2) by A9,A145,XBOOLE_0:def 4;
end;
case
A148: G*(i,1)`1 0 by A8,XREAL_1:129;
then s3=0 by XREAL_1:63;
then 0^2 + (r/2)^2 <=(r/2)^2 + (r/2)^2 by XREAL_1:6;
then
A153: sqrt(0^2 + (r/2)^2 )<=sqrt((r/2)^2 + (r/2)^2) by A152,
SQUARE_1:26;
A154: p`1=r2 & p`2=s2 by A131,EUCLID:52;
(r/2)^2 + (r/2)^2= 2*((r/2)^2)
.=(sqrt 2)^2*((r/2)^2) by SQUARE_1:def 2
.=(r/2*sqrt 2)^2;
then sqrt ((r/2)^2 + (r/2)^2) =r*((sqrt 2)/2) by A8,Lm1,
SQUARE_1:22;
then dist(u,u0) = (Pitag_dist 2).(v,v0) & sqrt((r2 - r3)^2 +
(s2 - s3)^2 ) {}(TOP-REAL 2) by A9,A149,XBOOLE_0:def 4;
end;
case
A155: r2=G*(i+1,1)`1;
(r/2)^2 + (r/2)^2= 2*((r/2)^2)
.=(sqrt 2)^2*((r/2)^2) by SQUARE_1:def 2
.=(r/2*sqrt 2)^2;
then
A156: sqrt ((r/2)^2 + (r/2)^2) =r*((sqrt 2)/2) by A8,Lm1,SQUARE_1:22;
set sl=G*(i+1,1)`1 - G*(i,1)`1;
set sm=min(r,sl);
set s3=s2-r/2,r3=r2-sm/2;
reconsider q0=|[r3,s3]| as Point of TOP-REAL 2;
A157: q0`1=r3 & q0`2=s3 by EUCLID:52;
reconsider u0=q0 as Point of Euclid 2 by EUCLID:22;
reconsider v0=u0 as Element of REAL 2;
A158: 1<=width G by Th34;
i*0 by XREAL_1:50;
then
A160: sm>0 by A8,XXREAL_0:21;
then r3=G*(i+1,1)`1-sl/2 by XREAL_1:10;
r*2">0 by A8,XREAL_1:129;
then s3G*(i+1,1)`1-(G*(i
+1,1)`1-G*(i,1)`1)/2 -(G*(i+1,1)`1-G*(i,1)`1)/2 by A159,XREAL_1:44,139;
then r3>G*(i,1)`1 by A155,A166,XXREAL_0:2;
then u0 in { |[r1,s1]| : G*(i,1)`1 {}(TOP-REAL 2) by A9,A165,XBOOLE_0:def 4;
end;
end;
hence Y /\ G0 <> {}(TOP-REAL 2);
end;
case
A168: 1<=i & i=G*
(1,width G)`2} by A3,Th31;
then consider r2,s2 such that
A169: p=|[r2,s2]| and
A170: G*(i,1)`1 <=r2 and
A171: r2<=G*(i+1,1)`1 and
A172: s2>=G*(1,width G)`2;
now
per cases by A170,A171,XXREAL_0:1;
case
A173: r2=G*(i,1)`1;
A174: p`1=r2 & p`2=s2 by A169,EUCLID:52;
sqrt 2/2<1 by Lm1,SQUARE_1:21,XREAL_1:189;
then
A175: r*(sqrt 2/2)0 by XREAL_1:50;
then
A180: rm>0 by A8,XXREAL_0:21;
then r3>r2 by XREAL_1:29,139;
then
A181: r3>G*(i,1)`1 by A170,XXREAL_0:2;
rm/2<=r/2 by XREAL_1:72,XXREAL_0:17;
then (rm/2)^2<=(r/2)^2 by A180,SQUARE_1:15;
then
A182: (r/2)^2+(rm/2)^2<=(r/2)^2+(r/2)^2 by XREAL_1:7;
0<=(rm/2)^2 & 0<=(r/2)^2 by XREAL_1:63;
then sqrt((r/2)^2+(rm/2)^2)<=sqrt((r/2)^2+(r/2) ^2 ) by A182,
SQUARE_1:26;
then dist(u,u0) = (Pitag_dist 2).(v,v0) & sqrt ((r2 - r3)^2 +
(s2 - s3)^2)0 by A8,XREAL_1:129;
then s2G*(1,width G)`2 by A172,XXREAL_0:2;
G*(i,1)`1+(G*(i+1,1)`1-G*(i,1)`1)/2
G*(1,width G)`2 } by A185,A181;
then u0 in Y by A168,GOBOARD6:25;
hence Y /\ G0 <> {}(TOP-REAL 2) by A9,A183,XBOOLE_0:def 4;
end;
case
A186: G*(i,1)`1 0 by A8,XREAL_1:129;
then s2G*(1,width G)`2 by A172,XXREAL_0:2;
then u0 in { |[r1,s1]| : G*(i,1)`1
G*(1,width G)`2 } by A186;
then
A187: u0 in Y by A168,GOBOARD6:25;
reconsider v0=u0 as Element of REAL 2;
A188: q0`1=r3 & q0`2=s3 by EUCLID:52;
sqrt 2/2<1 by Lm1,SQUARE_1:21,XREAL_1:189;
then
A189: r*(sqrt 2/2)=0 by XREAL_1:63;
then (r/2)^2 + 0^2 <=(r/2)^2 + (r/2)^2 by XREAL_1:6;
then
A191: sqrt((r/2)^2 + 0^2)<=sqrt((r/2)^2 + (r/2)^2) by A190,
SQUARE_1:26;
A192: p`1=r2 & p`2=s2 by A169,EUCLID:52;
(r/2)^2 + (r/2)^2= 2*((r/2)^2)
.=(sqrt 2)^2*((r/2)^2) by SQUARE_1:def 2
.=(r/2*sqrt 2)^2;
then sqrt ((r/2)^2 + (r/2)^2) =r*((sqrt 2)/2) by A8,Lm1,
SQUARE_1:22;
then dist(u,u0) = (Pitag_dist 2).(v,v0) & sqrt((r2 - r3)^2 +
(s2 - s3)^2) {}(TOP-REAL 2) by A9,A187,XBOOLE_0:def 4;
end;
case
A193: r2=G*(i+1,1)`1;
A194: p`1=r2 & p`2=s2 by A169,EUCLID:52;
sqrt 2/2<1 by Lm1,SQUARE_1:21,XREAL_1:189;
then
A195: r*(sqrt 2/2)0 by XREAL_1:50;
then
A200: rm>0 by A8,XXREAL_0:21;
then r3=G*(i+1,1)`1-rl/2 by XREAL_1:10;
r*2">0 by A8,XREAL_1:129;
then s3>s2 by XREAL_1:29;
then
A205: s3>G*(1,width G)`2 by A172,XXREAL_0:2;
G*(i+1,1)`1-(G*(i+1,1)`1-G*(i,1)`1)/2 >G*(i+1,1)`1-(G*(i
+1,1)`1-G*(i,1)`1)/2 -(G*(i+1,1)`1-G*(i,1)`1)/2 by A199,XREAL_1:44,139;
then r3>G*(i,1)`1 by A193,A204,XXREAL_0:2;
then u0 in { |[r1,s1]| : G*(i,1)`1
G*(1,width G)`2} by A205,A201;
then u0 in Y by A168,GOBOARD6:25;
hence Y /\ G0 <> {}(TOP-REAL 2) by A9,A203,XBOOLE_0:def 4;
end;
end;
hence Y /\ G0 <> {}(TOP-REAL 2);
end;
case
A206: 1<=i & i0 by XREAL_1:50;
then
A215: rm1>0 by A8,XXREAL_0:21;
then r3>r2 by XREAL_1:29,139;
then
A216: r3>G*(i,1)`1 by A208,XXREAL_0:2;
rm1/2<=rl1/2 by XREAL_1:72,XXREAL_0:17;
then
A217: G*(i,1)`1+rm1/2<=G*(i,1)`1+rl1/2 by XREAL_1:6;
G*(i,1)`1+(G*(i+1,1)`1-G*(i,1)`1)/2 0 by XREAL_1:50;
then
A223: rm>0 by A8,XXREAL_0:21;
then s3>s2 by XREAL_1:29,139;
then
A224: s3>G*(1,j)`2 by A210,XXREAL_0:2;
rm1/2<=r/2 by XREAL_1:72,XXREAL_0:17;
then
A225: (rm1/2)^2<=(r/2)^2 by A215,SQUARE_1:15;
rm/2<=r/2 by XREAL_1:72,XXREAL_0:17;
then (rm/2)^2<=(r/2)^2 by A223,SQUARE_1:15;
then
A226: (rm1/2)^2+(rm/2)^2<=(r/2)^2+(r/2)^2 by A225,XREAL_1:7;
sqrt 2/2<1 by Lm1,SQUARE_1:21,XREAL_1:189;
then
A227: r*(sqrt 2/2) {}(TOP-REAL 2) by A9,A230,XBOOLE_0:def 4;
end;
case
A231: r2=G*(i,1)`1 & G*(1,j)`2 0 by XREAL_1:50;
then
A234: rm1>0 by A8,XXREAL_0:21;
then
A235: r3>r2 by XREAL_1:29,139;
rm1/2<=rl1/2 by XREAL_1:72,XXREAL_0:17;
then
A236: G*(i,1)`1+rm1/2<=G*(i,1)`1+rl1/2 by XREAL_1:6;
G*(i,1)`1+(G*(i+1,1)`1-G*(i,1)`1)/2 =0 by XREAL_1:63;
then (r/2)^2 + 0^2 <=(r/2)^2 + (r/2)^2 by XREAL_1:6;
then
A243: sqrt((r/2)^2 + 0^2)<=sqrt((r/2)^2 + (r/2)^2) by A242,
SQUARE_1:26;
(r/2)^2 + (r/2)^2= 2*((r/2)^2)
.=(sqrt 2)^2*((r/2)^2) by SQUARE_1:def 2
.=(r/2*sqrt 2)^2;
then sqrt ((r/2)^2 + (r/2)^2) =r*((sqrt 2)/2) by A8,Lm1,
SQUARE_1:22;
then sqrt((r/2)^2 + 0^2) {}(TOP-REAL 2) by A9,A237,XBOOLE_0:def 4;
end;
case
A245: r2=G*(i,1)`1 & s2=G*(1,j+1)`2;
set rl1=G*(i+1,1)`1 - G*(i,1)`1;
set rl=G*(1,j+1)`2 - G*(1,j)`2;
set rm=min(r,rl);
set rm1=min(r,rl1);
set r3=r2+rm1/2,s3=s2-rm/2;
A246: 1<=width G by Th34;
i**0 by XREAL_1:50;
then
A248: rm1>0 by A8,XXREAL_0:21;
then r3>r2 by XREAL_1:29,139;
then
A249: r3>G*(i,1)`1 by A208,XXREAL_0:2;
rm1/2<=rl1/2 by XREAL_1:72,XXREAL_0:17;
then
A250: G*(i,1)`1+rm1/2<=G*(i,1)`1+rl1/2 by XREAL_1:6;
G*(i,1)`1+(G*(i+1,1)`1-G*(i,1)`1)/2 =G*(1,j+1)`2-rl/2 by XREAL_1:13;
reconsider q0=|[r3,s3]| as Point of TOP-REAL 2;
A253: q0`1=r3 & q0`2=s3 by EUCLID:52;
reconsider u0=q0 as Point of Euclid 2 by EUCLID:22;
reconsider v0=u0 as Element of REAL 2;
A254: 1<=len G by Th34;
j0 by XREAL_1:50;
then
A256: rm>0 by A8,XXREAL_0:21;
then s3G*(1,j+1)`2-(G*(1
,j+1)`2-G*(1,j)`2)/2 -(G*(1,j+1)`2-G*(1,j)`2)/2 by A255,XREAL_1:44,139;
then s3>G*(1,j)`2 by A245,A252,XXREAL_0:2;
then u0 in { |[r1,s1]| : G*(i,1)`1 < r1 & r1 < G*(i+1,1)`1 &
G*(1,j)`2 < s1 & s1 < G*(1,j+1)`2 } by A257,A249,A251;
then u0 in Y by A206,GOBOARD6:26;
hence Y /\ G0 <> {}(TOP-REAL 2) by A9,A263,XBOOLE_0:def 4;
end;
case
A264: G*(i,1)`1 0 by XREAL_1:50;
then
A267: rm>0 by A8,XXREAL_0:21;
then
A268: s3>s2 by XREAL_1:29,139;
rm/2<=rl/2 by XREAL_1:72,XXREAL_0:17;
then
A269: G*(1,j)`2+rm/2<=G*(1,j)`2+rl/2 by XREAL_1:6;
G*(1,j)`2+(G*(1,j+1)`2-G*(1,j)`2)/2 =0 by XREAL_1:63;
then 0^2+(r/2)^2 <=(r/2)^2 + (r/2)^2 by XREAL_1:6;
then
A276: sqrt
(0^2+(r/2)^2 )<=sqrt((r/2)^2 + (r/2)^2) by A275,SQUARE_1:26;
(r/2)^2 + (r/2)^2= 2*((r/2)^2)
.=(sqrt 2)^2*((r/2)^2) by SQUARE_1:def 2
.=(r/2*sqrt 2)^2;
then sqrt ((r/2)^2 + (r/2)^2) =r*((sqrt 2)/2) by A8,Lm1,
SQUARE_1:22;
then sqrt(0^2+(r/2)^2) {}(TOP-REAL 2) by A9,A270,XBOOLE_0:def 4;
end;
case
A278: G*(i,1)`1 {}(TOP-REAL 2) by A9,A280,XBOOLE_0:def 4;
end;
case
A281: G*(i,1)`1 0 by XREAL_1:50;
then
A284: rm>0 by A8,XXREAL_0:21;
then
A285: s3=G*(1,j+1)`2-rl/2 by XREAL_1:13;
G*(1,j+1)`2-(G*(1,j+1)`2-G*(1,j)`2)/2 >G*(1,j+1)`2-(G*(1
,j+1)`2-G*(1,j)`2)/2 -(G*(1,j+1)`2-G*(1,j)`2)/2 by A283,XREAL_1:44,139;
then s3>G*(1,j)`2 by A281,A286,XXREAL_0:2;
then u0 in { |[r1,s1]| : G*(i,1)`1 < r1 & r1 < G*(i+1,1)`1 &
G*(1,j)`2 < s1 & s1 < G* (1,j+1)`2 } by A281,A285;
then
A287: u0 in Y by A206,GOBOARD6:26;
sqrt 2/2<1 by Lm1,SQUARE_1:21,XREAL_1:189;
then
A288: r*(sqrt 2/2)=0 by XREAL_1:63;
then 0+(r/2)^2 <=(r/2)^2 + (r/2)^2 by XREAL_1:6;
then
A293: sqrt
(0^2+(r/2)^2 )<=sqrt((r/2)^2 + (r/2)^2) by A292,SQUARE_1:26;
(r/2)^2 + (r/2)^2= 2*((r/2)^2)
.=(sqrt 2)^2*((r/2)^2) by SQUARE_1:def 2
.=(r/2*sqrt 2)^2;
then sqrt ((r/2)^2 + (r/2)^2) =r*((sqrt 2)/2) by A8,Lm1,
SQUARE_1:22;
then sqrt(0^2+(r/2)^2) {}(TOP-REAL 2) by A9,A287,XBOOLE_0:def 4;
end;
case
A295: r2=G*(i+1,1)`1 & s2=G*(1,j)`2;
set rl1=G*(i+1,1)`1 - G*(i,1)`1;
set rl=G*(1,j+1)`2 - G*(1,j)`2;
set rm=min(r,rl);
set rm1=min(r,rl1);
set r3=r2-rm1/2,s3=s2+rm/2;
A296: 1<=width G by Th34;
i**0 by XREAL_1:50;
then
A298: rm1>0 by A8,XXREAL_0:21;
then r3=G*(i+1,1)`1-rl1/2 by XREAL_1:13;
G*(i+1,1)`1-(G*(i+1,1)`1-G*(i,1)`1)/2 >G*(i+1,1)`1-(G*(i
+1,1)`1-G*(i,1)`1)/2 -(G*(i+1,1)`1-G*(i,1)`1)/2 by A297,XREAL_1:44,139;
then
A301: r3>G*(i,1)`1 by A295,A300,XXREAL_0:2;
rm/2<=rl/2 by XREAL_1:72,XXREAL_0:17;
then
A302: G*(1,j)`2+rm/2<=G*(1,j)`2+rl/2 by XREAL_1:6;
reconsider q0=|[r3,s3]| as Point of TOP-REAL 2;
A303: q0`1=r3 & q0`2=s3 by EUCLID:52;
reconsider u0=q0 as Point of Euclid 2 by EUCLID:22;
reconsider v0=u0 as Element of REAL 2;
A304: 1<=len G by Th34;
j0 by XREAL_1:50;
then
A306: rm>0 by A8,XXREAL_0:21;
then s3>s2 by XREAL_1:29,139;
then
A307: s3>G*(1,j)`2 by A210,XXREAL_0:2;
rm1/2<=r/2 by XREAL_1:72,XXREAL_0:17;
then
A308: (rm1/2)^2<=(r/2)^2 by A298,SQUARE_1:15;
rm/2<=r/2 by XREAL_1:72,XXREAL_0:17;
then (rm/2)^2<=(r/2)^2 by A306,SQUARE_1:15;
then
A309: (rm1/2)^2+(rm/2)^2<=(r/2)^2+(r/2)^2 by A308,XREAL_1:7;
sqrt 2/2<1 by Lm1,SQUARE_1:21,XREAL_1:189;
then
A310: r*(sqrt 2/2) {}(TOP-REAL 2) by A9,A313,XBOOLE_0:def 4;
end;
case
A314: r2=G*(i+1,1)`1 & G*(1,j)`2 0 by XREAL_1:50;
then
A317: rm1>0 by A8,XXREAL_0:21;
then
A318: r3=G*(i+1,1)`1-rl1/2 by XREAL_1:13;
G*(i+1,1)`1-(G*(i+1,1)`1-G*(i,1)`1)/2 >G*(i+1,1)`1-(G*(i
+1,1)`1-G*(i,1)`1)/2 -(G*(i+1,1)`1-G*(i,1)`1)/2 by A316,XREAL_1:44,139;
then r3>G*(i,1)`1 by A314,A319,XXREAL_0:2;
then u0 in { |[r1,s1]| : G*(i,1)`1 < r1 & r1 < G*(i+1,1)`1 &
G*(1,j)`2 < s1 & s1 < G* (1,j+1)`2 } by A314,A318;
then
A320: u0 in Y by A206,GOBOARD6:26;
sqrt 2/2<1 by Lm1,SQUARE_1:21,XREAL_1:189;
then
A321: r*(sqrt 2/2)=0 by XREAL_1:63;
then (r/2)^2+0 <=(r/2)^2 + (r/2)^2 by XREAL_1:6;
then
A326: sqrt
((r/2)^2+0^2 )<=sqrt((r/2)^2 + (r/2)^2) by A325,SQUARE_1:26;
(r/2)^2 + (r/2)^2= 2*((r/2)^2)
.=(sqrt 2)^2*((r/2)^2) by SQUARE_1:def 2
.=(r/2*sqrt 2)^2;
then sqrt ((r/2)^2 + (r/2)^2) =r*((sqrt 2)/2) by A8,Lm1,
SQUARE_1:22;
then sqrt((r/2)^2+0^2) {}(TOP-REAL 2) by A9,A320,XBOOLE_0:def 4;
end;
case
A328: r2=G*(i+1,1)`1 & s2=G*(1,j+1)`2;
set rl1=G*(i+1,1)`1 - G*(i,1)`1;
set rl=G*(1,j+1)`2 - G*(1,j)`2;
set rm=min(r,rl);
set rm1=min(r,rl1);
set r3=r2-rm1/2,s3=s2-rm/2;
A329: 1<=width G by Th34;
i**0 by XREAL_1:50;
then
A331: rm1>0 by A8,XXREAL_0:21;
then r3=G*(i+1,1)`1-rl1/2 by XREAL_1:13;
G*(i+1,1)`1-(G*(i+1,1)`1-G*(i,1)`1)/2 >G*(i+1,1)`1-(G*(i
+1,1)`1-G*(i,1)`1)/2 -(G*(i+1,1)`1-G*(i,1)`1)/2 by A330,XREAL_1:44,139;
then
A334: r3>G*(i,1)`1 by A328,A333,XXREAL_0:2;
rm/2<=rl/2 by XREAL_1:72,XXREAL_0:17;
then
A335: G*(1,j+1)`2-rm/2>=G*(1,j+1)`2-rl/2 by XREAL_1:13;
sqrt 2/2<1 by Lm1,SQUARE_1:21,XREAL_1:189;
then
A336: r*(sqrt 2/2)0 by XREAL_1:50;
then
A344: rm>0 by A8,XXREAL_0:21;
then s3G*(1,j+1)`2-(G*(1
,j+1)`2-G*(1,j)`2)/2 -(G*(1,j+1)`2-G*(1,j)`2)/2 by A343,XREAL_1:44,139;
then s3>G*(1,j)`2 by A328,A335,XXREAL_0:2;
then u0 in { |[r1,s1]| : G*(i,1)`1 < r1 & r1 < G*(i+1,1)`1 &
G*(1,j)`2 < s1 & s1 < G*(1,j+1)`2 } by A345,A332,A334;
then u0 in Y by A206,GOBOARD6:26;
hence Y /\ G0 <> {}(TOP-REAL 2) by A9,A347,XBOOLE_0:def 4;
end;
end;
hence Y /\ G0 <> {}(TOP-REAL 2);
end;
end;
hence Y /\ G0 <> {}(TOP-REAL 2);
end;
hence thesis;
end;
hence thesis by PRE_TOPC:def 7;
end;
Cl Y c= Cl cell(G,i,j) & cell(G,i,j) is closed by Th33,PRE_TOPC:19,TOPS_1:16;
then Cl Y c= cell(G,i,j) by PRE_TOPC:22;
hence thesis by A2;
end;
*