Nuprl Definition : pairwise
(∀x,y∈L. P[x; y]) == ∀i:ℕ||L||. ∀j:ℕi. P[L[j]; L[i]]
Definitions occuring in Statement :
select: L[n],
length: ||as||,
int_seg: {i..j-},
all: ∀x:A. B[x],
natural_number: $n
Definitions occuring in definition :
length: ||as||,
all: ∀x:A. B[x],
int_seg: {i..j-},
natural_number: $n,
select: L[n]
FDL editor aliases :
pairwise
Latex:
(\mforall{}x,y\mmember{}L. P[x; y]) == \mforall{}i:\mBbbN{}||L||. \mforall{}j:\mBbbN{}i. P[L[j]; L[i]]
Date html generated:
2016_05_14-PM-01_48_57
Last ObjectModification:
2015_09_22-PM-05_54_50
Theory : list_1
Home
Index