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