:: On the Geometry of a Go-board
:: by Andrzej Trybulec
::
:: Received July 9, 1995
:: Copyright (c) 1995 Association of Mizar Users
Lm1:
for p, q being Point of (TOP-REAL 2) holds
( (p + q) `1 = (p `1 ) + (q `1 ) & (p + q) `2 = (p `2 ) + (q `2 ) )
Lm2:
for p, q being Point of (TOP-REAL 2) holds
( (p - q) `1 = (p `1 ) - (q `1 ) & (p - q) `2 = (p `2 ) - (q `2 ) )
Lm3:
for r being Real
for p being Point of (TOP-REAL 2) holds
( (r * p) `1 = r * (p `1 ) & (r * p) `2 = r * (p `2 ) )
theorem :: GOBOARD6:1
canceled;
theorem :: GOBOARD6:2
canceled;
theorem :: GOBOARD6:3
canceled;
theorem Th4: :: GOBOARD6:4
Lm4:
for M being MetrSpace
for B being Subset of (TopSpaceMetr M)
for r being real number
for u being Point of M st B = Ball u,r holds
B is open
theorem Th5: :: GOBOARD6:5
theorem :: GOBOARD6:6
theorem Th7: :: GOBOARD6:7
theorem :: GOBOARD6:8
theorem Th9: :: GOBOARD6:9
theorem Th10: :: GOBOARD6:10
theorem Th11: :: GOBOARD6:11
theorem Th12: :: GOBOARD6:12
theorem Th13: :: GOBOARD6:13
theorem Th14: :: GOBOARD6:14
Lm5:
TOP-REAL 2 = TopStruct(# the carrier of (Euclid 2),(Family_open_set (Euclid 2)) #)
by PCOMPS_1:def 6;
theorem Th15: :: GOBOARD6:15
theorem Th16: :: GOBOARD6:16
theorem Th17: :: GOBOARD6:17
theorem Th18: :: GOBOARD6:18
theorem Th19: :: GOBOARD6:19
theorem Th20: :: GOBOARD6:20
theorem Th21: :: GOBOARD6:21
theorem Th22: :: GOBOARD6:22
theorem Th23: :: GOBOARD6:23
theorem Th24: :: GOBOARD6:24
theorem Th25: :: GOBOARD6:25
theorem Th26: :: GOBOARD6:26
theorem Th27: :: GOBOARD6:27
theorem Th28: :: GOBOARD6:28
theorem Th29: :: GOBOARD6:29
theorem :: GOBOARD6:30
theorem :: GOBOARD6:31
theorem :: GOBOARD6:32
theorem :: GOBOARD6:33
theorem Th34: :: GOBOARD6:34
theorem Th35: :: GOBOARD6:35
theorem Th36: :: GOBOARD6:36
theorem Th37: :: GOBOARD6:37
theorem Th38: :: GOBOARD6:38
theorem Th39: :: GOBOARD6:39
theorem Th40: :: GOBOARD6:40
theorem Th41: :: GOBOARD6:41
theorem Th42: :: GOBOARD6:42
theorem Th43: :: GOBOARD6:43
for
i,
j being
Element of
NAT for
G being
Go-board st 1
<= i &
i < len G & 1
<= j &
j < width G holds
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 Th44: :: GOBOARD6:44
for
i,
j being
Element of
NAT for
G being
Go-board st 1
<= i &
i < len G & 1
<= j &
j < width G holds
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 Th45: :: GOBOARD6:45
for
i,
j being
Element of
NAT for
G being
Go-board st 1
<= i &
i < len G & 1
<= j &
j < width G holds
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 Th46: :: GOBOARD6:46
for
i,
j being
Element of
NAT for
G being
Go-board st 1
<= i &
i < len G & 1
<= j &
j < width G holds
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 Th47: :: GOBOARD6:47
for
j being
Element of
NAT for
G being
Go-board st 1
<= j &
j < width G holds
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 Th48: :: GOBOARD6:48
for
j being
Element of
NAT for
G being
Go-board st 1
<= j &
j < width G holds
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 Th49: :: GOBOARD6:49
for
i being
Element of
NAT for
G being
Go-board st 1
<= i &
i < len G holds
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 Th50: :: GOBOARD6:50
for
i being
Element of
NAT for
G being
Go-board st 1
<= i &
i < len G holds
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 Th51: :: GOBOARD6:51
for
j being
Element of
NAT for
G being
Go-board st 1
<= j &
j < width G holds
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 Th52: :: GOBOARD6:52
for
j being
Element of
NAT for
G being
Go-board st 1
<= j &
j < width G holds
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 Th53: :: GOBOARD6:53
for
j being
Element of
NAT for
G being
Go-board st 1
<= j &
j < width G holds
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 Th54: :: GOBOARD6:54
for
j being
Element of
NAT for
G being
Go-board st 1
<= j &
j < width G holds
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 Th55: :: GOBOARD6:55
for
i being
Element of
NAT for
G being
Go-board st 1
<= i &
i < len G holds
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 Th56: :: GOBOARD6:56
for
i being
Element of
NAT for
G being
Go-board st 1
<= i &
i < len G holds
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 Th57: :: GOBOARD6:57
for
i being
Element of
NAT for
G being
Go-board st 1
<= i &
i < len G holds
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 Th58: :: GOBOARD6:58
for
i being
Element of
NAT for
G being
Go-board st 1
<= i &
i < len G holds
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 Th59: :: GOBOARD6:59
theorem Th60: :: GOBOARD6:60
theorem Th61: :: GOBOARD6:61
theorem Th62: :: GOBOARD6:62
theorem Th63: :: GOBOARD6:63
theorem Th64: :: GOBOARD6:64
theorem Th65: :: GOBOARD6:65
theorem Th66: :: GOBOARD6:66
theorem :: GOBOARD6:67
for
i,
j being
Element of
NAT for
G being
Go-board st 1
<= i &
i < len G & 1
<= j &
j + 1
< width G holds
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:68
for
j,
i being
Element of
NAT for
G being
Go-board st 1
<= j &
j < width G & 1
<= i &
i + 1
< len G holds
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:69
for
i being
Element of
NAT for
G being
Go-board st 1
<= i &
i < len G & 1
< width G holds
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:70
for
i being
Element of
NAT for
G being
Go-board st 1
<= i &
i < len G & 1
< width G holds
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:71
for
j being
Element of
NAT for
G being
Go-board st 1
<= j &
j < width G & 1
< len G holds
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:72
for
j being
Element of
NAT for
G being
Go-board st 1
<= j &
j < width G & 1
< len G holds
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))))}
Lm6:
(1 / 2) + (1 / 2) = 1
;
theorem :: GOBOARD6:73
for
j being
Element of
NAT for
G being
Go-board st 1
< len G & 1
<= j &
j + 1
< width G holds
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:74
for
j being
Element of
NAT for
G being
Go-board st 1
< len G & 1
<= j &
j + 1
< width G holds
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:75
for
i being
Element of
NAT for
G being
Go-board st 1
< width G & 1
<= i &
i + 1
< len G holds
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:76
for
i being
Element of
NAT for
G being
Go-board st 1
< width G & 1
<= i &
i + 1
< len G holds
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:77
for
G being
Go-board st 1
< len G & 1
< width G holds
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:78
for
G being
Go-board st 1
< len G & 1
< width G holds
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:79
for
G being
Go-board st 1
< len G & 1
< width G holds
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:80
for
G being
Go-board st 1
< len G & 1
< width G holds
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:81
for
G being
Go-board st 1
< width G & 1
< len G holds
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:82
for
G being
Go-board st 1
< width G & 1
< len G holds
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:83
for
G being
Go-board st 1
< width G & 1
< len G holds
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:84
for
G being
Go-board st 1
< width G & 1
< len G holds
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:85
theorem :: GOBOARD6:86
theorem :: GOBOARD6:87
theorem :: GOBOARD6:88
theorem :: GOBOARD6:89
theorem :: GOBOARD6:90
theorem :: GOBOARD6:91
theorem :: GOBOARD6:92
theorem :: GOBOARD6:93
theorem Th94: :: GOBOARD6:94
theorem :: GOBOARD6:95
theorem :: GOBOARD6:96