Nuprl Definition : strict-bag-function
strict-bag-function(G;L;B;S) == ∀x:tuple-type(map(λT.bag(T);L)). ((∀i∈S.x.i = {} ∈ bag(L[i])) ⇒ ((G x) = {} ∈ bag(B)))
Definitions occuring in Statement :
empty-bag: {},
bag: bag(T),
select-tuple: x.n,
tuple-type: tuple-type(L),
l_all: (∀x∈L.P[x]),
select: L[n],
length: ||as||,
map: map(f;as),
all: ∀x:A. B[x],
implies: P ⇒ Q,
apply: f a,
lambda: λx.A[x],
equal: s = t ∈ T
Definitions occuring in definition :
all: ∀x:A. B[x],
tuple-type: tuple-type(L),
map: map(f;as),
lambda: λx.A[x],
implies: P ⇒ Q,
l_all: (∀x∈L.P[x]),
select: L[n],
select-tuple: x.n,
length: ||as||,
equal: s = t ∈ T,
bag: bag(T),
apply: f a,
empty-bag: {}
FDL editor aliases :
strict-bag-function
Latex:
strict-bag-function(G;L;B;S) == \mforall{}x:tuple-type(map(\mlambda{}T.bag(T);L)). ((\mforall{}i\mmember{}S.x.i = \{\}) {}\mRightarrow{} ((G x) = \{\}))
Date html generated:
2016_05_15-PM-02_58_39
Last ObjectModification:
2015_09_23-AM-07_40_39
Theory : bags
Home
Index