Nuprl Definition : es-sv-class
es-sv-class(es;X) == ∀e:E. (#(X es e) ≤ 1)
Definitions occuring in Statement :
es-E: E,
le: A ≤ B,
all: ∀x:A. B[x],
apply: f a,
natural_number: $n,
bag-size: #(bs)
FDL editor aliases :
es-sv-class
es-sv-class(es;X) == \mforall{}e:E. (\#(X es e) \mleq{} 1)
Date html generated:
2015_07_17-PM-00_19_06
Last ObjectModification:
2012_02_25-PM-01_13_39
Home
Index