Nuprl Definition : es-functional-class-at
X is functional at e == single-valued-classrel(es;X;T) ∧ (↑e ∈b X)
Definitions occuring in Statement :
single-valued-classrel: single-valued-classrel(es;X;T),
member-eclass: e ∈b X,
assert: ↑b,
and: P ∧ Q
FDL editor aliases :
init-es-functional-class-at
X is functional at e == single-valued-classrel(es;X;T) \mwedge{} (\muparrow{}e \mmember{}\msubb{} X)
Date html generated:
2015_07_17-PM-00_20_41
Last ObjectModification:
2013_06_05-PM-00_14_58
Home
Index