:: Introduction to Go-Board - Part II.Go-Board Determined by Finite Sequence of point from ${\calE}^2_{\rm T}$
:: by Jaros{\l}aw Kotowicz and Yatsuka Nakamura
::
:: Received August 24, 1992
:: Copyright (c) 1992 Association of Mizar Users
defpred S1[ Nat] means for R being finite Subset of REAL st R <> {} & card R = $1 holds
( R is bounded_above & upper_bound R in R & R is bounded_below & lower_bound R in R );
Lm1:
S1[ 0 ]
;
Lm2:
for n being Element of NAT st S1[n] holds
S1[n + 1]
Lm3:
for n being Element of NAT holds S1[n]
from NAT_1:sch 1(Lm1, Lm2);
theorem Th1: :: GOBOARD2:1
theorem :: GOBOARD2:2
canceled;
theorem Th3: :: GOBOARD2:3
theorem Th4: :: GOBOARD2:4
theorem Th5: :: GOBOARD2:5
theorem :: GOBOARD2:6
theorem :: GOBOARD2:7
theorem Th8: :: GOBOARD2:8
theorem :: GOBOARD2:9
theorem :: GOBOARD2:10
theorem Th11: :: GOBOARD2:11
theorem :: GOBOARD2:12
theorem :: GOBOARD2:13
theorem Th14: :: GOBOARD2:14
theorem Th15: :: GOBOARD2:15
theorem Th16: :: GOBOARD2:16
theorem :: GOBOARD2:17
theorem :: GOBOARD2:18
theorem Th19: :: GOBOARD2:19
theorem Th20: :: GOBOARD2:20
defpred S2[ Element of NAT ] means for v being FinSequence of REAL st card (rng v) = $1 holds
ex v1 being FinSequence of REAL st
( rng v1 = rng v & len v1 = card (rng v) & v1 is increasing );
Lm4:
S2[ 0 ]
Lm5:
for n being Element of NAT st S2[n] holds
S2[n + 1]
Lm6:
for n being Element of NAT holds S2[n]
from NAT_1:sch 1(Lm4, Lm5);
theorem :: GOBOARD2:21
defpred S3[ Element of NAT ] means for v1, v2 being FinSequence of REAL st len v1 = $1 & len v2 = $1 & rng v1 = rng v2 & v1 is increasing & v2 is increasing holds
v1 = v2;
Lm7:
S3[ 0 ]
Lm8:
for n being Element of NAT st S3[n] holds
S3[n + 1]
Lm9:
for n being Element of NAT holds S3[n]
from NAT_1:sch 1(Lm7, Lm8);
theorem :: GOBOARD2:22
definition
let v1,
v2 be
FinSequence of
REAL ;
assume A1:
(
v1 <> {} &
v2 <> {} )
;
func GoB v1,
v2 -> Matrix of
(TOP-REAL 2) means :
Def1:
:: GOBOARD2:def 1
(
len it = len v1 &
width it = len v2 & ( for
n,
m being
Element of
NAT st
[n,m] in Indices it holds
it * n,
m = |[(v1 . n),(v2 . m)]| ) );
existence
ex b1 being Matrix of (TOP-REAL 2) st
( len b1 = len v1 & width b1 = len v2 & ( for n, m being Element of NAT st [n,m] in Indices b1 holds
b1 * n,m = |[(v1 . n),(v2 . m)]| ) )
uniqueness
for b1, b2 being Matrix of (TOP-REAL 2) st len b1 = len v1 & width b1 = len v2 & ( for n, m being Element of NAT st [n,m] in Indices b1 holds
b1 * n,m = |[(v1 . n),(v2 . m)]| ) & len b2 = len v1 & width b2 = len v2 & ( for n, m being Element of NAT st [n,m] in Indices b2 holds
b2 * n,m = |[(v1 . n),(v2 . m)]| ) holds
b1 = b2
end;
:: deftheorem Def1 defines GoB GOBOARD2:def 1 :
:: deftheorem Def2 defines Incr GOBOARD2:def 2 :
:: deftheorem defines GoB GOBOARD2:def 3 :
theorem Th23: :: GOBOARD2:23
theorem Th24: :: GOBOARD2:24
theorem :: GOBOARD2:25
theorem :: GOBOARD2:26
theorem :: GOBOARD2:27
theorem :: GOBOARD2:28
theorem :: GOBOARD2:29