Nuprl Definition : es-class-def
∀a,e such that R[e; a]
e∈X with value F[e; a] ==
(∀e:E. (↑e ∈b X ⇐⇒ ∃a:A. R[e; a])) ∧ (∀e:E. ∀a:A. (R[e; a] ⇒ (X(e) = F[e; a] ∈ B)))
Definitions occuring in Statement :
eclass-val: X(e),
in-eclass: e ∈b X,
es-E: E,
assert: ↑b,
all: ∀x:A. B[x],
exists: ∃x:A. B[x],
iff: P ⇐⇒ Q,
implies: P ⇒ Q,
and: P ∧ Q,
equal: s = t ∈ T
FDL editor aliases :
es-class-def
Latex:
\mforall{}a,e such that R[e; a]
e\mmember{}X with value F[e; a] ==
(\mforall{}e:E. (\muparrow{}e \mmember{}\msubb{} X \mLeftarrow{}{}\mRightarrow{} \mexists{}a:A. R[e; a])) \mwedge{} (\mforall{}e:E. \mforall{}a:A. (R[e; a] {}\mRightarrow{} (X(e) = F[e; a])))
Date html generated:
2015_07_21-PM-03_25_49
Last ObjectModification:
2012_02_25-PM-02_24_21
Home
Index