Nuprl Definition : es-total-class
es-total-class(es;X) == ∀e:E. (1 ≤ #(X(e)))
Definitions occuring in Statement :
class-ap: X(e),
es-E: E,
le: A ≤ B,
all: ∀x:A. B[x],
natural_number: $n,
bag-size: #(bs)
FDL editor aliases :
es-total-class
es-total-class(es;X) == \mforall{}e:E. (1 \mleq{} \#(X(e)))
Date html generated:
2015_07_17-PM-00_18_54
Last ObjectModification:
2013_01_11-PM-04_02_51
Home
Index