Nuprl Definition : es-interface-pair-prior
X;Y == λes,e. if e ∈b (X)' ∧b e ∈b Y then {<(X)'(e), Y(e)>} else {} fi
Definitions occuring in Statement :
es-prior-val: (X)',
eclass-val: X(e),
in-eclass: e ∈b X,
band: p ∧b q,
ifthenelse: if b then t else f fi ,
lambda: λx.A[x],
pair: <a, b>,
single-bag: {x},
empty-bag: {}
FDL editor aliases :
es-interface-pair-prior
Latex:
X;Y == \mlambda{}es,e. if e \mmember{}\msubb{} (X)' \mwedge{}\msubb{} e \mmember{}\msubb{} Y then \{<(X)'(e), Y(e)>\} else \{\} fi
Date html generated:
2015_07_21-PM-03_47_06
Last ObjectModification:
2012_02_25-PM-02_46_57
Home
Index