### Nuprl Lemma : non-empty-bag-mapfilter-union-of-list

`∀[T:Type]`
`  ∀P:T ⟶ 𝔹. ∀f:T ⟶ Top. ∀L:bag(T) List.  (0 < #(bag-mapfilter(f;λx.P[x];bag-union(L))) `⇐⇒` (∃b∈L. 0 < #([x∈b|P[x]])))`

Proof

Definitions occuring in Statement :  bag-union: `bag-union(bbs)` bag-size: `#(bs)` bag-mapfilter: `bag-mapfilter(f;P;bs)` bag-filter: `[x∈b|p[x]]` bag: `bag(T)` l_exists: `(∃x∈L. P[x])` list: `T List` bool: `𝔹` less_than: `a < b` uall: `∀[x:A]. B[x]` top: `Top` so_apply: `x[s]` all: `∀x:A. B[x]` iff: `P `⇐⇒` Q` lambda: `λx.A[x]` function: `x:A ⟶ B[x]` natural_number: `\$n` universe: `Type`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` all: `∀x:A. B[x]` bag-union: `bag-union(bbs)` bag-mapfilter: `bag-mapfilter(f;P;bs)` bag-size: `#(bs)` bag-filter: `[x∈b|p[x]]` bag-map: `bag-map(f;bs)` member: `t ∈ T` top: `Top` so_lambda: `λ2x.t[x]` so_apply: `x[s]` subtype_rel: `A ⊆r B` uimplies: `b supposing a` prop: `ℙ` implies: `P `` Q` concat: `concat(ll)` iff: `P `⇐⇒` Q` and: `P ∧ Q` less_than: `a < b` squash: `↓T` less_than': `less_than'(a;b)` false: `False` rev_implies: `P `` Q` l_exists: `(∃x∈L. P[x])` exists: `∃x:A. B[x]` select: `L[n]` nil: `[]` it: `⋅` so_lambda: `λ2x y.t[x; y]` so_apply: `x[s1;s2]` guard: `{T}` int_seg: `{i..j-}` lelt: `i ≤ j < k` satisfiable_int_formula: `satisfiable_int_formula(fmla)` not: `¬A` nat: `ℕ` decidable: `Dec(P)` or: `P ∨ Q` uiff: `uiff(P;Q)` ge: `i ≥ j ` nat_plus: `ℕ+`
Lemmas referenced :  length-map top_wf bag-filter_wf bag-union_wf list-subtype-bag bag_wf subtype_rel_self list_wf bool_wf list_induction iff_wf less_than_wf bag-size_wf assert_wf reduce_nil_lemma filter_nil_lemma length_of_nil_lemma stuck-spread base_wf int_seg_properties satisfiable-full-omega-tt intformand_wf intformless_wf itermVar_wf itermConstant_wf intformle_wf int_formula_prop_and_lemma int_formula_prop_less_lemma int_term_value_var_lemma int_term_value_constant_lemma int_formula_prop_le_lemma int_formula_prop_wf l_exists_wf_nil reduce_cons_lemma filter_append_sq length-append decidable__lt nat_wf l_exists_wf l_member_wf add-is-int-iff intformnot_wf itermAdd_wf int_formula_prop_not_lemma int_term_value_add_lemma false_wf nat_properties add_nat_plus nat_plus_wf nat_plus_properties intformeq_wf int_formula_prop_eq_lemma equal_wf or_wf l_exists_cons cons_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation lambdaFormation sqequalRule cut introduction extract_by_obid sqequalHypSubstitution isectElimination thin isect_memberEquality voidElimination voidEquality hypothesis cumulativity hypothesisEquality lambdaEquality applyEquality functionExtensionality because_Cache independent_isectElimination functionEquality universeEquality setEquality independent_functionElimination rename dependent_functionElimination independent_pairFormation imageElimination productElimination natural_numberEquality baseClosed setElimination dependent_pairFormation int_eqEquality intEquality computeAll unionElimination inlFormation inrFormation equalityTransitivity equalitySymmetry pointwiseFunctionality promote_hyp baseApply closedConclusion addEquality applyLambdaEquality dependent_set_memberEquality addLevel impliesFunctionality

Latex:
\mforall{}[T:Type]
\mforall{}P:T  {}\mrightarrow{}  \mBbbB{}.  \mforall{}f:T  {}\mrightarrow{}  Top.  \mforall{}L:bag(T)  List.
(0  <  \#(bag-mapfilter(f;\mlambda{}x.P[x];bag-union(L)))  \mLeftarrow{}{}\mRightarrow{}  (\mexists{}b\mmember{}L.  0  <  \#([x\mmember{}b|P[x]])))

Date html generated: 2017_10_01-AM-08_47_09
Last ObjectModification: 2017_07_26-PM-04_31_46

Theory : bags

Home Index