---

Step * of Lemma bag-member-mapfilter

∀[T,U:Type]. ∀[P:T ⟶ 𝔹]. ∀[x:U]. ∀[bs:bag(T)]. ∀[f:{x:T| ↑(P x)}  ⟶ U].
  uiff(x ↓∈ bag-mapfilter(f;P;bs);↓∃v:{x:T| ↑(P x)} . (v ↓∈ bs ∧ (x = (f v) ∈ U)))
BY
{ ((UnivCD THENA Auto)
   THEN UseWitness ⌜<Ax, Ax>⌝⋅
   THEN BagD (-2)
   THEN ThinVar `bs'
   THEN Auto
   THEN All (RepUR ``bag-mapfilter bag-map bag-filter``)
   THEN All (Fold `mapfilter`)
   THEN D -1
   THEN ExRepD) }

1
1. T : Type
2. U : Type
3. P : T ⟶ 𝔹
4. x : U
5. f : {x:T| ↑(P x)}  ⟶ U
6. as : T List
7. L : U List
8. L = mapfilter(f;λx.(P x);as) ∈ bag(U)
9. (x ∈ L)
⊢ Ax ∈ ↓∃v@0:{x:T| ↑(P x)} . (v@0 ↓∈ as ∧ (x = (f v@0) ∈ U))

2
1. T : Type
2. U : Type
3. P : T ⟶ 𝔹
4. x : U
5. f : {x:T| ↑(P x)}  ⟶ U
6. as : T List
7. v@0 : {x:T| ↑(P x)} 
8. v@0 ↓∈ as
9. x = (f v@0) ∈ U
⊢ Ax ∈ x ↓∈ mapfilter(f;λx.(P x);as)

---

Latex:

---

Latex:
\mforall{}[T,U:Type].  \mforall{}[P:T  {}\mrightarrow{}  \mBbbB{}].  \mforall{}[x:U].  \mforall{}[bs:bag(T)].  \mforall{}[f:\{x:T|  \muparrow{}(P  x)\}    {}\mrightarrow{}  U].
    uiff(x  \mdownarrow{}\mmember{}  bag-mapfilter(f;P;bs);\mdownarrow{}\mexists{}v:\{x:T|  \muparrow{}(P  x)\}  .  (v  \mdownarrow{}\mmember{}  bs  \mwedge{}  (x  =  (f  v))))


By

---

Latex:
((UnivCD  THENA  Auto)
  THEN  UseWitness  \mkleeneopen{}<Ax,  Ax>\mkleeneclose{}\mcdot{}
  THEN  BagD  (-2)
  THEN  ThinVar  `bs'
  THEN  Auto
  THEN  All  (RepUR  ``bag-mapfilter  bag-map  bag-filter``)
  THEN  All  (Fold  `mapfilter`)
  THEN  D  -1
  THEN  ExRepD)

---

Home Index