### Nuprl Lemma : int-bag-product-positive

`∀[b:bag(ℤ)]. 0 < Π(b) supposing ∀[x:ℤ]. (x ↓∈ b `` 0 < x)`

Proof

Definitions occuring in Statement :  bag-member: `x ↓∈ bs` int-bag-product: `Π(b)` bag: `bag(T)` less_than: `a < b` uimplies: `b supposing a` uall: `∀[x:A]. B[x]` implies: `P `` Q` natural_number: `\$n` int: `ℤ`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` uimplies: `b supposing a` implies: `P `` Q` prop: `ℙ` squash: `↓T` exists: `∃x:A. B[x]` rev_implies: `P `` Q` all: `∀x:A. B[x]` iff: `P `⇐⇒` Q` and: `P ∧ Q` int-bag-product: `Π(b)` bag-product: `Πx ∈ b. f[x]` bag-summation: `Σ(x∈b). f[x]` bag-accum: `bag-accum(v,x.f[v; x];init;bs)` nat: `ℕ` false: `False` ge: `i ≥ j ` not: `¬A` satisfiable_int_formula: `satisfiable_int_formula(fmla)` top: `Top` nat_plus: `ℕ+` guard: `{T}` or: `P ∨ Q` so_lambda: `λ2x y.t[x; y]` so_apply: `x[s1;s2]` decidable: `Dec(P)` cons: `[a / b]` le: `A ≤ B` less_than': `less_than'(a;b)` colength: `colength(L)` nil: `[]` it: `⋅` so_lambda: `λ2x.t[x]` so_apply: `x[s]` sq_type: `SQType(T)` less_than: `a < b` subtype_rel: `A ⊆r B` l_member: `(x ∈ l)` select: `L[n]` cand: `A c∧ B` uiff: `uiff(P;Q)` true: `True`
Lemmas referenced :  istype-int bag-member_wf istype-less_than member-less_than int-bag-product_wf bag_wf bag_to_squash_list less_than_wf bag-member-list decidable__equal_int l_member_wf nat_properties full-omega-unsat intformand_wf intformle_wf itermConstant_wf itermVar_wf intformless_wf int_formula_prop_and_lemma istype-void int_formula_prop_le_lemma int_term_value_constant_lemma int_term_value_var_lemma int_formula_prop_less_lemma int_formula_prop_wf ge_wf nat_plus_properties intformeq_wf int_formula_prop_eq_lemma list-cases list_accum_nil_lemma decidable__lt intformnot_wf int_formula_prop_not_lemma nat_plus_wf nil_wf product_subtype_list colength-cons-not-zero istype-nat colength_wf_list istype-le list_wf list_accum_wf subtract-1-ge-0 subtype_base_sq set_subtype_base int_subtype_base spread_cons_lemma subtract_wf itermSubtract_wf itermAdd_wf int_term_value_subtract_lemma int_term_value_add_lemma decidable__le le_wf list_accum_cons_lemma cons_wf cons_member length_of_cons_lemma add_nat_plus length_wf_nat add-is-int-iff false_wf length_wf list_subtype_base mul_nat_plus
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation_alt introduction cut hypothesis sqequalRule isectIsType extract_by_obid functionIsType universeIsType sqequalHypSubstitution isectElimination thin intEquality hypothesisEquality natural_numberEquality isect_memberEquality_alt independent_isectElimination isectIsTypeImplies inhabitedIsType imageElimination productElimination promote_hyp equalitySymmetry hyp_replacement applyLambdaEquality isectEquality functionEquality rename lambdaFormation_alt independent_functionElimination dependent_functionElimination setElimination intWeakElimination approximateComputation dependent_pairFormation_alt lambdaEquality_alt int_eqEquality voidElimination independent_pairFormation equalityTransitivity functionIsTypeImplies unionElimination because_Cache hypothesis_subsumption equalityIstype dependent_set_memberEquality_alt multiplyEquality instantiate baseApply closedConclusion baseClosed applyEquality sqequalBase inrFormation_alt pointwiseFunctionality productIsType imageMemberEquality dependent_set_memberEquality

Latex:
\mforall{}[b:bag(\mBbbZ{})].  0  <  \mPi{}(b)  supposing  \mforall{}[x:\mBbbZ{}].  (x  \mdownarrow{}\mmember{}  b  {}\mRightarrow{}  0  <  x)

Date html generated: 2020_05_20-AM-08_01_51
Last ObjectModification: 2019_11_27-PM-03_08_09

Theory : bags

Home Index