Nuprl Definition : l_member
(x ∈ l) == ∃i:ℕ. (i < ||l|| c∧ (x = l[i] ∈ T))
Definitions occuring in Statement :
select: L[n],
length: ||as||,
nat: ℕ,
less_than: a < b,
cand: A c∧ B,
exists: ∃x:A. B[x],
equal: s = t ∈ T
Definitions occuring in definition :
exists: ∃x:A. B[x],
nat: ℕ,
cand: A c∧ B,
less_than: a < b,
length: ||as||,
equal: s = t ∈ T,
select: L[n]
FDL editor aliases :
l_member
Latex:
(x \mmember{} l) == \mexists{}i:\mBbbN{}. (i < ||l|| c\mwedge{} (x = l[i]))
Date html generated:
2016_05_14-AM-06_36_02
Last ObjectModification:
2015_12_03-PM-02_06_31
Theory : list_0
Home
Index