---

Step * of Lemma non-empty-bag-mapfilter-union-of-list

∀[T:Type]
  ∀P:T ⟶ 𝔹. ∀f:T ⟶ Top. ∀L:bag(T) List.  (0 < #(bag-mapfilter(f;λx.P[x];bag-union(L))) ⇐⇒ (∃b∈L. 0 < #([x∈b|P[x]])))
BY
{ ((UnivCD THENA Auto)
   THEN RW (AddrC [1] (UnfoldsC ``bag-size bag-mapfilter bag-union``)) 0
   THEN RW (AddrC [1] (UnfoldsC ``bag-map bag-filter``)) 0
   THEN (InstLemma `length-map` [⌜f⌝;⌜Top⌝]⋅ THENA Auto)
   THEN (RWO "-1" 0 THENA (Folds ``bag-filter bag-union`` 0 THEN Auto)⋅)
   THEN Thin (-1)) }

1
1. [T] : Type
2. P : T ⟶ 𝔹
3. f : T ⟶ Top
4. L : bag(T) List
⊢ 0 < ||filter(λx.((λx.P[x]) x);concat(L))|| ⇐⇒ (∃b∈L. 0 < #([x∈b|P[x]]))

---

Latex:

---

Latex:
\mforall{}[T:Type]
    \mforall{}P:T  {}\mrightarrow{}  \mBbbB{}.  \mforall{}f:T  {}\mrightarrow{}  Top.  \mforall{}L:bag(T)  List.
        (0  <  \#(bag-mapfilter(f;\mlambda{}x.P[x];bag-union(L)))  \mLeftarrow{}{}\mRightarrow{}  (\mexists{}b\mmember{}L.  0  <  \#([x\mmember{}b|P[x]])))


By

---

Latex:
((UnivCD  THENA  Auto)
  THEN  RW  (AddrC  [1]  (UnfoldsC  ``bag-size  bag-mapfilter  bag-union``))  0
  THEN  RW  (AddrC  [1]  (UnfoldsC  ``bag-map  bag-filter``))  0
  THEN  (InstLemma  `length-map`  [\mkleeneopen{}f\mkleeneclose{};\mkleeneopen{}Top\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (RWO  "-1"  0  THENA  (Folds  ``bag-filter  bag-union``  0  THEN  Auto)\mcdot{})
  THEN  Thin  (-1))

---

Home Index