:: On the Geometry of a Go-board :: by Andrzej Trybulec :: :: Received July 9, 1995 :: Copyright (c) 1995-2018 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, PRE_TOPC, EUCLID, GOBOARD1, ARYTM_3, MCART_1, ARYTM_1, RELAT_1, XBOOLE_0, METRIC_1, XXREAL_0, CARD_1, PCOMPS_1, RCOMP_1, STRUCT_0, CONNSP_2, TOPS_1, TARSKI, SQUARE_1, FUNCT_1, FINSEQ_1, TREES_1, GOBOARD5, COMPLEX1, RLTOPSP1, SUPINF_2, NAT_1; notations TARSKI, XBOOLE_0, ORDINAL1, SUBSET_1, NUMBERS, XXREAL_0, XREAL_0, XCMPLX_0, COMPLEX1, REAL_1, NAT_1, SQUARE_1, NAT_D, BINOP_1, FINSEQ_1, MATRIX_0, STRUCT_0, METRIC_1, PRE_TOPC, TOPS_1, CONNSP_2, PCOMPS_1, RLVECT_1, RLTOPSP1, EUCLID, GOBOARD1, GOBOARD5; constructors REAL_1, SQUARE_1, NAT_1, COMPLEX1, NAT_D, TOPS_1, CONNSP_2, PCOMPS_1, GOBOARD1, GOBOARD5, FUNCSDOM, BINOP_2; registrations RELSET_1, XXREAL_0, XREAL_0, STRUCT_0, METRIC_1, PCOMPS_1, EUCLID, TOPS_1, PRE_TOPC, SQUARE_1, ORDINAL1, NAT_1; requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM; begin reserve n for Nat, i,j for Nat, r,s,r1,s1,r2,s2,r9,s9 for Real, p,q for Point of TOP-REAL 2, G for Go-board, x,y for set, v for Point of Euclid 2; theorem :: GOBOARD6:1 for M being non empty Reflexive MetrStruct, u being Point of M, r being Real holds r > 0 implies u in Ball(u,r); theorem :: GOBOARD6:2 for p being Point of Euclid n, q being Point of TOP-REAL n, r being Real st p = q & r > 0 holds Ball (p, r) is a_neighborhood of q; theorem :: GOBOARD6:3 for B being Subset of TOP-REAL n, u being Point of Euclid n st B = Ball(u,r) holds B is open; theorem :: GOBOARD6:4 for M being non empty MetrSpace, u being Point of M, P being Subset of TopSpaceMetr(M) holds u in Int P iff ex r being Real st r > 0 & Ball(u,r) c= P; theorem :: GOBOARD6:5 for u being Point of Euclid n, P being Subset of TOP-REAL n holds u in Int P iff ex r being Real st r > 0 & Ball(u,r) c= P; theorem :: GOBOARD6:6 :: TOPREAL3:12 for u,v being Point of Euclid 2 st u = |[r1,s1]| & v = |[r2,s2]| holds dist(u,v) =sqrt ((r1 - r2)^2 + (s1 - s2)^2); theorem :: GOBOARD6:7 for u being Point of Euclid 2 st u = |[r,s]| holds 0 <= r2 & r2 < r1 implies |[r+r2,s]| in Ball(u,r1); theorem :: GOBOARD6:8 for u being Point of Euclid 2 st u = |[r,s]| holds 0 <= s2 & s2 < s1 implies |[r,s+s2]| in Ball(u,s1); theorem :: GOBOARD6:9 for u being Point of Euclid 2 st u = |[r,s]| holds 0 <= r2 & r2 < r1 implies |[r-r2,s]| in Ball(u,r1); theorem :: GOBOARD6:10 for u being Point of Euclid 2 st u = |[r,s]| holds 0 <= s2 & s2 < s1 implies |[r,s-s2]| in Ball(u,s1); theorem :: GOBOARD6:11 1 <= i & i < len G & 1 <= j & j < width G implies G*(i,j)+G*(i+1 ,j+1) = G*(i,j+1)+G*(i+1,j); theorem :: GOBOARD6:12 Int v_strip(G,0) = { |[r,s]| : r < G*(1,1)`1 }; theorem :: GOBOARD6:13 Int v_strip(G,len G) = { |[r,s]| : G*(len G,1)`1 < r }; theorem :: GOBOARD6:14 1 <= i & i < len G implies Int v_strip(G,i) = { |[r,s]| : G*(i,1 )`1 < r & r < G*(i+1,1)`1 }; theorem :: GOBOARD6:15 Int h_strip(G,0) = { |[r,s]| : s < G*(1,1)`2 }; theorem :: GOBOARD6:16 Int h_strip(G,width G) = { |[r,s]| : G*(1,width G)`2 < s }; theorem :: GOBOARD6:17 1 <= j & j < width G implies Int h_strip(G,j) = { |[r,s]| : G*(1 ,j)`2 < s & s < G*(1,j+1)`2 }; theorem :: GOBOARD6:18 Int cell(G,0,0) = { |[r,s]| : r < G*(1,1)`1 & s < G*(1,1)`2 }; theorem :: GOBOARD6:19 Int cell(G,0,width G) = { |[r,s]| : r < G*(1,1)`1 & G*(1,width G )`2 < s }; theorem :: GOBOARD6:20 1 <= j & j < width G implies Int cell(G,0,j) = { |[r,s]| : r < G *(1,1)`1 & G*(1,j)`2 < s & s < G*(1,j+1)`2 }; theorem :: GOBOARD6:21 Int cell(G,len G,0) = { |[r,s]| : G*(len G,1)`1 < r & s < G*(1,1 )`2 }; theorem :: GOBOARD6:22 Int cell(G,len G,width G) = { |[r,s]| : G*(len G,1)`1 < r & G*(1 ,width G)`2 < s }; theorem :: GOBOARD6:23 1 <= j & j < width G implies Int cell(G,len G,j) = { |[r,s]| : G *(len G,1)`1 < r & G*(1,j)`2 < s & s < G*(1,j+1)`2 }; theorem :: GOBOARD6:24 1 <= i & i < len G implies Int cell(G,i,0) = { |[r,s]| : G*(i,1) `1 < r & r < G*(i+1,1)`1 & s < G*(1,1)`2 }; theorem :: GOBOARD6:25 1 <= i & i < len G implies Int cell(G,i,width G) = { |[r,s]| : G *(i,1)`1 < r & r < G*(i+1,1)`1 & G*(1,width G)`2 < s }; theorem :: GOBOARD6:26 1 <= i & i < len G & 1 <= j & j < width G implies Int 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 }; theorem :: GOBOARD6:27 1 <= j & j <= width G & p in Int h_strip(G,j) implies p`2 > G*(1,j)`2; theorem :: GOBOARD6:28 j < width G & p in Int h_strip(G,j) implies p`2 < G*(1,j+1)`2; theorem :: GOBOARD6:29 1 <= i & i <= len G & p in Int v_strip(G,i) implies p`1 > G*(i,1)`1; theorem :: GOBOARD6:30 i < len G & p in Int v_strip(G,i) implies p`1 < G*(i+1,1)`1; theorem :: GOBOARD6:31 1 <= i & i+1 <= len G & 1 <= j & j+1 <= width G implies 1/2*(G*( i,j)+G*(i+1,j+1)) in Int cell(G,i,j); theorem :: GOBOARD6:32 1 <= i & i+1 <= len G implies 1/2*(G*(i,width G)+G*(i+1,width G) )+|[0,1]| in Int cell(G,i,width G); theorem :: GOBOARD6:33 1 <= i & i+1 <= len G implies 1/2*(G*(i,1)+G*(i+1,1))-|[0,1]| in Int cell(G,i,0); theorem :: GOBOARD6:34 1 <= j & j+1 <= width G implies 1/2*(G*(len G,j)+G*(len G,j+1))+ |[1,0]| in Int cell(G,len G,j); theorem :: GOBOARD6:35 1 <= j & j+1 <= width G implies 1/2*(G*(1,j)+G*(1,j+1))-|[1,0]| in Int cell(G,0,j); theorem :: GOBOARD6:36 G*(1,1)-|[1,1]| in Int cell(G,0,0); theorem :: GOBOARD6:37 G*(len G,width G)+|[1,1]| in Int cell(G,len G,width G); theorem :: GOBOARD6:38 G*(1,width G)+|[-1,1]| in Int cell(G,0,width G); theorem :: GOBOARD6:39 G*(len G,1)+|[1,-1]| in Int cell(G,len G,0); theorem :: GOBOARD6:40 1 <= i & i < len G & 1 <= j & j < width G implies LSeg(1/2*(G*(i ,j)+G*(i+1,j+1)),1/2*(G*(i,j)+G*(i,j+1))) c= Int cell(G,i,j) \/ { 1/2*(G*(i,j)+ G*(i,j+1)) }; theorem :: GOBOARD6:41 1 <= i & i < len G & 1 <= j & j < width G implies LSeg(1/2*(G*(i ,j)+G*(i+1,j+1)),1/2*(G*(i,j+1)+G*(i+1,j+1))) c= Int cell(G,i,j) \/ { 1/2*(G*(i ,j+1)+G*(i+1,j+1)) }; theorem :: GOBOARD6:42 1 <= i & i < len G & 1 <= j & j < width G implies LSeg(1/2*(G*(i ,j)+G*(i+1,j+1)),1/2*(G*(i+1,j)+G*(i+1,j+1))) c= Int cell(G,i,j) \/ { 1/2*(G*(i +1,j)+G*(i+1,j+1)) }; theorem :: GOBOARD6:43 1 <= i & i < len G & 1 <= j & j < width G implies LSeg(1/2*(G*(i ,j)+G*(i+1,j+1)),1/2*(G*(i,j)+G*(i+1,j))) c= Int cell(G,i,j) \/ { 1/2*(G*(i,j)+ G*(i+1,j)) }; theorem :: GOBOARD6:44 1 <= j & j < width G implies LSeg(1/2*(G*(1,j)+G*(1,j+1)) - |[1, 0]|,1/2*(G*(1,j)+G*(1,j+1))) c= Int cell(G,0,j) \/ { 1/2*(G*(1,j)+G*(1,j+1)) }; theorem :: GOBOARD6:45 1 <= j & j < width G implies LSeg(1/2*(G*(len G,j)+G*(len G,j+1) ) + |[1,0]|,1/2*(G*(len G,j)+G*(len G,j+1))) c= Int cell(G,len G,j) \/ { 1/2*(G *(len G,j)+G*(len G,j+1)) }; theorem :: GOBOARD6:46 1 <= i & i < len G implies LSeg(1/2*(G*(i,1)+G*(i+1,1)) - |[0,1 ]|,1/2*(G*(i,1)+G*(i+1,1))) c= Int cell(G,i,0) \/ { 1/2*(G*(i,1)+G*(i+1,1)) } ; theorem :: GOBOARD6:47 1 <= i & i < len G implies LSeg(1/2*(G*(i,width G)+G*(i+1,width G))+ |[0,1]|, 1/2*(G*(i,width G)+G*(i+1,width G))) c= Int cell(G,i,width G) \/ { 1/2*(G*(i,width G)+G*(i+1,width G)) }; theorem :: GOBOARD6:48 1 <= j & j < width G implies LSeg(1/2*(G*(1,j)+G*(1,j+1)) - |[1, 0]|,G*(1,j) - |[1,0]|) c= Int cell(G,0,j) \/ { G*(1,j) - |[1,0]| }; theorem :: GOBOARD6:49 1 <= j & j < width G implies LSeg(1/2*(G*(1,j)+G*(1,j+1)) - |[1, 0]|,G*(1,j+1) - |[1,0]|) c= Int cell(G,0,j) \/ { G*(1,j+1) - |[1,0]| }; theorem :: GOBOARD6:50 1 <= j & j < width G implies LSeg(1/2*(G*(len G,j)+G*(len G,j+1) ) + |[1,0]|,G*(len G,j) + |[1,0]|) c= Int cell(G,len G,j) \/ { G*(len G,j) + |[ 1,0]| }; theorem :: GOBOARD6:51 1 <= j & j < width G implies LSeg(1/2*(G*(len G,j)+G*(len G,j+1) ) + |[1,0]|,G*(len G,j+1) + |[1,0]|) c= Int cell(G,len G,j) \/ { G*(len G,j+1) + |[1,0]| }; theorem :: GOBOARD6:52 1 <= i & i < len G implies LSeg(1/2*(G*(i,1)+G*(i+1,1)) - |[0,1 ]|,G*(i,1) - |[0,1]|) c= Int cell(G,i,0) \/ { G*(i,1) - |[0,1]| }; theorem :: GOBOARD6:53 1 <= i & i < len G implies LSeg(1/2*(G*(i,1)+G*(i+1,1)) - |[0,1 ]|,G*(i+1,1) - |[0,1]|) c= Int cell(G,i,0) \/ { G*(i+1,1) - |[0,1]| }; theorem :: GOBOARD6:54 1 <= i & i < len G implies LSeg(1/2*(G*(i,width G)+G*(i+1,width G)) + |[0,1]|,G* (i,width G) + |[0,1]|) c= Int cell(G,i,width G) \/ { G*(i, width G) + |[0,1]| }; theorem :: GOBOARD6:55 1 <= i & i < len G implies LSeg(1/2*(G*(i,width G)+G*(i+1,width G)) + |[0,1]|,G* (i+1,width G) + |[0,1]|) c= Int cell(G,i,width G) \/ { G*(i+1, width G) + |[0,1]| }; theorem :: GOBOARD6:56 LSeg(G*(1,1) - |[1,1]|,G*(1,1) - |[1,0]|) c= Int cell(G,0,0) \/ { G*(1,1) - |[1,0]| }; theorem :: GOBOARD6:57 LSeg(G*(len G,1) + |[1,-1]|,G*(len G,1) + |[1,0]|) c= Int cell(G ,len G,0) \/ { G*(len G,1) + |[1,0]| }; theorem :: GOBOARD6:58 LSeg(G*(1,width G) + |[-1,1]|,G*(1,width G) - |[1,0]|) c= Int cell(G,0,width G) \/ { G*(1,width G) - |[1,0]| }; theorem :: GOBOARD6:59 LSeg(G*(len G,width G) + |[1,1]|,G*(len G,width G) + |[1,0]|) c= Int cell(G,len G,width G) \/ { G*(len G,width G) + |[1,0]| }; theorem :: GOBOARD6:60 LSeg(G*(1,1) - |[1,1]|,G*(1,1) - |[0,1]|) c= Int cell(G,0,0) \/ { G*(1,1) - |[0,1]| }; theorem :: GOBOARD6:61 LSeg(G*(len G,1) + |[1,-1]|,G*(len G,1) - |[0,1]|) c= Int cell(G ,len G,0) \/ { G*(len G,1) - |[0,1]| }; theorem :: GOBOARD6:62 LSeg(G*(1,width G) + |[-1,1]|,G*(1,width G) + |[0,1]|) c= Int cell(G,0,width G) \/ { G*(1,width G) + |[0,1]| }; theorem :: GOBOARD6:63 LSeg(G*(len G,width G) + |[1,1]|,G*(len G,width G) + |[0,1]|) c= Int cell(G,len G,width G) \/ { G*(len G,width G) + |[0,1]| }; theorem :: GOBOARD6:64 1 <= i & i < len G & 1 <= j & j+1 < width G implies LSeg(1/2*(G*(i,j)+ G*(i+1,j+1)),1/2*(G*(i,j+1)+G*(i+1,j+2))) c= Int cell(G,i,j) \/ Int cell(G,i,j+ 1) \/ { 1/2*(G*(i,j+1)+G*(i+1,j+1)) }; theorem :: GOBOARD6:65 1 <= j & j < width G & 1 <= i & i+1 < len G implies LSeg(1/2*(G*(i,j)+ G*(i+1,j+1)),1/2*(G*(i+1,j)+G*(i+2,j+1))) c= Int cell(G,i,j) \/ Int cell(G,i+1, j) \/ { 1/2*(G*(i+1,j)+G*(i+1,j+1)) }; theorem :: GOBOARD6:66 1 <= i & i < len G & 1 < width G implies LSeg(1/2*(G*(i,1)+G*(i+1,1))- |[0,1]|,1/2*(G*(i,1)+G*(i+1,2))) c= Int cell(G,i,0) \/ Int cell(G,i,1) \/ { 1/2 *(G*(i,1)+G*(i+1,1)) }; theorem :: GOBOARD6:67 1 <= i & i < len G & 1 < width G implies LSeg(1/2*(G*(i,width G)+G*(i+ 1,width G))+|[0,1]|, 1/2*(G*(i,width G)+G*(i+1,width G -' 1))) c= Int cell(G,i, width G -'1) \/ Int cell(G,i,width G) \/ { 1/2*(G*(i,width G)+G*(i+1,width G)) }; theorem :: GOBOARD6:68 1 <= j & j < width G & 1 < len G implies LSeg(1/2*(G*(1,j)+G*(1,j+1))- |[1,0]|,1/2*(G*(1,j)+G*(2,j+1))) c= Int cell(G,0,j) \/ Int cell(G,1,j) \/ { 1/2 *(G*(1,j)+G*(1,j+1)) }; theorem :: GOBOARD6:69 1 <= j & j < width G & 1 < len G implies LSeg(1/2*(G*(len G,j)+G*(len G,j+1))+|[1,0]|, 1/2*(G*(len G,j)+G*(len G -' 1,j+1))) c= Int cell(G,len G -' 1 ,j) \/ Int cell(G,len G,j) \/ { 1/2*(G*(len G,j)+G*(len G,j+1)) }; theorem :: GOBOARD6:70 1 < len G & 1 <= j & j+1 < width G implies LSeg(1/2*(G*(1,j)+G*(1,j+1) )-|[1,0]|,1/2*(G*(1,j+1)+G*(1,j+2))-|[1,0]|) c= Int cell(G,0,j) \/ Int cell(G,0 ,j+1) \/ { G*(1,j+1)-|[1,0]| }; theorem :: GOBOARD6:71 1 < len G & 1 <= j & j+1 < width G implies LSeg(1/2*(G*(len G,j)+G*( len G,j+1))+|[1,0]|, 1/2*(G*(len G,j+1)+G*(len G,j+2))+|[1,0]|) c= Int cell(G, len G,j) \/ Int cell(G,len G,j+1) \/ { G*(len G,j+1)+|[1,0]| }; theorem :: GOBOARD6:72 1 < width G & 1 <= i & i+1 < len G implies LSeg(1/2*(G*(i,1)+G*(i+1,1) )-|[0,1]|,1/2*(G*(i+1,1)+G*(i+2,1))-|[0,1]|) c= Int cell(G,i,0) \/ Int cell(G,i +1,0) \/ { G*(i+1,1)-|[0,1]| }; theorem :: GOBOARD6:73 1 < width G & 1 <= i & i+1 < len G implies LSeg(1/2*(G*(i,width G)+G*( i+1,width G))+|[0,1]|, 1/2*(G*(i+1,width G)+G*(i+2,width G))+|[0,1]|) c= Int cell(G,i,width G) \/ Int cell(G,i+1,width G) \/ { G*(i+1,width G)+|[0,1]| }; theorem :: GOBOARD6:74 1 < len G & 1 < width G implies LSeg(G*(1,1)-|[1,1]|,1/2*(G*(1,1)+G*(1 ,2))-|[1,0]|) c= Int cell(G,0,0) \/ Int cell(G,0,1) \/ { G*(1,1)-|[1,0]| }; theorem :: GOBOARD6:75 1 < len G & 1 < width G implies LSeg(G*(len G,1)+|[1,-1]|,1/2*(G*(len G,1)+G*(len G,2))+|[1,0]|) c= Int cell(G,len G,0) \/ Int cell(G,len G,1) \/ { G *(len G,1)+|[1,0]| }; theorem :: GOBOARD6:76 1 < len G & 1 < width G implies LSeg(G*(1,width G)+|[-1,1]|,1/2*(G*(1, width G)+G* (1,width G -' 1))-|[1,0]|) c= Int cell(G,0,width G) \/ Int cell(G,0 ,width G -' 1) \/ { G*(1,width G)-|[1,0]| }; theorem :: GOBOARD6:77 1 < len G & 1 < width G implies LSeg(G*(len G,width G)+|[1,1]|, 1/2*(G *(len G,width G)+G*(len G,width G -' 1))+|[1,0]|) c= Int cell(G,len G,width G) \/ Int cell(G,len G,width G -' 1) \/ { G*(len G,width G)+|[1,0]| }; theorem :: GOBOARD6:78 1 < width G & 1 < len G implies LSeg(G*(1,1)-|[1,1]|,1/2*(G*(1,1)+G*(2 ,1))-|[0,1]|) c= Int cell(G,0,0) \/ Int cell(G,1,0) \/ { G*(1,1)-|[0,1]| }; theorem :: GOBOARD6:79 1 < width G & 1 < len G implies LSeg(G*(1,width G)+|[-1,1]|,1/2*(G*(1, width G)+G*(2,width G))+|[0,1]|) c= Int cell(G,0,width G) \/ Int cell(G,1,width G) \/ { G*(1,width G)+|[0,1]| }; theorem :: GOBOARD6:80 1 < width G & 1 < len G implies LSeg(G*(len G,1)+|[1,-1]|,1/2*(G*(len G,1)+G*(len G -' 1,1))-|[0,1]|) c= Int cell(G,len G,0) \/ Int cell(G,len G -' 1 ,0) \/ { G*(len G,1)-|[0,1]| }; theorem :: GOBOARD6:81 1 < width G & 1 < len G implies LSeg(G*(len G,width G)+|[1,1]|, 1/2*(G *(len G,width G)+G*(len G -' 1,width G))+|[0,1]|) c= Int cell(G,len G,width G) \/ Int cell(G,len G -' 1,width G) \/ { G*(len G,width G)+|[0,1]| }; theorem :: GOBOARD6:82 1 <= i & i+1 <= len G & 1 <= j & j+1 <= width G implies LSeg(1/2*(G*(i ,j)+G*(i+1,j+1)),p) meets Int cell(G,i,j); theorem :: GOBOARD6:83 1 <= i & i+1 <= len G implies LSeg(p,1/2*(G*(i,width G)+G*(i+1,width G ))+|[0,1]|) meets Int cell(G,i,width G); theorem :: GOBOARD6:84 1 <= i & i+1 <= len G implies LSeg(1/2*(G*(i,1)+G*(i+1,1))-|[0,1]|,p) meets Int cell(G,i,0); theorem :: GOBOARD6:85 1 <= j & j+1 <= width G implies LSeg(1/2*(G*(1,j)+G*(1,j+1))-|[1,0]|,p ) meets Int cell(G,0,j); theorem :: GOBOARD6:86 1 <= j & j+1 <= width G implies LSeg(p,1/2*(G*(len G,j)+G*(len G,j+1)) +|[1,0]|) meets Int cell(G,len G,j); theorem :: GOBOARD6:87 LSeg(p,G*(1,1)-|[1,1]|) meets Int cell(G,0,0); theorem :: GOBOARD6:88 LSeg(p,G*(len G,width G)+|[1,1]|) meets Int cell(G,len G,width G); theorem :: GOBOARD6:89 LSeg(p,G*(1,width G)+|[-1,1]|) meets Int cell(G,0,width G); theorem :: GOBOARD6:90 LSeg(p,G*(len G,1)+|[1,-1]|) meets Int cell(G,len G,0); theorem :: GOBOARD6:91 for M being non empty MetrSpace, p being Point of M, q being Point of TopSpaceMetr M, r being Real st p = q & r > 0 holds Ball (p, r) is a_neighborhood of q; theorem :: GOBOARD6:92 for M being non empty MetrSpace, A being Subset of TopSpaceMetr M, p being Point of M holds p in Cl A iff for r being Real st r > 0 holds Ball (p, r) meets A; :: Moved from JORDAN19, AG 20.01.2006 theorem :: GOBOARD6:93 for A be Subset of TOP-REAL n for p be Point of TOP-REAL n for p9 be Point of Euclid n st p = p9 for s be Real st s > 0 holds p in Cl A iff for r be Real st 0 < r & r < s holds Ball (p9,r) meets A;