### Nuprl Lemma : imax-bag-lb

`∀[bs:bag(ℤ)]. (0 < #(bs) `` imax-bag(bs) ↓∈ bs)`

Proof

Definitions occuring in Statement :  bag-member: `x ↓∈ bs` imax-bag: `imax-bag(bs)` bag-size: `#(bs)` bag: `bag(T)` less_than: `a < b` uall: `∀[x:A]. B[x]` implies: `P `` Q` natural_number: `\$n` int: `ℤ`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` implies: `P `` Q` squash: `↓T` subtype_rel: `A ⊆r B` prop: `ℙ` so_lambda: `λ2x.t[x]` uimplies: `b supposing a` so_apply: `x[s]` all: `∀x:A. B[x]` sq_stable: `SqStable(P)` bag-member: `x ↓∈ bs` exists: `∃x:A. B[x]` imax-bag: `imax-bag(bs)` bag-size: `#(bs)` and: `P ∧ Q` cand: `A c∧ B` nat: `ℕ`
Lemmas referenced :  bag_to_squash_list sq_stable__all less_than_wf bag-size_wf bag-member_wf imax-bag_wf sq_stable__bag-member squash_wf imax-list-member equal-wf-base bag_wf list_subtype_base int_subtype_base l_member_wf imax-list_wf length_wf nat_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut lambdaFormation thin extract_by_obid sqequalHypSubstitution isectElimination intEquality hypothesisEquality imageElimination natural_numberEquality hypothesis applyEquality because_Cache sqequalRule lambdaEquality independent_isectElimination independent_functionElimination dependent_functionElimination imageMemberEquality baseClosed productElimination promote_hyp rename dependent_pairFormation independent_pairFormation productEquality hyp_replacement equalitySymmetry Error :applyLambdaEquality,  functionEquality setElimination

Latex:
\mforall{}[bs:bag(\mBbbZ{})].  (0  <  \#(bs)  {}\mRightarrow{}  imax-bag(bs)  \mdownarrow{}\mmember{}  bs)

Date html generated: 2016_10_25-AM-10_32_15
Last ObjectModification: 2016_07_12-AM-06_47_50

Theory : bags

Home Index