Nuprl Definition : p-open-member
s ∈ C == ∃n:ℕ. ((C <n, s>) = 1 ∈ ℤ)
Definitions occuring in Statement :
nat: ℕ,
exists: ∃x:A. B[x],
apply: f a,
pair: <a, b>,
natural_number: $n,
int: ℤ,
equal: s = t ∈ T
Definitions :
exists: ∃x:A. B[x],
nat: ℕ,
equal: s = t ∈ T,
int: ℤ,
apply: f a,
pair: <a, b>,
natural_number: $n
FDL editor aliases :
p-open-member
s \mmember{} C == \mexists{}n:\mBbbN{}. ((C <n, s>) = 1)
Date html generated:
2015_07_17-AM-07_59_56
Last ObjectModification:
2008_02_27-PM-05_49_24
Home
Index