### Nuprl Lemma : bag-from-member-function-exists

`∀[T,A:Type].`
`  ∀bs:bag(T). ∀P:T ⟶ A ⟶ ℙ.`
`    ((∀x,y:A.  Dec(x = y ∈ A))`
`    `` (∀x,y:T.  Dec(x = y ∈ T))`
`    `` (∀i:T. (i ↓∈ bs `` (∃a:A. P[i;a])))`
`    `` (∃b:bag(T × A). ((∀i:T. (i ↓∈ bs `` i ↓∈ bag-map(λx.(fst(x));b))) ∧ (∀x:T × A. (x ↓∈ b `` P[fst(x);snd(x)])))))`

Proof

Definitions occuring in Statement :  bag-member: `x ↓∈ bs` bag-map: `bag-map(f;bs)` bag: `bag(T)` decidable: `Dec(P)` uall: `∀[x:A]. B[x]` prop: `ℙ` so_apply: `x[s1;s2]` pi1: `fst(t)` pi2: `snd(t)` all: `∀x:A. B[x]` exists: `∃x:A. B[x]` implies: `P `` Q` and: `P ∧ Q` lambda: `λx.A[x]` function: `x:A ⟶ B[x]` product: `x:A × B[x]` universe: `Type` equal: `s = t ∈ T`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` all: `∀x:A. B[x]` implies: `P `` Q` exists: `∃x:A. B[x]` member: `t ∈ T` prop: `ℙ` so_lambda: `λ2x.t[x]` so_apply: `x[s1;s2]` subtype_rel: `A ⊆r B` so_apply: `x[s]` uimplies: `b supposing a` and: `P ∧ Q` uiff: `uiff(P;Q)` rev_uimplies: `rev_uimplies(P;Q)` bag-member: `x ↓∈ bs` squash: `↓T` pi1: `fst(t)` inject: `Inj(A;B;f)` sq_stable: `SqStable(P)` respects-equality: `respects-equality(S;T)` true: `True` guard: `{T}` iff: `P `⇐⇒` Q` rev_implies: `P `` Q` pi2: `snd(t)`
Lemmas referenced :  bag-map-member-wf bag-member_wf pi1_wf bag-member-evidence subtype_rel_self bag-map_wf pi2_wf decidable_wf equal_wf bag_wf istype-universe bag-member-map2 bag-member-map3-deq sq_stable__bag-member respects-equality-product respects-equality-set-trivial2 respects-equality-trivial istype-base decidable__equal_product squash_wf true_wf iff_weakening_equal
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation_alt lambdaFormation_alt rename dependent_pairFormation_alt cut introduction extract_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality productEquality lambdaEquality_alt hypothesis universeIsType setElimination independent_pairEquality because_Cache sqequalRule applyEquality independent_isectElimination setIsType productIsType functionIsType inhabitedIsType instantiate universeEquality independent_pairFormation dependent_functionElimination setEquality productElimination imageElimination imageMemberEquality baseClosed dependent_set_memberEquality_alt equalityIsType1 independent_functionElimination equalitySymmetry equalityTransitivity equalityIstype applyLambdaEquality sqequalBase functionEquality cumulativity natural_numberEquality

Latex:
\mforall{}[T,A:Type].
\mforall{}bs:bag(T).  \mforall{}P:T  {}\mrightarrow{}  A  {}\mrightarrow{}  \mBbbP{}.
((\mforall{}x,y:A.    Dec(x  =  y))
{}\mRightarrow{}  (\mforall{}x,y:T.    Dec(x  =  y))
{}\mRightarrow{}  (\mforall{}i:T.  (i  \mdownarrow{}\mmember{}  bs  {}\mRightarrow{}  (\mexists{}a:A.  P[i;a])))
{}\mRightarrow{}  (\mexists{}b:bag(T  \mtimes{}  A)
((\mforall{}i:T.  (i  \mdownarrow{}\mmember{}  bs  {}\mRightarrow{}  i  \mdownarrow{}\mmember{}  bag-map(\mlambda{}x.(fst(x));b)))
\mwedge{}  (\mforall{}x:T  \mtimes{}  A.  (x  \mdownarrow{}\mmember{}  b  {}\mRightarrow{}  P[fst(x);snd(x)])))))

Date html generated: 2019_10_15-AM-11_04_05
Last ObjectModification: 2019_06_25-PM-01_21_12

Theory : bags

Home Index