Nuprl Lemma : mapfilter-subbag

`∀T,U:Type. ∀f:T ─→ U. ∀P,Q:T ─→ 𝔹. ∀L:T List.`
`  ((∀t:T. ((↑(P t)) `` (↑(Q t)))) `` sub-bag(U;mapfilter(f;P;L);mapfilter(f;Q;L)))`

Proof

Definitions occuring in Statement :  mapfilter: `mapfilter(f;P;L)` list: `T List` assert: `↑b` bool: `𝔹` all: `∀x:A. B[x]` implies: `P `` Q` apply: `f a` function: `x:A ─→ B[x]` universe: `Type` sub-bag: `sub-bag(T;as;bs)`
Lemmas :  mapfilter_wf bnot_wf bool_wf eqtt_to_assert equal_wf bool_cases_sqequal subtype_base_sq bool_subtype_base eqff_to_assert assert-bnot subtype_rel_dep_function assert_wf set_wf list-subtype-bag mapfilter-bor-eq bag_wf bag-append_wf all_wf list_wf append_wf bfalse_wf iff_imp_equal_bool btrue_wf true_wf not_wf false_wf iff_transitivity iff_weakening_uiff assert_of_band assert_of_bnot iff_wf mapfilter-nil l_member_wf int_seg_wf length_wf append-nil subtype_rel_list top_wf

Latex:
\mforall{}T,U:Type.  \mforall{}f:T  {}\mrightarrow{}  U.  \mforall{}P,Q:T  {}\mrightarrow{}  \mBbbB{}.  \mforall{}L:T  List.
((\mforall{}t:T.  ((\muparrow{}(P  t))  {}\mRightarrow{}  (\muparrow{}(Q  t))))  {}\mRightarrow{}  sub-bag(U;mapfilter(f;P;L);mapfilter(f;Q;L)))

Date html generated: 2015_07_21-PM-04_52_50
Last ObjectModification: 2015_01_28-AM-08_43_47

Home Index