Nuprl Definition : set-member
(x ∈ s) == let I,f = s in ∃i:I. (x = (f i) ∈ T)
Definitions occuring in Statement :
exists: ∃x:A. B[x],
apply: f a,
spread: spread def,
equal: s = t ∈ T
Definitions occuring in definition :
spread: spread def,
exists: ∃x:A. B[x],
equal: s = t ∈ T,
apply: f a
FDL editor aliases :
set-member
Latex:
(x \mmember{} s) == let I,f = s in \mexists{}i:I. (x = (f i))
Date html generated:
2016_05_13-PM-03_51_36
Last ObjectModification:
2015_09_22-PM-05_45_24
Theory : bar-induction
Home
Index