Nuprl Definition : l_exists
(∃x∈L. P[x]) == ∃i:ℕ||L||. P[L[i]]
Definitions occuring in Statement :
select: L[n],
length: ||as||,
int_seg: {i..j-},
exists: ∃x:A. B[x],
natural_number: $n
Definitions occuring in definition :
exists: ∃x:A. B[x],
int_seg: {i..j-},
natural_number: $n,
length: ||as||,
select: L[n]
FDL editor aliases :
l_exists
Latex:
(\mexists{}x\mmember{}L. P[x]) == \mexists{}i:\mBbbN{}||L||. P[L[i]]
Date html generated:
2016_05_14-AM-06_39_32
Last ObjectModification:
2015_12_03-PM-02_07_03
Theory : list_0
Home
Index