Nuprl Lemma : bag-member-product
∀[A,B:Type]. ∀[as:bag(A)]. ∀[bs:bag(B)]. ∀[p:A × B]. uiff(p ↓∈ as × bs;fst(p) ↓∈ as ∧ snd(p) ↓∈ bs)
Proof
Definitions occuring in Statement :
bag-member: x ↓∈ bs,
bag-product: bs × cs,
bag: bag(T),
uiff: uiff(P;Q),
uall: ∀[x:A]. B[x],
pi1: fst(t),
pi2: snd(t),
and: P ∧ Q,
product: x:A × B[x],
universe: Type
Definitions unfolded in proof :
member: t ∈ T,
uall: ∀[x:A]. B[x],
prop: ℙ,
and: P ∧ Q,
so_lambda: λ2x.t[x],
so_apply: x[s],
empty-bag: {},
top: Top,
uiff: uiff(P;Q),
uimplies: b supposing a,
false: False,
bag-member: x ↓∈ bs,
squash: ↓T,
single-bag: {x},
bag-append: as + bs,
append: as @ bs,
all: ∀x:A. B[x],
so_lambda: so_lambda(x,y,z.t[x; y; z]),
so_apply: x[s1;s2;s3],
subtype_rel: A ⊆r B,
pi1: fst(t),
pi2: snd(t),
implies: P ⇒ Q,
sq_stable: SqStable(P),
exists: ∃x:A. B[x],
iff: P ⇐⇒ Q,
rev_implies: P ⇐ Q,
sq_or: a ↓∨ b,
or: P ∨ Q,
guard: {T},
cand: A c∧ B
Lemmas referenced :
bag-member_wf,
bag-product_wf,
pi1_wf,
pi2_wf,
squash_wf,
bag-product-empty,
bag-member-empty-iff,
empty-bag_wf,
list_ind_cons_lemma,
list_ind_nil_lemma,
single-bag_wf,
bag-subtype-list,
subtype_rel_list,
top_wf,
bag-append_wf,
bag-map_wf,
list-subtype-bag,
uiff_wf,
bag_wf,
bag_to_squash_list,
sq_stable__uiff,
sq_stable__bag-member,
sq_stable__and,
list_induction,
list_wf,
bag-product-append,
bag-product-single,
bag-member-append,
bag-member-map,
bag-member-single,
and_wf,
equal_wf
Rules used in proof :
comment,
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
hypothesisEquality,
cut,
introduction,
extract_by_obid,
sqequalHypSubstitution,
isectElimination,
thin,
productEquality,
cumulativity,
productElimination,
independent_pairEquality,
hypothesis,
sqequalRule,
lambdaEquality,
because_Cache,
isect_memberEquality,
voidElimination,
voidEquality,
independent_pairFormation,
isect_memberFormation,
independent_isectElimination,
imageElimination,
imageMemberEquality,
baseClosed,
dependent_functionElimination,
applyEquality,
universeEquality,
equalityTransitivity,
equalitySymmetry,
independent_functionElimination,
lambdaFormation,
promote_hyp,
rename,
hyp_replacement,
applyLambdaEquality,
unionElimination,
inlFormation,
dependent_set_memberEquality,
setElimination,
inrFormation,
dependent_pairFormation
Latex:
\mforall{}[A,B:Type]. \mforall{}[as:bag(A)]. \mforall{}[bs:bag(B)]. \mforall{}[p:A \mtimes{} B]. uiff(p \mdownarrow{}\mmember{} as \mtimes{} bs;fst(p) \mdownarrow{}\mmember{} as \mwedge{} snd(p) \mdownarrow{}\mmember{} bs)
Date html generated:
2017_10_01-AM-08_54_39
Last ObjectModification:
2017_07_26-PM-04_36_25
Theory : bags
Home
Index