Nuprl Lemma : mapfilter-bor

T,U:Type.

f:T

U.

P,Q:T

.

L:T List.
sub-bag(U;mapfilter(f;

x.(P[x]

Q[x]);L);mapfilter(f;P;L) @ mapfilter(f;Q;L))

Proof not projected

Definitions occuring in Statement : append: as @ bs, bor: p

q, bool:

, so_apply: x[s], all:

x:A. B[x], lambda:

x.A[x], function: x:A

B[x], list: type List, universe: Type, mapfilter: mapfilter(f;P;L), sub-bag: sub-bag(T;as;bs)
Definitions : all:

x:A. B[x], sub-bag: sub-bag(T;as;bs), so_apply: x[s], exists:

x:A. B[x], bag-append: as + bs, member: t

T, subtype: S

T, suptype: suptype(S; T), uall:

[x:A]. B[x], prop:

Lemmas : mapfilter_wf, band_wf, assert_wf, bag_qinc, mapfilter-bor-eq, equal_wf, bag_wf, append_wf, bag-append_wf, bor_wf, bool_wf

\mforall{}T,U:Type. \mforall{}f:T {}\mrightarrow{} U. \mforall{}P,Q:T {}\mrightarrow{} \mBbbB{}. \mforall{}L:T List. sub-bag(U;mapfilter(f;\mlambda{}x.(P[x] \mvee{}\msubb{}Q[x]);L);mapfilter(f;P;L) @ mapfilter(f;Q;L)) Date html generated: 2012_01_23-PM-12_49_38 Last ObjectModification: 2011_12_01-PM-02_07_16 Home Index