---

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


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]]))
BY
{ (ListInd'(-1) THENA ((Fold `bag-size` 0 THEN Fold `bag-union` 0 THEN Fold `bag-filter` 0) THEN Auto)) }

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

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

---

Latex:

---

Latex:

1.  [T]  :  Type
2.  P  :  T  {}\mrightarrow{}  \mBbbB{}
3.  f  :  T  {}\mrightarrow{}  Top
4.  L  :  bag(T)  List
\mvdash{}  0  <  ||filter(\mlambda{}x.((\mlambda{}x.P[x])  x);concat(L))||  \mLeftarrow{}{}\mRightarrow{}  (\mexists{}b\mmember{}L.  0  <  \#([x\mmember{}b|P[x]]))


By

---

Latex:
(ListInd'(-1)
  THENA  ((Fold  `bag-size`  0  THEN  Fold  `bag-union`  0  THEN  Fold  `bag-filter`  0)  THEN  Auto)
  )

---

Home Index