---

Step * of Lemma bag-combine-filter

∀[A,B:Type]. ∀[p:A ⟶ 𝔹]. ∀[f:{a:A| ↑p[a]}  ⟶ bag(B)]. ∀[ba:bag(A)].
  (⋃a∈[a∈ba|p[a]].f[a] = ⋃a∈ba.if p[a] then f[a] else {} fi  ∈ bag(B))
BY
{ (Auto THEN RepUR ``bag-bind`` 0 THEN BagD (-1) THEN Auto) }

1
1. A : Type
2. B : Type
3. p : A ⟶ 𝔹
4. f : {a:A| ↑p[a]}  ⟶ bag(B)
5. as : A List
6. bs : A List
7. permutation(A;as;bs)
⊢ ⋃a∈[a∈as|p[a]].f[a] = ⋃a∈bs.if p[a] then f[a] else {} fi  ∈ bag(B)

---

Latex:

---

Latex:
\mforall{}[A,B:Type].  \mforall{}[p:A  {}\mrightarrow{}  \mBbbB{}].  \mforall{}[f:\{a:A|  \muparrow{}p[a]\}    {}\mrightarrow{}  bag(B)].  \mforall{}[ba:bag(A)].
    (\mcup{}a\mmember{}[a\mmember{}ba|p[a]].f[a]  =  \mcup{}a\mmember{}ba.if  p[a]  then  f[a]  else  \{\}  fi  )


By

---

Latex:
(Auto  THEN  RepUR  ``bag-bind``  0  THEN  BagD  (-1)  THEN  Auto)

---

Home Index