Nuprl Definition : l_all
(∀x∈L.P[x]) == ∀i:ℕ||L||. P[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 :
all: ∀x:A. B[x],
int_seg: {i..j-},
natural_number: $n,
length: ||as||,
select: L[n]
FDL editor aliases :
l_all
Latex:
(\mforall{}x\mmember{}L.P[x]) == \mforall{}i:\mBbbN{}||L||. P[L[i]]
Date html generated:
2016_05_14-AM-06_39_24
Last ObjectModification:
2015_12_03-PM-02_06_59
Theory : list_0
Home
Index