Nuprl Definition : classrel-list
classrel-list(es;A;X;L;e) ==
(∀p:A × E. ((p ∈ L) ⇒ fst(p) ∈ X(snd(p))))
∧ sorted-by(λp1,p2. (snd(p1) <loc snd(p2));L)
∧ no_repeats(E;map(λp.(snd(p));L))
∧ (∀e':E. (e' ≤loc e ∧ (∃a:A. a ∈ X(e')) ⇐⇒ (e' ∈ map(λp.(snd(p));L))))
Definitions occuring in Statement :
classrel: v ∈ X(e),
es-le: e ≤loc e' ,
es-locl: (e <loc e'),
es-E: E,
sorted-by: sorted-by(R;L),
no_repeats: no_repeats(T;l),
l_member: (x ∈ l),
map: map(f;as),
pi1: fst(t),
pi2: snd(t),
all: ∀x:A. B[x],
exists: ∃x:A. B[x],
iff: P ⇐⇒ Q,
implies: P ⇒ Q,
and: P ∧ Q,
lambda: λx.A[x],
product: x:A × B[x]
FDL editor aliases :
classrel-list
Latex:
classrel-list(es;A;X;L;e) ==
(\mforall{}p:A \mtimes{} E. ((p \mmember{} L) {}\mRightarrow{} fst(p) \mmember{} X(snd(p))))
\mwedge{} sorted-by(\mlambda{}p1,p2. (snd(p1) <loc snd(p2));L)
\mwedge{} no\_repeats(E;map(\mlambda{}p.(snd(p));L))
\mwedge{} (\mforall{}e':E. (e' \mleq{}loc e \mwedge{} (\mexists{}a:A. a \mmember{} X(e')) \mLeftarrow{}{}\mRightarrow{} (e' \mmember{} map(\mlambda{}p.(snd(p));L))))
Date html generated:
2015_07_22-PM-00_17_28
Last ObjectModification:
2012_11_29-AM-11_16_04
Home
Index