Nuprl Lemma : bag-combine-combine

`∀[A,B,C:Type]. ∀[b:bag(A)]. ∀[f:A ⟶ bag(B)]. ∀[g:B ⟶ bag(C)].  (⋃x∈⋃y∈b.f[y].g[x] = ⋃x∈b.⋃y∈f[x].g[y] ∈ bag(C))`

Proof

Definitions occuring in Statement :  bag-combine: `⋃x∈bs.f[x]` bag: `bag(T)` uall: `∀[x:A]. B[x]` so_apply: `x[s]` function: `x:A ⟶ B[x]` universe: `Type` equal: `s = t ∈ T`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` so_lambda: `λ2x.t[x]` top: `Top` so_apply: `x[s]` subtype_rel: `A ⊆r B` uimplies: `b supposing a`
Lemmas referenced :  bag-combine-assoc subtype_rel_bag top_wf trivial-equal bag_wf bag-combine_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut equalitySymmetry sqequalRule lemma_by_obid sqequalHypSubstitution isectElimination thin isect_memberEquality voidElimination voidEquality hypothesisEquality applyEquality hypothesis independent_isectElimination lambdaEquality because_Cache functionEquality axiomEquality

Latex:
\mforall{}[A,B,C:Type].  \mforall{}[b:bag(A)].  \mforall{}[f:A  {}\mrightarrow{}  bag(B)].  \mforall{}[g:B  {}\mrightarrow{}  bag(C)].
(\mcup{}x\mmember{}\mcup{}y\mmember{}b.f[y].g[x]  =  \mcup{}x\mmember{}b.\mcup{}y\mmember{}f[x].g[y])

Date html generated: 2016_05_15-PM-02_29_08
Last ObjectModification: 2015_12_27-AM-09_49_51

Theory : bags

Home Index