Nuprl Definition : square-board
square-board(n;T) == {s:T List List| (||s|| = n ∈ ℤ) ∧ (∀i:ℕn. (||s[i]|| = n ∈ ℤ))}
Definitions occuring in Statement :
select: L[n],
length: ||as||,
list: T List,
int_seg: {i..j-},
all: ∀x:A. B[x],
and: P ∧ Q,
set: {x:A| B[x]} ,
natural_number: $n,
int: ℤ,
equal: s = t ∈ T
Definitions occuring in definition :
set: {x:A| B[x]} ,
list: T List,
and: P ∧ Q,
all: ∀x:A. B[x],
int_seg: {i..j-},
natural_number: $n,
equal: s = t ∈ T,
int: ℤ,
length: ||as||,
select: L[n]
FDL editor aliases :
square-board
Latex:
square-board(n;T) == \{s:T List List| (||s|| = n) \mwedge{} (\mforall{}i:\mBbbN{}n. (||s[i]|| = n))\}
Date html generated:
2016_05_15-PM-03_13_49
Last ObjectModification:
2015_09_23-AM-07_42_45
Theory : general
Home
Index