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: supposing a uall: [x:A]. B[x] so_apply: x[s] all: x:A. B[x] implies:  Q function: x:A ⟶ B[x] universe: Type equal: 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 ⊆B uimplies: supposing a guard: {T} iff: ⇐⇒ Q and: P ∧ Q rev_implies:  Q implies:  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