Nuprl Definition : class-value-has
X(e) has a == (↑e ∈b X) ∧ (¬a#X(e):T)
Definitions occuring in Statement :
eclass-val: X(e),
in-eclass: e ∈b X,
free-from-atom: a#x:T,
assert: ↑b,
not: ¬A,
and: P ∧ Q
FDL editor aliases :
class-value-has
Latex:
X(e) has a == (\muparrow{}e \mmember{}\msubb{} X) \mwedge{} (\mneg{}a\#X(e):T)
Date html generated:
2015_07_23-PM-00_00_07
Last ObjectModification:
2012_08_30-PM-02_30_09
Home
Index