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

`∀[T:Type]. ∀L:bag(T) List. (0 < #(bag-union(L)) `⇐⇒` (∃b∈L. 0 < #(b)))`

Proof

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

Latex:
\mforall{}[T:Type].  \mforall{}L:bag(T)  List.  (0  <  \#(bag-union(L))  \mLeftarrow{}{}\mRightarrow{}  (\mexists{}b\mmember{}L.  0  <  \#(b)))

Date html generated: 2017_10_01-AM-08_47_04
Last ObjectModification: 2017_07_26-PM-04_31_44

Theory : bags

Home Index