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