:: Some Topological Properties of Cells in $R^2$
:: by Yatsuka Nakamura and Andrzej Trybulec
::
:: Received July 22, 1996
:: Copyright (c) 1996-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, 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 & $1<len GoB f implies (
GoB f)*($1+1,1)`1<=r);
1<len GoB f by GOBOARD7:32;
then 1+1<=len GoB f by NAT_1:13;
then
A4: 1+1-1<=l-1 by XREAL_1:9;
assume
A5: not ex j st 1<=j & j<len GoB f & (GoB f)*(j,1)`1<=r & r<(GoB f
)*(j+1,1)`1;
A6: for k holds P[k] implies P[k+1]
proof
let k;
assume
A7: k=0 or ( 1<=k & k<len GoB f implies (GoB f)*(k+1,1)`1<=r);
1<=k+1 & k+1<len GoB f implies (GoB f)*(k+1+1,1)`1<=r
proof
assume
A8: 1<=k+1 & k+1<len GoB f;
now
assume
A9: r< (GoB f)*(k+1+1,1)`1;
then k<>0 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-1<l-1+1 by XREAL_1:29;
then reconsider l1=l-1 as Nat by A4,SPPOL_1:2;
0<l1 by A4;
hence contradiction by A3,A11,A4,A12;
end;
hence
ex j st 1<=j & j<len GoB f & (GoB f)*(j,1)`1<=r & r<(GoB f)*(j+1,1) `1;
end;
now
per cases by A1;
case
A13: r<(GoB f)*(1,1)`1;
reconsider G=GoB f as Go-board;
1 <= width G by GOBOARD7:33;
then
A14: v_strip(G,0) = { |[r1,s]| where r1,s is Real : r1 <= G*(1,1)`1 }
by GOBOARD5:10;
|[r,p`2]| in { |[r1,s]| where r1,s is Real : r1 <= (GoB f)*(1,1)`1 }
by A13;
then p in v_strip(GoB f,0) by A14,EUCLID:53;
hence ex j0 being Nat st j0<=j1 & x in v_strip(GoB f,j0);
end;
case
A15: (GoB f)*(len GoB f,1)`1 <=r;
reconsider G=GoB f as Go-board;
1 <= width G by GOBOARD7:33;
then
A16: v_strip(G,len G) = { |[r1,s]| where r1,s is Real : G*(len G,1)`1<=r1}
by GOBOARD5:9;
|[r,p`2]| in { |[r1,s]| where r1,s is Real : (GoB f)*(len G,1)`1 <=r1}
by A15;
then p in v_strip(GoB f,len GoB f) by A16,EUCLID:53;
hence ex j0 being Nat st j0<=j1 & x in v_strip(GoB f,j0);
end;
case
A17: ex j st 1<=j & j<len GoB f & (GoB f)*(j,1)`1<=r & r<(GoB f)*( j+1,1)`1;
reconsider G=GoB f as Go-board;
consider j such that
A18: 1<=j and
A19: j<len GoB f and
A20: (GoB f)*(j,1)`1<=r & r<(GoB f)*(j+1,1)`1 by A17;
A21: |[r,p`2]| in { |[r1,s]| where r1,s is Real:
G*(j,1)`1<=r1 & r1<=G* (j+1,1)`1 } by A20;
1 <= width G by GOBOARD7:33;
then v_strip(G,j) = { |[r1,s]| where r1,s is Real :
G*(j,1)`1<=r1 & r1<=G*(j+1,1)`1} by A18,A19,GOBOARD5:8;
then p in v_strip(GoB f,j) by A21,EUCLID:53;
hence ex j0 being Nat st j0<=j1 & x in v_strip(GoB f,j0) by
A19;
end;
end;
then consider j0 being Nat such that
A22: j0<=j1 and
A23: x in v_strip(GoB f,j0);
set s=p`2;
A24: now
assume that
A25: not s<(GoB f)*(1,1)`2 and
A26: not (GoB f)*(1,width GoB f)`2 <=s;
now
reconsider l=width GoB f as Nat;
defpred P[Nat] means $1=0 or (1<=$1 & $1<width GoB f
implies (GoB f)*(1,$1+1)`2<=s);
1<width GoB f by GOBOARD7:33;
then 1+1<=width GoB f by NAT_1:13;
then
A27: 1+1-1<=l-1 by XREAL_1:9;
assume
A28: not ex j st 1<=j & j<width GoB f & (GoB f)*(1,j)`2<=s & s<(
GoB f)*(1,j+1)`2;
A29: for k holds P[k] implies P[k+1]
proof
let k;
assume
A30: k=0 or ( 1<=k & k<width GoB f implies (GoB f)*(1,k+1)`2<=s);
1<=k+1 & k+1<width GoB f implies (GoB f)*(1,k+1+1)`2<=s
proof
assume
A31: 1<=k+1 & k+1<width GoB f;
now
assume
A32: s< (GoB f)*(1,k+1+1)`2;
then k<>0 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<l-1+1 by XREAL_1:29;
then reconsider l1=l-1 as Nat by A27,SPPOL_1:2;
0<l1 by A27;
hence contradiction by A26,A34,A27,A35;
end;
hence
ex j st 1<=j & j<width GoB f & (GoB f)*(1,j)`2<=s & s<(GoB f)*(1,j+
1) `2;
end;
now
per cases by A24;
case
A36: s<(GoB f)*(1,1)`2;
reconsider G=GoB f as Go-board;
1 <= len G by GOBOARD7:32;
then
A37: h_strip(G,0) = { |[r1,s1]| : s1 <= G*(1,1)`2 } by GOBOARD5:7;
|[r,s]| in { |[r1,s1]| : s1 <= (GoB f)*(1,1)`2 } by A36;
then p in h_strip(GoB f,0) by A37,EUCLID:53;
hence ex i0 being Nat st i0<=j2 & x in h_strip(GoB f,i0);
end;
case
A38: (GoB f)*(1,width GoB f)`2 <=s;
reconsider G=GoB f as Go-board;
1 <= len G by GOBOARD7:32;
then
A39: h_strip(G,width G) = { |[r1,s1]| : G*(1,width G)`2<=s1} by GOBOARD5:6;
|[r,s]| in { |[r1,s1]| : (GoB f)*(1,width G)`2 <=s1} by A38;
then p in h_strip(GoB f,width GoB f) by A39,EUCLID:53;
hence ex i0 being Nat st i0<=j2 & x in h_strip(GoB f,i0);
end;
case
A40: ex j st 1<=j & j<width GoB f & (GoB f)*(1,j)`2<=s & s<(GoB f)
*(1,j+1)`2;
reconsider G=GoB f as Go-board;
consider j such that
A41: 1<=j and
A42: j<width GoB f and
A43: (GoB f)*(1,j)`2<=s & s<(GoB f)*(1,j+1)`2 by A40;
A44: |[r,s]| in { |[r1,s1]| : G*(1,j)`2<=s1 & s1<=G* (1,j+1)`2 } by A43;
1 <= len G by GOBOARD7:32;
then h_strip(G,j) = { |[r1,s1]| : G*(1,j)`2<=s1 & s1<=G*(1,j+1)`2} by
A41,A42,GOBOARD5:5;
then p in h_strip(GoB f,j) by A44,EUCLID:53;
hence ex i0 being Nat st i0<=j2 & x in h_strip(GoB f,i0) by
A42;
end;
end;
then consider i0 being Nat such that
A45: i0<=j2 and
A46: x in h_strip(GoB f,i0);
reconsider X0=cell(GoB f,j0,i0) as set;
x in v_strip(GoB f,j0) /\ h_strip(GoB f,i0) by A23,A46,XBOOLE_0:def 4;
then
A47: x in X0 by GOBOARD5:def 3;
X0 in {cell(GoB f,i,j):i<=j1 & j<=j2} by A22,A45;
hence thesis by A47,TARSKI:def 4;
end;
let x be object;
assume x in union {cell(GoB f,i,j):i<=j1 & j<=j2};
then consider X0 being set such that
A48: x in X0 & X0 in {cell(GoB f,i,j):i<=j1 & j<=j2} by TARSKI:def 4;
ex i,j st X0=cell(GoB f,i,j) & i<=j1 & j<=j2 by A48;
hence thesis by A48;
end;
Lm3: 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;
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;
{ |[ 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;
Lm7: 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;
Lm8: for s1 holds { |[ sb,tb ]|: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;
Lm9: for s1 holds { |[ sb,tb ]|: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]| : s <= G*(1,j+1)`2 } by A1,GOBOARD5:def 2
;
hence thesis by Th12;
end;
hence thesis by A2;
end;
case
1 <= j & j < width G;
then
A3: h_strip(G,j) = { |[r,s]| : G*(1,j)`2 <= s & s <= G*(1,j+1)`2 } by
GOBOARD5:def 2;
reconsider P2={ |[r1,s1]| : s1<= G*(1,j+1)`2 } as Subset of TOP-REAL 2
by Lm5;
reconsider P1={ |[r1,s1]| : G*(1,j)`2 <= s1} as Subset of TOP-REAL 2 by
Lm3;
A4: { |[r,s]| : G*(1,j)`2 <= s & s <= G*(1,j+1)`2 }= { |[r1,s1]| : G*(1
,j)`2 <= s1} /\ {|[r2,s2]| : s2 <= G*(1,j+1)`2 }
proof
A5: { |[r1,s1]| : G*(1,j)`2 <= s1} /\ {|[r2,s2]| : s2 <= G*(1,j+1)`2
} c= { |[r,s]| : G*(1,j)`2 <= s & s <= G*(1,j+1)`2 }
proof
let x be object;
assume
A6: x in { |[r1,s1]| : G*(1,j)`2 <= s1} /\ {|[r2,s2]| : s2 <= G
* (1,j+1)`2 };
then
A7: x in { |[r1,s1]| : G*(1,j)`2 <= s1} by XBOOLE_0:def 4;
x in {|[r2,s2]| : s2 <= G*(1,j+1)`2 } by A6,XBOOLE_0:def 4;
then consider r2,s2 such that
A8: |[r2,s2]|=x and
A9: s2 <= G*(1,j+1)`2;
consider r1,s1 such that
A10: |[r1,s1]|=x and
A11: G*(1,j)`2 <= s1 by A7;
s1=s2 by A10,A8,SPPOL_2:1;
hence thesis by A10,A11,A9;
end;
A12: { |[r,s]| : G*(1,j)`2 <= s & s <= G*(1,j+1)`2 } c= {|[r1,s1]| : G
*(1,j)`2 <= s1 }
proof
let x be object;
assume x in { |[r,s]| : G*(1,j)`2 <= s & s <= G*(1,j+1)`2 };
then ex r,s st x=|[r,s]| & G*(1,j)`2 <= s & s <= G*(1,j+1)`2;
hence thesis;
end;
{ |[r,s]| : G*(1,j)`2 <= s & s <= G*(1,j+1)`2 } c= {|[r1,s1]| :
s1 <= G*(1,j+1)`2 }
proof
let x be object;
assume x in { |[r,s]| : G*(1,j)`2 <= s & s <= G*(1,j+1)`2 };
then ex r,s st x=|[r,s]| & G*(1,j)`2 <= s & s <= G*(1,j+1)`2;
hence thesis;
end;
then { |[r,s]| : G*(1,j)`2 <= s & s <= G*(1,j+1)`2 } c= { |[r1,s1]| :
G*(1,j)`2 <= s1} /\ {|[r2,s2]| : s2 <= G*(1,j+1)`2 } by A12,XBOOLE_1:19;
hence thesis by A5;
end;
P1 is closed & P2 is closed by Th12,Th13;
hence thesis by A3,A4,TOPS_1:8;
end;
case
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:
s <= G*(j+1,1)`1 } by A1,GOBOARD5:def 1;
hence thesis by Th14;
end;
hence thesis by A2;
end;
case
1 <= j & j < len G;
then
A3: v_strip(G,j) = { |[s,r]| where s,r is Real:
G*(j,1)`1 <= s & s <= G*(j+1,1)`1 } by GOBOARD5:def 1;
reconsider P2={ |[s1,r1]| where s1,r1 is Real:
s1<= G*(j+1,1)`1 } as Subset of TOP-REAL 2
by Lm7;
reconsider P1={ |[s1,r1]| where s1,r1 is Real:
G*(j,1)`1 <= s1} as Subset of TOP-REAL 2 by Lm9;
A4: { |[s,r]| where s,r is Real :
G*(j,1)`1 <= s & s <= G*(j+1,1)`1 }=
{ |[s1,r1]| where s1,r1 is Real: G*(j
,1)`1 <= s1} /\ {|[s2,r2]| where s2,r2 is Real: s2 <= G*(j+1,1)`1 }
proof
A5: { |[s1,r1]| where s1,r1 is Real: G*(j,1)`1 <= s1} /\
{|[s2,r2]| where s2,r2 is Real: s2 <= G*(j+1,1)`1
} c= { |[s,r]| where s,r is Real : G*(j,1)`1 <= s & s <= G*(j+1,1)`1 }
proof
let x be object;
assume
A6: x in { |[s1,r1]| where s1,r1 is Real :
G*(j,1)`1 <= s1} /\ {|[s2,r2]| where s2,r2 is Real: s2 <= G
* (j+1,1)`1 };
then
A7: x in {|[s2,r2]| where s2,r2 is Real : s2 <= G*(j+1,1)`1 }
by XBOOLE_0:def 4;
x in { |[s1,r1]| where s1,r1 is Real: G*(j,1)`1 <= s1}
by A6,XBOOLE_0:def 4;
then ex s1,r1 st |[s1,r1]|=x & G*(j,1)`1 <= s1;
then consider r1,s1 such that
A8: |[s1,r1]|=x and
A9: G*(j,1)`1 <= s1;
consider s2,r2 such that
A10: |[s2,r2]|=x and
A11: s2 <= G*(j+1,1)`1 by A7;
s1=s2 by A8,A10,SPPOL_2:1;
hence thesis by A8,A9,A11;
end;
A12: { |[s,r]| where s,r is Real: G*(j,1)`1 <= s & s <= G*(j+1,1)`1 } c=
{|[s1,r1]| where s1,r1 is Real: G*(j,1)`1 <= s1 }
proof
let x be object;
assume x in { |[s,r]| where s,r is Real:
G*(j,1)`1 <= s & s <= G*(j+1,1)`1 };
then ex s,r st x=|[s,r]| & G*(j,1)`1 <= s & s <= G*(j+1,1)`1;
hence thesis;
end;
{ |[s,r]| where s,r is Real:
G*(j,1)`1 <= s & s <= G*(j+1,1)`1 } c= {|[s1,r1]| where s1,r1 is Real:
s1 <= G*(j+1,1)`1 }
proof
let x be object;
assume x in { |[s,r]| where s,r is Real:
G*(j,1)`1 <= s & s <= G*(j+1,1)`1 };
then ex s,r st x=|[s,r]| & G*(j,1)`1 <= s & s <= G*(j+1,1)`1;
hence thesis;
end;
then { |[s,r]| where s,r is Real: G*(j,1)`1 <= s & s <= G*(j+1,1)`1 }
c=
{ |[s1,r1]| where s1,r1 is Real: G*(j,1)`1 <= s1} /\
{|[s2,r2]| where s2,r2 is Real: s2 <= G*(j+1,1)`1 } by A12,XBOOLE_1:19;
hence thesis by A5;
end;
P1 is closed & P2 is closed by Th14,Th15;
hence thesis by A3,A4,TOPS_1:8;
end;
case
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<s3+r/2 by XREAL_1:29;
then
A16: s3<G*(1,1)`2 by A14,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<r3+r/2 by A15,XREAL_1:29;
then r3<G*(1,1)`1 by A13,XXREAL_0:2;
then
u0 in { |[r1,s1]| : r1 < G*(1,1)`1 & s1 < G* (1,1)`2 } by A16;
then
A17: u0 in Y by A11,GOBOARD6:18;
reconsider v0=u0 as Element of REAL 2;
A18: q0`1=r3 & q0`2=s3 by EUCLID:52;
sqrt 2/2<1 by Lm1,SQUARE_1:21,XREAL_1:189;
then
A19: r*(sqrt 2/2)<r*1 by A8,XREAL_1:68;
(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
A20: sqrt ((r/2)^2 + (r/2)^2) =r*((sqrt 2)/2) by A8,Lm1,SQUARE_1:22;
A21: r2-r3 =r/2 & s2-s3=r/2;
p`1=r2 & p`2=s2 by A12,EUCLID:52;
then dist(u,u0) = (Pitag_dist 2).(v,v0) & (Pitag_dist 2).(v,v0)<r
by A18,A21,A19,A20,METRIC_1:def 1,TOPREAL3:7;
then u0 in Ball(u,r) by METRIC_1:11;
hence Y /\ G0 <> {}(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<r3+r/2 by A26,XREAL_1:29;
then r3<G*(1,1)`1 by A24,XXREAL_0:2;
then u0 in { |[r1,s1]| : r1 < G*(1,1)`1 & G*(1,width G)`2<s1 } by
A27;
then
A28: u0 in Y by A22,GOBOARD6:19;
reconsider v0=u0 as Element of REAL 2;
A29: q0`1=r3 & q0`2=s3 by EUCLID:52;
sqrt 2/2<1 by Lm1,SQUARE_1:21,XREAL_1:189;
then
A30: r*(sqrt 2/2)<r*1 by A8,XREAL_1:68;
(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
A31: dist(u,u0) = (Pitag_dist 2).(v,v0) & sqrt ((r2 - r3)^2 + (s2
- s3)^2)<r by A8,A30,Lm1,METRIC_1:def 1,SQUARE_1:22;
p`1=r2 & p`2=s2 by A23,EUCLID:52;
then dist(u,u0) < r by A29,A31,TOPREAL3:7;
then u0 in Ball(u,r) by METRIC_1:11;
hence Y /\ G0 <> {}(TOP-REAL 2) by A9,A28,XBOOLE_0:def 4;
end;
case
A32: i=0 & 1<=j & j<width G;
then
p in { |[r2,s2]| : r2 <= G*(1,1)`1 & G*(1,j)`2 <=s2 & s2<=G*(
1,j+1)`2} by A3,Th26;
then consider r2,s2 such that
A33: p=|[r2,s2]| and
A34: r2 <= G*(1,1)`1 and
A35: G*(1,j)`2 <=s2 and
A36: s2<=G*(1,j+1)`2;
now
per cases by A35,A36,XXREAL_0:1;
case
A37: s2=G*(1,j)`2;
A38: p`1=r2 & p`2=s2 by A33,EUCLID:52;
sqrt 2/2<1 by Lm1,SQUARE_1:21,XREAL_1:189;
then
A39: r*(sqrt 2/2)<r*1 by A8,XREAL_1:68;
(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
A40: sqrt ((r/2)^2 + (r/2)^2) =r*((sqrt 2)/2) by A8,Lm1,SQUARE_1:22;
set rl=G*(1,j+1)`2 - G*(1,j)`2;
set rm=min(r,rl);
set r3=r2-r/2 ,s3=s2+rm/2;
set q0=|[r3,s3]|;
A41: 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;
A42: 1<=len G by Th34;
j<j+1 & j+1<=width G by A32,NAT_1:13;
then G*(1,j)`2<G*(1,j+1)`2 by A32,A42,GOBOARD5:4;
then
A43: rl>0 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)<r by A39,A40,METRIC_1:def 1,XXREAL_0:2;
then dist(u,u0) < r by A38,A41,TOPREAL3:7;
then
A47: u0 in Ball(u,r) by METRIC_1:11;
rm/2<=rl/2 by XREAL_1:72,XXREAL_0:17;
then
A48: G*(1,j)`2+rm/2<=G*(1,j)`2+rl/2 by XREAL_1:6;
r*2">0 by A8,XREAL_1:129;
then r3<r3+r/2 by XREAL_1:29;
then
A49: r3<G*(1,1)`1 by A34,XXREAL_0:2;
G*(1,j)`2+(G*(1,j+1)`2-G*(1,j)`2)/2 <G*(1,j)`2+(G*(1,j+1)
`2-G*(1,j)`2)/2 +(G*(1,j+1)`2-G*(1,j)`2)/2 by A43,XREAL_1:29,139;
then s3<G*(1,j+1)`2 by A37,A48,XXREAL_0:2;
then
u0 in { |[r1,s1]| : r1 < G*(1,1)`1 & G*(1,j)`2<s1 & s1<G*
(1,j+1)`2} by A49,A45;
then u0 in Y by A32,GOBOARD6:20;
hence Y /\ G0 <> {}(TOP-REAL 2) by A9,A47,XBOOLE_0:def 4;
end;
case
A50: G*(1,j)`2 <s2 & s2<G*(1,j+1)`2;
set r3=r2-r/2,s3=s2;
reconsider q0=|[r3,s3]| as Point of TOP-REAL 2;
reconsider u0=q0 as Point of Euclid 2 by EUCLID:22;
r*2">0 by A8,XREAL_1:129;
then r3<r3+r/2 by XREAL_1:29;
then r3<G*(1,1)`1 by A34,XXREAL_0:2;
then u0 in { |[r1,s1]| : r1 < G*(1,1)`1 & G*(1,j)`2<s1 & s1<G
*(1,j+1)`2} by A50;
then
A51: u0 in Y by A32,GOBOARD6:20;
reconsider v0=u0 as Element of REAL 2;
A52: q0`1=r3 & q0`2=s3 by EUCLID:52;
sqrt 2/2<1 by Lm1,SQUARE_1:21,XREAL_1:189;
then
A53: r*(sqrt 2/2)<r*1 by A8,XREAL_1:68;
A54: (r/2)^2 >=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)<r by A53,A55,METRIC_1:def 1,XXREAL_0:2;
then dist(u,u0) < r by A56,A52,TOPREAL3:7;
then u0 in Ball(u,r) by METRIC_1:11;
hence Y /\ G0 <> {} 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)<r*1 by A8,XREAL_1:68;
(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
A60: sqrt ((r/2)^2 + (r/2)^2) =r*((sqrt 2)/2) by A8,Lm1,SQUARE_1:22;
set rl=G*(1,j+1)`2 - G*(1,j)`2;
set rm=min(r,rl);
set r3=r2-r/2,s3=s2-rm/2;
reconsider q0=|[r3,s3]| as Point of TOP-REAL 2;
A61: 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;
A62: 1<=len G by Th34;
j<j+1 & j+1<=width G by A32,NAT_1:13;
then G*(1,j)`2<G*(1,j+1)`2 by A32,A62,GOBOARD5:4;
then
A63: rl>0 by XREAL_1:50;
then
A64: rm>0 by A8,XXREAL_0:21;
then s3<s3+rm/2 by XREAL_1:29,139;
then
A65: s3<G*(1,j+1)`2 by A36,XXREAL_0:2;
rm/2<=r/2 by XREAL_1:72,XXREAL_0:17;
then (rm/2)^2<=(r/2)^2 by A64,SQUARE_1:15;
then
A66: (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 A66,
SQUARE_1:26;
then dist(u,u0) = (Pitag_dist 2).(v,v0) & sqrt ((r2 - r3)^2 +
(s2 - s3)^2)<r by A59,A60,METRIC_1:def 1,XXREAL_0:2;
then dist(u,u0) < r by A58,A61,TOPREAL3:7;
then
A67: u0 in Ball(u,r) by METRIC_1:11;
rm/2<=rl/2 by XREAL_1:72,XXREAL_0:17;
then
A68: G*(1,j+1)`2-rm/2>=G*(1,j+1)`2-rl/2 by XREAL_1:10;
r*2">0 by A8,XREAL_1:129;
then r3<r3+r/2 by XREAL_1:29;
then
A69: r3<G*(1,1)`1 by A34,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 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<s1 & s1<G
*(1,j+1)`2} by A69,A65;
then u0 in Y by A32,GOBOARD6:20;
hence Y /\ G0 <> {} 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<s3+r/2 by A74,XREAL_1:29;
then s3<G*(1,1)`2 by A73,XXREAL_0:2;
then u0 in { |[r1,s1]| : r1 > 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)<r*1 by A8,XREAL_1:68;
(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
A79: dist(u,u0) = (Pitag_dist 2).(v,v0) & sqrt ((r2 - r3)^2 + (s2
- s3)^2)<r by A8,A78,Lm1,METRIC_1:def 1,SQUARE_1:22;
p`1=r2 & p`2=s2 by A71,EUCLID:52;
then dist(u,u0) < r by A77,A79,TOPREAL3:7;
then u0 in Ball(u,r) by METRIC_1:11;
hence Y /\ G0 <> {} 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)<r*1 by A8,XREAL_1:68;
(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
A82: sqrt ((r/2)^2 + (r/2)^2) =r*((sqrt 2)/2) by A8,Lm1,SQUARE_1:22;
p in { |[r2,s2]| : G*(len G,1)`1<=r2 & G*(1,width G)`2<= s2
} by A3,A80,Th28;
then consider r2,s2 such that
A83: p=|[r2,s2]| and
A84: G*(len G,1)`1<=r2 and
A85: G*(1,width G)`2<=s2;
set r3=r2+r/2,s3=s2+r/2;
A86: r*2">0 by A8,XREAL_1:129;
then s2<s2+r/2 by XREAL_1:29;
then
A87: s3>G*(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;
r2<r2+r/2 by A86,XREAL_1:29;
then r3>G*(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<width G;
then p in { |[r2,s2]| : r2 >= 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)<r*1 by A8,XREAL_1:68;
(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
A100: sqrt ((r/2)^2 + (r/2)^2) =r*((sqrt 2)/2) by A8,Lm1,SQUARE_1:22;
set rl=G*(1,j+1)`2 - G*(1,j)`2;
set rm=min(r,rl);
set r3=r2+r/2 ,s3=s2+rm/2;
reconsider q0=|[r3,s3]| as Point of TOP-REAL 2;
A101: 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;
A102: 1<=len G by Th34;
j<j+1 & j+1<=width G by A92,NAT_1:13;
then G*(1,j)`2<G*(1,j+1)`2 by A92,A102,GOBOARD5:4;
then
A103: rl>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)<r by A99,A100,METRIC_1:def 1,XXREAL_0:2;
then dist(u,u0) < r by A98,A101,TOPREAL3:7;
then
A107: u0 in Ball(u,r) by METRIC_1:11;
rm/2<=rl/2 by XREAL_1:72,XXREAL_0:17;
then
A108: G*(1,j)`2+rm/2<=G*(1,j)`2+rl/2 by XREAL_1:6;
r*2">0 by A8,XREAL_1:129;
then r2<r2+r/2 by XREAL_1:29;
then
A109: r3>G*(len G,1)`1 by A94,XXREAL_0:2;
G*(1,j)`2+(G*(1,j+1)`2-G*(1,j)`2)/2 <G*(1,j)`2+(G*(1,j+1
)`2-G*(1,j)`2)/2 +(G*(1,j+1)`2-G*(1,j)`2)/2 by A103,XREAL_1:29,139;
then s3<G*(1,j+1)`2 by A97,A108,XXREAL_0:2;
then u0 in { |[r1,s1]| : r1 > G*(len G,1)`1 & G*(1,j)`2<s1 &
s1<G*(1,j+1)`2} by A109,A105;
then u0 in Y by A92,GOBOARD6:23;
hence Y /\ G0 <> {} by A9,A107,XBOOLE_0:def 4;
end;
case
A110: G*(1,j)`2 <s2 & s2<G*(1,j+1)`2;
set r3=r2+r/2,s3=s2;
reconsider q0=|[r3,s3]| as Point of TOP-REAL 2;
reconsider u0=q0 as Point of Euclid 2 by EUCLID:22;
r*2">0 by A8,XREAL_1:129;
then r2<r2+r/2 by XREAL_1:29;
then r3>G*(len G,1)`1 by A94,XXREAL_0:2;
then u0 in { |[r1,s1]| : r1 > G*(len G,1)`1 & G*(1,j)`2<s1 &
s1<G*(1,j+1)`2} by A110;
then
A111: u0 in Y by A92,GOBOARD6:23;
reconsider v0=u0 as Element of REAL 2;
A112: q0`1=r3 & q0`2=s3 by EUCLID:52;
sqrt 2/2<1 by Lm1,SQUARE_1:21,XREAL_1:189;
then
A113: r*(sqrt 2/2)<r*1 by A8,XREAL_1:68;
A114: (r/2)^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)<r by A113,A115,METRIC_1:def 1,XXREAL_0:2;
then dist(u,u0) < r by A116,A112,TOPREAL3:7;
then u0 in Ball(u,r) by METRIC_1:11;
hence Y /\ G0 <> {} 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)<r*1 by A8,XREAL_1:68;
(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
A120: sqrt ((r/2)^2 + (r/2)^2) =r*((sqrt 2)/2) by A8,Lm1,SQUARE_1:22;
set rl=G*(1,j+1)`2 - G*(1,j)`2;
set rm=min(r,rl);
set r3=r2+r/2,s3=s2-rm/2;
reconsider q0=|[r3,s3]| as Point of TOP-REAL 2;
A121: 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;
A122: 1<=len G by Th34;
j<j+1 & j+1<=width G by A92,NAT_1:13;
then G*(1,j)`2<G*(1,j+1)`2 by A92,A122,GOBOARD5:4;
then
A123: rl>0 by XREAL_1:50;
then
A124: rm>0 by A8,XXREAL_0:21;
then s3<s3+rm/2 by XREAL_1:29,139;
then
A125: s3<G*(1,j+1)`2 by A96,XXREAL_0:2;
rm/2<=r/2 by XREAL_1:72,XXREAL_0:17;
then (rm/2)^2<=(r/2)^2 by A124,SQUARE_1:15;
then
A126: (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 A126,
SQUARE_1:26;
then dist(u,u0) = (Pitag_dist 2).(v,v0) & sqrt ((r2 - r3)^2 +
(s2 - s3)^2)<r by A119,A120,METRIC_1:def 1,XXREAL_0:2;
then dist(u,u0) < r by A118,A121,TOPREAL3:7;
then
A127: u0 in Ball(u,r) by METRIC_1:11;
rm/2<=rl/2 by XREAL_1:72,XXREAL_0:17;
then
A128: G*(1,j+1)`2-rm/2>=G*(1,j+1)`2-rl/2 by XREAL_1:10;
r*2">0 by A8,XREAL_1:129;
then r2<r2+r/2 by XREAL_1:29;
then
A129: r3>G*(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<s1 &
s1<G*(1,j+1)`2} by A129,A125;
then u0 in Y by A92,GOBOARD6:23;
hence Y /\ G0 <> {}(TOP-REAL 2) by A9,A127,XBOOLE_0:def 4;
end;
end;
hence Y /\ G0 <> {}(TOP-REAL 2);
end;
case
A130: 1<=i & i<len G & j=0;
then p in { |[r2,s2]| : G*(i,1)`1 <=r2 & r2<=G*(i+1,1)`1 & s2 <=
G*(1,1)`2 } by A3,Th30;
then consider r2,s2 such that
A131: p=|[r2,s2]| and
A132: G*(i,1)`1 <=r2 and
A133: r2<=G*(i+1,1)`1 and
A134: s2 <= G*(1,1)`2;
now
per cases by A132,A133,XXREAL_0:1;
case
A135: r2=G*(i,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
A136: 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;
A137: 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;
A138: 1<=width G by Th34;
i<i+1 & i+1<=len G by A130,NAT_1:13;
then G*(i,1)`1<G*(i+1,1)`1 by A130,A138,GOBOARD5:3;
then
A139: sl>0 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)<r*1 by A8,XREAL_1:68;
sm/2<=r/2 by XREAL_1:72,XXREAL_0:17;
then (sm/2)^2<=(r/2)^2 by A140,SQUARE_1:15;
then
A143: (r/2)^2+(sm/2)^2<=(r/2)^2+(r/2)^2 by XREAL_1:7;
0<=(sm/2)^2 & 0<=(r/2)^2 by XREAL_1:63;
then
A144: sqrt((r/2)^2+(sm/2)^2)<=sqrt((r/2)^2+(r/2) ^2 ) by A143,
SQUARE_1:26;
p`1=r2 & p`2=s2 by A131,EUCLID:52;
then dist(u,u0) = (Pitag_dist 2).(v,v0) & sqrt ((p`1 - q0`1)
^2 + (p`2 - q0`2)^2)< r by A144,A137,A142,A136,METRIC_1:def 1,XXREAL_0:2;
then dist(u,u0) < r by TOPREAL3:7;
then
A145: u0 in Ball(u,r) by METRIC_1:11;
sm/2<=sl/2 by XREAL_1:72,XXREAL_0:17;
then
A146: G*(i,1)`1+sm/2<=G*(i,1)`1+sl/2 by XREAL_1:6;
r*2">0 by A8,XREAL_1:129;
then s3<s3+r/2 by XREAL_1:29;
then
A147: s3<G*(1,1)`2 by A134,XXREAL_0:2;
G*(i,1)`1+(G*(i+1,1)`1-G*(i,1)`1)/2 <G*(i,1)`1+(G*(i+1,1
)`1-G*(i,1)`1)/2 +(G*(i+1,1)`1-G*(i,1)`1)/2 by A139,XREAL_1:29,139;
then r3<G*(i+1,1)`1 by A135,A146,XXREAL_0:2;
then u0 in { |[r1,s1]| : G*(i,1)`1<r1 & r1<G*(i+1,1)`1 & s1 <
G*(1,1)`2} by A147,A141;
then u0 in Y by A130,GOBOARD6:24;
hence Y /\ G0 <> {}(TOP-REAL 2) by A9,A145,XBOOLE_0:def 4;
end;
case
A148: G*(i,1)`1 <r2 & r2<G*(i+1,1)`1;
set s3=s2-r/2,r3=r2;
reconsider q0=|[r3,s3]| as Point of TOP-REAL 2;
reconsider u0=q0 as Point of Euclid 2 by EUCLID:22;
r*2">0 by A8,XREAL_1:129;
then s3<s3+r/2 by XREAL_1:29;
then s3<G*(1,1)`2 by A134,XXREAL_0:2;
then u0 in { |[r1,s1]| : G*(i,1)`1<r1 & r1<G*(i+1,1)`1 & s1 <
G*(1,1)`2 } by A148;
then
A149: u0 in Y by A130,GOBOARD6:24;
reconsider v0=u0 as Element of REAL 2;
A150: q0`1=r3 & q0`2=s3 by EUCLID:52;
sqrt 2/2<1 by Lm1,SQUARE_1:21,XREAL_1:189;
then
A151: r*(sqrt 2/2)<r*1 by A8,XREAL_1:68;
A152: (r/2)^2 >=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 )<r by A151,A153,METRIC_1:def 1,XXREAL_0:2;
then dist(u,u0) < r by A154,A150,TOPREAL3:7;
then u0 in Ball(u,r) by METRIC_1:11;
hence Y /\ G0 <> {}(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<i+1 & i+1<=len G by A130,NAT_1:13;
then G*(i,1)`1<G*(i+1,1)`1 by A130,A158,GOBOARD5:3;
then
A159: sl>0 by XREAL_1:50;
then
A160: sm>0 by A8,XXREAL_0:21;
then r3<r3+sm/2 by XREAL_1:29,139;
then
A161: r3<G*(i+1,1)`1 by A133,XXREAL_0:2;
sqrt 2/2<1 by Lm1,SQUARE_1:21,XREAL_1:189;
then
A162: r*(sqrt 2/2)<r*1 by A8,XREAL_1:68;
sm/2<=r/2 by XREAL_1:72,XXREAL_0:17;
then (sm/2)^2<=(r/2)^2 by A160,SQUARE_1:15;
then
A163: (r/2)^2+(sm/2)^2<=(r/2)^2+(r/2)^2 by XREAL_1:7;
0<=(sm/2)^2 & 0<=(r/2)^2 by XREAL_1:63;
then
A164: sqrt((r/2)^2+(sm/2)^2)<=sqrt((r/2)^2+(r/2) ^2 ) by A163,
SQUARE_1:26;
p`1=r2 & p`2=s2 by A131,EUCLID:52;
then dist(u,u0) = (Pitag_dist 2).(v,v0) & sqrt ((p`1 - q0`1)
^2 + (p`2 - q0`2)^2)< r by A164,A157,A162,A156,METRIC_1:def 1,XXREAL_0:2;
then dist(u,u0) < r by TOPREAL3:7;
then
A165: u0 in Ball(u,r) by METRIC_1:11;
sm/2<=sl/2 by XREAL_1:72,XXREAL_0:17;
then
A166: G*(i+1,1)`1-sm/2>=G*(i+1,1)`1-sl/2 by XREAL_1:10;
r*2">0 by A8,XREAL_1:129;
then s3<s3+r/2 by XREAL_1:29;
then
A167: s3<G*(1,1)`2 by A134,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 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<r1 & r1<G*(i+1,1)`1 & s1 <
G*(1,1)`2 } by A167,A161;
then u0 in Y by A130,GOBOARD6:24;
hence Y /\ G0 <> {}(TOP-REAL 2) by A9,A165,XBOOLE_0:def 4;
end;
end;
hence Y /\ G0 <> {}(TOP-REAL 2);
end;
case
A168: 1<=i & i<len G & j=width G;
then p in { |[r2,s2]| : G*(i,1)`1 <=r2 & r2<=G*(i+1,1)`1 & s2>=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)<r*1 by A8,XREAL_1:68;
(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
A176: sqrt ((r/2)^2 + (r/2)^2) =r*((sqrt 2)/2) by A8,Lm1,SQUARE_1:22;
set rl=G*(i+1,1)`1 - G*(i,1)`1;
set rm=min(r,rl);
set s3=s2+r/2,r3=r2+rm/2;
reconsider q0=|[r3,s3]| as Point of TOP-REAL 2;
A177: 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;
A178: 1<=width G by Th34;
i<i+1 & i+1<=len G by A168,NAT_1:13;
then G*(i,1)`1<G*(i+1,1)`1 by A168,A178,GOBOARD5:3;
then
A179: rl>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)<r by A175,A176,METRIC_1:def 1,XXREAL_0:2;
then dist(u,u0) < r by A174,A177,TOPREAL3:7;
then
A183: u0 in Ball(u,r) by METRIC_1:11;
rm/2<=rl/2 by XREAL_1:72,XXREAL_0:17;
then
A184: G*(i,1)`1+rm/2<=G*(i,1)`1+rl/2 by XREAL_1:6;
r*2">0 by A8,XREAL_1:129;
then s2<s2+r/2 by XREAL_1:29;
then
A185: s3>G*(1,width G)`2 by A172,XXREAL_0:2;
G*(i,1)`1+(G*(i+1,1)`1-G*(i,1)`1)/2 <G*(i,1)`1+(G*(i+1,1
)`1-G*(i,1)`1)/2 +(G*(i+1,1)`1-G*(i,1)`1)/2 by A179,XREAL_1:29,139;
then r3<G*(i+1,1)`1 by A173,A184,XXREAL_0:2;
then u0 in { |[r1,s1]| : G*(i,1)`1<r1 & r1<G*(i+1,1)`1 & s1 >
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 <r2 & r2<G*(i+1,1)`1;
set s3=s2+r/2,r3=r2;
reconsider q0=|[r3,s3]| as Point of TOP-REAL 2;
reconsider u0=q0 as Point of Euclid 2 by EUCLID:22;
r*2">0 by A8,XREAL_1:129;
then s2<s3 by XREAL_1:29;
then s3>G*(1,width G)`2 by A172,XXREAL_0:2;
then u0 in { |[r1,s1]| : G*(i,1)`1<r1 & r1<G*(i+1,1)`1 & s1 >
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)<r*1 by A8,XREAL_1:68;
A190: (r/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)<r by A189,A191,METRIC_1:def 1,XXREAL_0:2;
then dist(u,u0) < r by A192,A188,TOPREAL3:7;
then u0 in Ball(u,r) by METRIC_1:11;
hence Y /\ G0 <> {}(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)<r*1 by A8,XREAL_1:68;
(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
A196: sqrt ((r/2)^2 + (r/2)^2) =r*((sqrt 2)/2) by A8,Lm1,SQUARE_1:22;
set rl=G*(i+1,1)`1 - G*(i,1)`1;
set rm=min(r,rl);
set s3=s2+r/2,r3=r2-rm/2;
reconsider q0=|[r3,s3]| as Point of TOP-REAL 2;
A197: 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;
A198: 1<=width G by Th34;
i<i+1 & i+1<=len G by A168,NAT_1:13;
then G*(i,1)`1<G*(i+1,1)`1 by A168,A198,GOBOARD5:3;
then
A199: rl>0 by XREAL_1:50;
then
A200: rm>0 by A8,XXREAL_0:21;
then r3<r3+rm/2 by XREAL_1:29,139;
then
A201: r3<G*(i+1,1)`1 by A171,XXREAL_0:2;
rm/2<=r/2 by XREAL_1:72,XXREAL_0:17;
then (rm/2)^2<=(r/2)^2 by A200,SQUARE_1:15;
then
A202: (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 A202,
SQUARE_1:26;
then dist(u,u0) = (Pitag_dist 2).(v,v0) & sqrt ((r2 - r3)^2 +
(s2 - s3)^2)<r by A195,A196,METRIC_1:def 1,XXREAL_0:2;
then dist(u,u0) < r by A194,A197,TOPREAL3:7;
then
A203: u0 in Ball(u,r) by METRIC_1:11;
rm/2<=rl/2 by XREAL_1:72,XXREAL_0:17;
then
A204: G*(i+1,1)`1-rm/2>=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<r1 & r1<G*(i+1,1)`1 & s1 >
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 & i<len G & 1<=j & j<width G;
then p in { |[r2,s2]| : G*(i,1)`1 <=r2 & r2<=G*(i+1,1)`1 & G*(1,j
)`2 <=s2 & s2<=G*(1,j+1)`2} by A3,Th32;
then consider r2,s2 such that
A207: p=|[r2,s2]| and
A208: G*(i,1)`1 <=r2 and
A209: r2<=G*(i+1,1)`1 and
A210: G*(1,j)`2 <=s2 and
A211: s2<=G*(1,j+1)`2;
now
per cases by A208,A209,A210,A211,XXREAL_0:1;
case
A212: r2=G*(i,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;
A213: 1<=width G by Th34;
i<i+1 & i+1<=len G by A206,NAT_1:13;
then G*(i,1)`1<G*(i+1,1)`1 by A206,A213,GOBOARD5:3;
then
A214: rl1>0 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 <G*(i,1)`1+(G*(i+1,1
)`1-G*(i,1)`1)/2 +(G*(i+1,1)`1-G*(i,1)`1)/2 by A214,XREAL_1:29,139;
then
A218: r3<G*(i+1,1)`1 by A212,A217,XXREAL_0:2;
rm/2<=rl/2 by XREAL_1:72,XXREAL_0:17;
then
A219: 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;
A220: 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;
A221: 1<=len G by Th34;
j<j+1 & j+1<=width G by A206,NAT_1:13;
then G*(1,j)`2<G*(1,j+1)`2 by A206,A221,GOBOARD5:4;
then
A222: rl>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)<r*1 by A8,XREAL_1:68;
(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
A228: sqrt ((r/2)^2 + (r/2)^2) =r*((sqrt 2)/2) by A8,Lm1,SQUARE_1:22;
A229: p`1=r2 & p`2=s2 by A207,EUCLID:52;
0<=(rm/2)^2 & 0<=(rm1/2)^2 by XREAL_1:63;
then sqrt((rm1/2)^2+(rm/2)^2)<=sqrt((r/2)^2+(r/ 2)^2 ) by A226,
SQUARE_1:26;
then dist(u,u0) = (Pitag_dist 2).(v,v0) & sqrt ((r2 - r3)^2 +
(s2 - s3)^2)<r by A227,A228,METRIC_1:def 1,XXREAL_0:2;
then dist(u,u0) < r by A229,A220,TOPREAL3:7;
then
A230: u0 in Ball(u,r) by METRIC_1:11;
G*(1,j)`2+(G*(1,j+1)`2-G*(1,j)`2)/2 <G*(1,j)`2+(G*(1,j+1
)`2-G*(1,j)`2)/2 +(G*(1,j+1)`2-G*(1,j)`2)/2 by A222,XREAL_1:29,139;
then s3<G*(1,j+1)`2 by A212,A219,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 A224,A216,A218;
then u0 in Y by A206,GOBOARD6:26;
hence Y /\ G0 <> {}(TOP-REAL 2) by A9,A230,XBOOLE_0:def 4;
end;
case
A231: r2=G*(i,1)`1 & G*(1,j)`2 <s2 & s2<G*(1,j+1)`2;
set s3=s2;
set rl1=G*(i+1,1)`1 - G*(i,1)`1;
set rm1=min(r,rl1);
set r3=r2+rm1/2;
reconsider q0=|[r3,s3]| as Point of TOP-REAL 2;
reconsider u0=q0 as Point of Euclid 2 by EUCLID:22;
A232: 1<=width G by Th34;
i<i+1 & i+1<=len G by A206,NAT_1:13;
then G*(i,1)`1<G*(i+1,1)`1 by A206,A232,GOBOARD5:3;
then
A233: rl1>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 <G*(i,1)`1+(G*(i+1,1
)`1-G*(i,1)`1)/2 +(G*(i+1,1)`1-G*(i,1)`1)/2 by A233,XREAL_1:29,139;
then r3<G*(i+1,1)`1 by A231,A236,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 A231,A235;
then
A237: u0 in Y by A206,GOBOARD6:26;
sqrt 2/2<1 by Lm1,SQUARE_1:21,XREAL_1:189;
then
A238: r*(sqrt 2/2)<r*1 by A8,XREAL_1:68;
reconsider v0=u0 as Element of REAL 2;
A239: 0<=(rm1/2)^2 by XREAL_1:63;
rm1/2<=r/2 by XREAL_1:72,XXREAL_0:17;
then (rm1/2)^2+0^2<=(r/2)^2+0^2 by A234,SQUARE_1:15;
then
A240: sqrt((rm1/2)^2+0^2)<=sqrt((r/2)^2+0^2) by A239,SQUARE_1:26;
A241: q0`1=r3 & q0`2=s3 by EUCLID:52;
A242: (r/2)^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)<r by A238,A243,XXREAL_0:2;
then
A244: dist(u,u0) = (Pitag_dist 2).(v,v0) & sqrt((r2 - r3)^2 +
(s2 - s3)^2)<r by A240,METRIC_1:def 1,XXREAL_0:2;
p`1=r2 & p`2=s2 by A207,EUCLID:52;
then dist(u,u0) < r by A241,A244,TOPREAL3:7;
then u0 in Ball(u,r) by METRIC_1:11;
hence Y /\ G0 <> {}(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<i+1 & i+1<=len G by A206,NAT_1:13;
then G*(i,1)`1<G*(i+1,1)`1 by A206,A246,GOBOARD5:3;
then
A247: rl1>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*(i,1)`1+(G*(i+1,1
)`1-G*(i,1)`1)/2 +(G*(i+1,1)`1-G*(i,1)`1)/2 by A247,XREAL_1:29,139;
then
A251: r3<G*(i+1,1)`1 by A245,A250,XXREAL_0:2;
rm/2<=rl/2 by XREAL_1:72,XXREAL_0:17;
then
A252: G*(1,j+1)`2-rm/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;
j<j+1 & j+1<=width G by A206,NAT_1:13;
then G*(1,j)`2<G*(1,j+1)`2 by A206,A254,GOBOARD5:4;
then
A255: rl>0 by XREAL_1:50;
then
A256: rm>0 by A8,XXREAL_0:21;
then s3<s2 by XREAL_1:44,139;
then
A257: s3<G*(1,j+1)`2 by A211,XXREAL_0:2;
rm1/2<=r/2 by XREAL_1:72,XXREAL_0:17;
then
A258: (rm1/2)^2<=(r/2)^2 by A248,SQUARE_1:15;
rm/2<=r/2 by XREAL_1:72,XXREAL_0:17;
then (rm/2)^2<=(r/2)^2 by A256,SQUARE_1:15;
then
A259: (rm1/2)^2+(rm/2)^2<=(r/2)^2+(r/2)^2 by A258,XREAL_1:7;
sqrt 2/2<1 by Lm1,SQUARE_1:21,XREAL_1:189;
then
A260: r*(sqrt 2/2)<r*1 by A8,XREAL_1:68;
(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
A261: sqrt ((r/2)^2 + (r/2)^2) =r*((sqrt 2)/2) by A8,Lm1,SQUARE_1:22;
A262: p`1=r2 & p`2=s2 by A207,EUCLID:52;
0<=(rm/2)^2 & 0<=(rm1/2)^2 by XREAL_1:63;
then sqrt((rm1/2)^2+(rm/2)^2)<=sqrt((r/2)^2+(r/ 2)^2 ) by A259,
SQUARE_1:26;
then dist(u,u0) = (Pitag_dist 2).(v,v0) & sqrt ((r2 - r3)^2 +
(s2 - s3)^2)<r by A260,A261,METRIC_1:def 1,XXREAL_0:2;
then dist(u,u0) < r by A262,A253,TOPREAL3:7;
then
A263: u0 in Ball(u,r) by METRIC_1:11;
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 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 <r2 & r2<G*(i+1,1)`1 & s2=G*(1,j)`2;
set r3=r2;
set rl=G*(1,j+1)`2 - G*(1,j)`2;
set rm=min(r,rl);
set s3=s2+rm/2;
reconsider q0=|[r3,s3]| as Point of TOP-REAL 2;
reconsider u0=q0 as Point of Euclid 2 by EUCLID:22;
A265: 1<=len G by Th34;
j<j+1 & j+1<=width G by A206,NAT_1:13;
then G*(1,j)`2<G*(1,j+1)`2 by A206,A265,GOBOARD5:4;
then
A266: rl>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 <G*(1,j)`2+(G*(1,j+1
)`2-G*(1,j)`2)/2 +(G*(1,j+1)`2-G*(1,j)`2)/2 by A266,XREAL_1:29,139;
then s3<G*(1,j+1)`2 by A264,A269,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 A264,A268;
then
A270: u0 in Y by A206,GOBOARD6:26;
sqrt 2/2<1 by Lm1,SQUARE_1:21,XREAL_1:189;
then
A271: r*(sqrt 2/2)<r*1 by A8,XREAL_1:68;
reconsider v0=u0 as Element of REAL 2;
A272: 0<=(rm/2)^2 by XREAL_1:63;
rm/2<=r/2 by XREAL_1:72,XXREAL_0:17;
then (rm/2)^2+0^2<=(r/2)^2+0^2 by A267,SQUARE_1:15;
then
A273: sqrt(0^2+(rm/2)^2)<=sqrt(0^2+(r/2)^2) by A272,SQUARE_1:26;
A274: q0`1=r3 & q0`2=s3 by EUCLID:52;
A275: (r/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)<r by A271,A276,XXREAL_0:2;
then
A277: dist(u,u0) = (Pitag_dist 2).(v,v0) & sqrt((r2 - r3)^2 +
(s2 - s3)^2)<r by A273,METRIC_1:def 1,XXREAL_0:2;
p`1=r2 & p`2=s2 by A207,EUCLID:52;
then dist(u,u0) < r by A274,A277,TOPREAL3:7;
then u0 in Ball(u,r) by METRIC_1:11;
hence Y /\ G0 <> {}(TOP-REAL 2) by A9,A270,XBOOLE_0:def 4;
end;
case
A278: G*(i,1)`1 <r2 & r2<G*(i+1,1)`1 & G*(1,j)`2 <s2 & s2<
G*(1,j+1)`2;
set s3=s2,r3=r2;
reconsider q0=|[r3,s3]| as Point of TOP-REAL 2;
A279: 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;
dist(u,u0) = (Pitag_dist 2).(v,v0) & sqrt((r2 - r3)^2 +
(s2 - s3)^2 )<r by A8,METRIC_1:def 1;
then dist(u,u0) < r by A207,A279,TOPREAL3:7;
then
A280: u0 in Ball(u,r) by METRIC_1:11;
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 A278;
then u0 in Y by A206,GOBOARD6:26;
hence Y /\ G0 <> {}(TOP-REAL 2) by A9,A280,XBOOLE_0:def 4;
end;
case
A281: G*(i,1)`1 <r2 & r2<G*(i+1,1)`1 & s2=G*(1,j+1)`2;
set r3=r2;
set rl=G*(1,j+1)`2 - G*(1,j)`2;
set rm=min(r,rl);
set s3=s2-rm/2;
reconsider q0=|[r3,s3]| as Point of TOP-REAL 2;
reconsider u0=q0 as Point of Euclid 2 by EUCLID:22;
A282: 1<=len G by Th34;
j<j+1 & j+1<=width G by A206,NAT_1:13;
then G*(1,j)`2<G*(1,j+1)`2 by A206,A282,GOBOARD5:4;
then
A283: rl>0 by XREAL_1:50;
then
A284: rm>0 by A8,XXREAL_0:21;
then
A285: s3<s2 by XREAL_1:44,139;
rm/2<=rl/2 by XREAL_1:72,XXREAL_0:17;
then
A286: G*(1,j+1)`2-rm/2>=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)<r*1 by A8,XREAL_1:68;
reconsider v0=u0 as Element of REAL 2;
A289: 0<=(rm/2)^2 by XREAL_1:63;
rm/2<=r/2 by XREAL_1:72,XXREAL_0:17;
then (rm/2)^2+0^2<=(r/2)^2+0^2 by A284,SQUARE_1:15;
then
A290: sqrt(0^2+(rm/2)^2)<=sqrt(0^2+(r/2)^2) by A289,SQUARE_1:26;
A291: q0`1=r3 & q0`2=s3 by EUCLID:52;
A292: (r/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)<r by A288,A293,XXREAL_0:2;
then
A294: dist(u,u0) = (Pitag_dist 2).(v,v0) & sqrt((r2 - r3)^2 +
(s2 - s3)^2 )<r by A290,METRIC_1:def 1,XXREAL_0:2;
p`1=r2 & p`2=s2 by A207,EUCLID:52;
then dist(u,u0) < r by A291,A294,TOPREAL3:7;
then u0 in Ball(u,r) by METRIC_1:11;
hence Y /\ G0 <> {}(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<i+1 & i+1<=len G by A206,NAT_1:13;
then G*(i,1)`1<G*(i+1,1)`1 by A206,A296,GOBOARD5:3;
then
A297: rl1>0 by XREAL_1:50;
then
A298: rm1>0 by A8,XXREAL_0:21;
then r3<r2 by XREAL_1:44,139;
then
A299: r3<G*(i+1,1)`1 by A209,XXREAL_0:2;
rm1/2<=rl1/2 by XREAL_1:72,XXREAL_0:17;
then
A300: G*(i+1,1)`1-rm1/2>=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;
j<j+1 & j+1<=width G by A206,NAT_1:13;
then G*(1,j)`2<G*(1,j+1)`2 by A206,A304,GOBOARD5:4;
then
A305: rl>0 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)<r*1 by A8,XREAL_1:68;
(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
A311: sqrt ((r/2)^2 + (r/2)^2) =r*((sqrt 2)/2) by A8,Lm1,SQUARE_1:22;
A312: p`1=r2 & p`2=s2 by A207,EUCLID:52;
0<=(rm/2)^2 & 0<=(rm1/2)^2 by XREAL_1:63;
then sqrt((rm1/2)^2+(rm/2)^2)<=sqrt((r/2)^2+(r/ 2)^2 ) by A309,
SQUARE_1:26;
then dist(u,u0) = (Pitag_dist 2).(v,v0) & sqrt ((r2 - r3)^2 +
(s2 - s3)^2)<r by A310,A311,METRIC_1:def 1,XXREAL_0:2;
then dist(u,u0) < r by A312,A303,TOPREAL3:7;
then
A313: u0 in Ball(u,r) by METRIC_1:11;
G*(1,j)`2+(G*(1,j+1)`2-G*(1,j)`2)/2 <G*(1,j)`2+(G*(1,j+1
)`2-G*(1,j)`2)/2 +(G*(1,j+1)`2-G*(1,j)`2)/2 by A305,XREAL_1:29,139;
then s3<G*(1,j+1)`2 by A295,A302,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 A307,A299,A301;
then u0 in Y by A206,GOBOARD6:26;
hence Y /\ G0 <> {}(TOP-REAL 2) by A9,A313,XBOOLE_0:def 4;
end;
case
A314: r2=G*(i+1,1)`1 & G*(1,j)`2 <s2 & s2<G*(1,j+1)`2;
set s3=s2;
set rl1=G*(i+1,1)`1 - G*(i,1)`1;
set rm1=min(r,rl1);
set r3=r2-rm1/2;
reconsider q0=|[r3,s3]| as Point of TOP-REAL 2;
reconsider u0=q0 as Point of Euclid 2 by EUCLID:22;
A315: 1<=width G by Th34;
i<i+1 & i+1<=len G by A206,NAT_1:13;
then G*(i,1)`1<G*(i+1,1)`1 by A206,A315,GOBOARD5:3;
then
A316: rl1>0 by XREAL_1:50;
then
A317: rm1>0 by A8,XXREAL_0:21;
then
A318: r3<r2 by XREAL_1:44,139;
rm1/2<=rl1/2 by XREAL_1:72,XXREAL_0:17;
then
A319: G*(i+1,1)`1-rm1/2>=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)<r*1 by A8,XREAL_1:68;
reconsider v0=u0 as Element of REAL 2;
A322: 0<=(rm1/2)^2 by XREAL_1:63;
rm1/2<=r/2 by XREAL_1:72,XXREAL_0:17;
then 0^2+(rm1/2)^2<=0^2+(r/2)^2 by A317,SQUARE_1:15;
then
A323: sqrt((rm1/2)^2+0^2)<=sqrt((r/2)^2+0^2) by A322,SQUARE_1:26;
A324: q0`1=r3 & q0`2=s3 by EUCLID:52;
A325: (r/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)<r by A321,A326,XXREAL_0:2;
then
A327: dist(u,u0) = (Pitag_dist 2).(v,v0) & sqrt((r2 - r3)^2 +
(s2 - s3)^2 )<r by A323,METRIC_1:def 1,XXREAL_0:2;
p`1=r2 & p`2=s2 by A207,EUCLID:52;
then dist(u,u0) < r by A324,A327,TOPREAL3:7;
then u0 in Ball(u,r) by METRIC_1:11;
hence Y /\ G0 <> {}(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<i+1 & i+1<=len G by A206,NAT_1:13;
then G*(i,1)`1<G*(i+1,1)`1 by A206,A329,GOBOARD5:3;
then
A330: rl1>0 by XREAL_1:50;
then
A331: rm1>0 by A8,XXREAL_0:21;
then r3<r2 by XREAL_1:44,139;
then
A332: r3<G*(i+1,1)`1 by A209,XXREAL_0:2;
rm1/2<=rl1/2 by XREAL_1:72,XXREAL_0:17;
then
A333: G*(i+1,1)`1-rm1/2>=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)<r*1 by A8,XREAL_1:68;
A337: p`1=r2 & p`2=s2 by A207,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
A338: sqrt ((r/2)^2 + (r/2)^2) =r*((sqrt 2)/2) by A8,Lm1,SQUARE_1:22;
A339: 1<=len G by Th34;
rm1/2<=r/2 by XREAL_1:72,XXREAL_0:17;
then
A340: (rm1/2)^2<=(r/2)^2 by A331,SQUARE_1:15;
reconsider q0=|[r3,s3]| as Point of TOP-REAL 2;
A341: 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;
A342: r2-r3=rm1/2 & s2-s3=rm/2;
j<j+1 & j+1<=width G by A206,NAT_1:13;
then G*(1,j)`2<G*(1,j+1)`2 by A206,A339,GOBOARD5:4;
then
A343: rl>0 by XREAL_1:50;
then
A344: rm>0 by A8,XXREAL_0:21;
then s3<s2 by XREAL_1:44,139;
then
A345: s3<G*(1,j+1)`2 by A211,XXREAL_0:2;
rm/2<=r/2 by XREAL_1:72,XXREAL_0:17;
then (rm/2)^2<=(r/2)^2 by A344,SQUARE_1:15;
then
A346: (rm1/2)^2+(rm/2)^2<=(r/2)^2+(r/2)^2 by A340,XREAL_1:7;
0<=(rm/2)^2 & 0<=(rm1/2)^2 by XREAL_1:63;
then sqrt((rm1/2)^2+(rm/2)^2)<=sqrt((r/2)^2+(r/ 2)^2 ) by A346,
SQUARE_1:26;
then dist(u,u0) = (Pitag_dist 2).(v,v0) & sqrt ((rm1/2)^2 + (
rm/2)^2)<r by A336,A338,METRIC_1:def 1,XXREAL_0:2;
then dist(u,u0) < r by A337,A341,A342,TOPREAL3:7;
then
A347: u0 in Ball(u,r) by METRIC_1:11;
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 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;