Nuprl Definition : oalist
oal(a;b) == {ps:(a × (b↓set)) List| (↑sd_ordered(map(λx.(fst(x));ps))) ∧ (¬↑(e ∈b map(λx.(snd(x));ps)))}
Definitions occuring in Statement :
sd_ordered: sd_ordered(as),
mem: a ∈b as,
dset_list: s List,
map: map(f;as),
assert: ↑b,
pi1: fst(t),
pi2: snd(t),
not: ¬A,
and: P ∧ Q,
lambda: λx.A[x],
dset_of_mon: g↓set,
grp_id: e,
dset_set: dset_set,
set_prod: s × t
Definitions occuring in definition :
dset_set: dset_set,
dset_list: s List,
set_prod: s × t,
and: P ∧ Q,
sd_ordered: sd_ordered(as),
pi1: fst(t),
not: ¬A,
assert: ↑b,
mem: a ∈b as,
dset_of_mon: g↓set,
grp_id: e,
map: map(f;as),
lambda: λx.A[x],
pi2: snd(t)
Latex:
oal(a;b) ==
\{ps:(a \mtimes{} (b\mdownarrow{}set)) List|
(\muparrow{}sd\_ordered(map(\mlambda{}x.(fst(x));ps))) \mwedge{} (\mneg{}\muparrow{}(e \mmember{}\msubb{} map(\mlambda{}x.(snd(x));ps)))\}
Date html generated:
2016_05_16-AM-08_15_22
Last ObjectModification:
2015_09_23-AM-09_52_49
Theory : polynom_2
Home
Index