begin
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
canceled;
theorem
canceled;
theorem
canceled;
theorem Th4:
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:
theorem Th6:
theorem Th7:
Lm5:
for T being TopSpace
for A being Subset of T
for B being Subset of TopStruct(# the carrier of T,the topology of T #) st A = B holds
Int A = Int B
theorem Th8:
theorem Th9:
theorem Th10:
theorem Th11:
theorem Th12:
theorem Th13:
theorem Th14:
Lm6: TopStruct(# the carrier of (TOP-REAL 2),the topology of (TOP-REAL 2) #) =
TopSpaceMetr (Euclid 2)
by EUCLID:def 8
.=
TopStruct(# the carrier of (Euclid 2),(Family_open_set (Euclid 2)) #)
by PCOMPS_1:def 6
;
theorem Th15:
theorem Th16:
theorem Th17:
theorem Th18:
theorem Th19:
theorem Th20:
theorem Th21:
theorem Th22:
theorem Th23:
theorem Th24:
theorem Th25:
theorem Th26:
theorem Th27:
theorem Th28:
theorem Th29:
theorem
theorem
theorem
theorem
theorem Th34:
theorem Th35:
theorem Th36:
theorem Th37:
theorem Th38:
theorem Th39:
theorem Th40:
theorem Th41:
theorem Th42:
theorem Th43:
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:
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:
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:
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:
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:
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:
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:
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:
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:
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:
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:
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:
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:
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:
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:
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:
theorem Th60:
theorem Th61:
theorem Th62:
theorem Th63:
theorem Th64:
theorem Th65:
theorem Th66:
theorem
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
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
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
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
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
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))))}
Lm7:
(1 / 2) + (1 / 2) = 1
;
theorem
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
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
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
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
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
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
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
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
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
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
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
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
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem Th94:
theorem
theorem