let i be Nat; for G being Go-board st i <= len G holds
not cell (G,i,0) is bounded
let G be Go-board; ( i <= len G implies not cell (G,i,0) is bounded )
assume A1:
i <= len G
; not cell (G,i,0) is bounded
per cases
( i = 0 or ( i >= 1 & i < len G ) or i = len G )
by A1, NAT_1:14, XXREAL_0:1;
suppose
i = 0
;
not cell (G,i,0) is bounded then A2:
cell (
G,
i,
0)
= { |[r,s]| where r, s is Real : ( r <= (G * (1,1)) `1 & s <= (G * (1,1)) `2 ) }
by GOBRD11:24;
for
r being
Real ex
q being
Point of
(TOP-REAL 2) st
(
q in cell (
G,
i,
0) & not
|.q.| < r )
proof
let r be
Real;
ex q being Point of (TOP-REAL 2) st
( q in cell (G,i,0) & not |.q.| < r )
take q =
|[(min ((- r),((G * (1,1)) `1))),(min ((- r),((G * (1,1)) `2)))]|;
( q in cell (G,i,0) & not |.q.| < r )
A3:
|.(q `1).| <= |.q.|
by JGRAPH_1:33;
(
min (
(- r),
((G * (1,1)) `1))
<= (G * (1,1)) `1 &
min (
(- r),
((G * (1,1)) `2))
<= (G * (1,1)) `2 )
by XXREAL_0:17;
hence
q in cell (
G,
i,
0)
by A2;
not |.q.| < r
end; hence
not
cell (
G,
i,
0) is
bounded
by JORDAN2C:34;
verum end; suppose A6:
(
i >= 1 &
i < len G )
;
not cell (G,i,0) is bounded then A7:
cell (
G,
i,
0)
= { |[r,s]| where r, s is Real : ( (G * (i,1)) `1 <= r & r <= (G * ((i + 1),1)) `1 & s <= (G * (1,1)) `2 ) }
by GOBRD11:30;
for
r being
Real ex
q being
Point of
(TOP-REAL 2) st
(
q in cell (
G,
i,
0) & not
|.q.| < r )
proof
let r be
Real;
ex q being Point of (TOP-REAL 2) st
( q in cell (G,i,0) & not |.q.| < r )
take q =
|[((G * (i,1)) `1),(min ((- r),((G * (1,1)) `2)))]|;
( q in cell (G,i,0) & not |.q.| < r )
A8:
min (
(- r),
((G * (1,1)) `2))
<= (G * (1,1)) `2
by XXREAL_0:17;
width G <> 0
by MATRIX_0:def 10;
then A9:
1
<= width G
by NAT_1:14;
(
i < i + 1 &
i + 1
<= len G )
by A6, NAT_1:13;
then
(G * (i,1)) `1 <= (G * ((i + 1),1)) `1
by A6, A9, GOBOARD5:3;
hence
q in cell (
G,
i,
0)
by A7, A8;
not |.q.| < r
A10:
|.(q `2).| <= |.q.|
by JGRAPH_1:33;
end; hence
not
cell (
G,
i,
0) is
bounded
by JORDAN2C:34;
verum end; suppose
i = len G
;
not cell (G,i,0) is bounded then A13:
cell (
G,
i,
0)
= { |[r,s]| where r, s is Real : ( (G * ((len G),1)) `1 <= r & s <= (G * (1,1)) `2 ) }
by GOBRD11:27;
for
r being
Real ex
q being
Point of
(TOP-REAL 2) st
(
q in cell (
G,
i,
0) & not
|.q.| < r )
proof
let r be
Real;
ex q being Point of (TOP-REAL 2) st
( q in cell (G,i,0) & not |.q.| < r )
take q =
|[(max (r,((G * ((len G),1)) `1))),((G * (1,1)) `2)]|;
( q in cell (G,i,0) & not |.q.| < r )
A14:
|.(q `1).| <= |.q.|
by JGRAPH_1:33;
(G * ((len G),1)) `1 <= max (
r,
((G * ((len G),1)) `1))
by XXREAL_0:25;
hence
q in cell (
G,
i,
0)
by A13;
not |.q.| < r
end; hence
not
cell (
G,
i,
0) is
bounded
by JORDAN2C:34;
verum end; end;