### Nuprl Lemma : bag-combine-eq-out

`∀[A,B,C:Type]. ∀[as:bag(A)]. ∀[bs:bag(B)]. ∀[f:A ⟶ bag(C)]. ∀[g:B ⟶ bag(C)]. ∀[h:A ⟶ B].`
`  (⋃a∈as.f[a] = ⋃b∈bs.g[b] ∈ bag(C)) supposing `
`     ((∀a:A. (a ↓∈ as `` (g[h[a]] = f[a] ∈ bag(C)))) and `
`     (bs = bag-map(h;as) ∈ bag(B)))`

Proof

Definitions occuring in Statement :  bag-member: `x ↓∈ bs` bag-combine: `⋃x∈bs.f[x]` bag-map: `bag-map(f;bs)` bag: `bag(T)` uimplies: `b supposing a` uall: `∀[x:A]. B[x]` so_apply: `x[s]` all: `∀x:A. B[x]` implies: `P `` Q` function: `x:A ⟶ B[x]` universe: `Type` equal: `s = t ∈ T`
Definitions unfolded in proof :  member: `t ∈ T` squash: `↓T` uall: `∀[x:A]. B[x]` prop: `ℙ` so_lambda: `λ2x.t[x]` so_apply: `x[s]` true: `True` subtype_rel: `A ⊆r B` uimplies: `b supposing a` guard: `{T}` iff: `P `⇐⇒` Q` and: `P ∧ Q` rev_implies: `P `` Q` implies: `P `` Q` all: `∀x:A. B[x]` sq_stable: `SqStable(P)`
Lemmas referenced :  equal_wf squash_wf true_wf bag_wf bag-combine_wf bag-combine-map iff_weakening_equal set_wf bag-member_wf bag-subtype sq_stable__bag-member all_wf bag-map_wf
Rules used in proof :  cut hypothesis thin applyEquality sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaEquality sqequalHypSubstitution imageElimination introduction extract_by_obid isectElimination hypothesisEquality equalityTransitivity equalitySymmetry because_Cache cumulativity sqequalRule functionExtensionality natural_numberEquality imageMemberEquality baseClosed universeEquality independent_isectElimination productElimination independent_functionElimination functionEquality dependent_functionElimination setElimination rename hyp_replacement applyLambdaEquality isect_memberFormation isect_memberEquality axiomEquality

Latex:
\mforall{}[A,B,C:Type].  \mforall{}[as:bag(A)].  \mforall{}[bs:bag(B)].  \mforall{}[f:A  {}\mrightarrow{}  bag(C)].  \mforall{}[g:B  {}\mrightarrow{}  bag(C)].  \mforall{}[h:A  {}\mrightarrow{}  B].
(\mcup{}a\mmember{}as.f[a]  =  \mcup{}b\mmember{}bs.g[b])  supposing
((\mforall{}a:A.  (a  \mdownarrow{}\mmember{}  as  {}\mRightarrow{}  (g[h[a]]  =  f[a])))  and
(bs  =  bag-map(h;as)))

Date html generated: 2017_10_01-AM-08_57_13
Last ObjectModification: 2017_07_26-PM-04_39_21

Theory : bags

Home Index