Nuprl Definition : in-eclass
e ∈b X == (#(X eo e) =z 1)
Definitions occuring in Statement :
eq_int: (i =z j),
apply: f a,
natural_number: $n,
bag-size: #(bs)
FDL editor aliases :
in-eclass
e \mmember{}\msubb{} X == (\#(X eo e) =\msubz{} 1)
Date html generated:
2015_07_17-PM-00_40_07
Last ObjectModification:
2012_02_25-PM-01_18_15
Home
Index