### Nuprl Lemma : bag-all_wf

`∀[T:Type]. ∀[p:T ⟶ 𝔹]. ∀[bs:bag(T)].  (bag-all(x.p[x];bs) ∈ 𝔹)`

Proof

Definitions occuring in Statement :  bag-all: `bag-all(x.p[x];bs)` bag: `bag(T)` bool: `𝔹` uall: `∀[x:A]. B[x]` so_apply: `x[s]` member: `t ∈ T` function: `x:A ⟶ B[x]` universe: `Type`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` bag-all: `bag-all(x.p[x];bs)` so_lambda: `λ2x y.t[x; y]` all: `∀x:A. B[x]` implies: `P `` Q` bool: `𝔹` unit: `Unit` it: `⋅` btrue: `tt` band: `p ∧b q` ifthenelse: `if b then t else f fi ` bfalse: `ff` prop: `ℙ` so_apply: `x[s1;s2]` uimplies: `b supposing a` comm: `Comm(T;op)` infix_ap: `x f y` squash: `↓T` true: `True` subtype_rel: `A ⊆r B` guard: `{T}` iff: `P `⇐⇒` Q` and: `P ∧ Q` rev_implies: `P `` Q` assoc: `Assoc(T;op)` top: `Top` uiff: `uiff(P;Q)` so_apply: `x[s]`
Lemmas referenced :  bag-reduce_wf bool_wf btrue_wf equal_wf squash_wf true_wf band_commutes iff_weakening_equal band_assoc eqtt_to_assert bag-map_wf bag_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut sqequalRule extract_by_obid sqequalHypSubstitution isectElimination thin hypothesis lambdaEquality hypothesisEquality lambdaFormation unionElimination equalityElimination equalityTransitivity equalitySymmetry dependent_functionElimination independent_functionElimination because_Cache independent_isectElimination applyEquality imageElimination natural_numberEquality imageMemberEquality baseClosed universeEquality productElimination isect_memberEquality axiomEquality voidElimination voidEquality cumulativity functionExtensionality functionEquality

Latex:
\mforall{}[T:Type].  \mforall{}[p:T  {}\mrightarrow{}  \mBbbB{}].  \mforall{}[bs:bag(T)].    (bag-all(x.p[x];bs)  \mmember{}  \mBbbB{})

Date html generated: 2017_10_01-AM-08_52_13
Last ObjectModification: 2017_07_26-PM-04_33_53

Theory : bags

Home Index