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