---

Step * 1 of Lemma bag-member-mapfilter


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))
BY
{ ((EqTypeHD (-2) THEN Auto) THEN FLemma `member-permutation` [-2] THEN Auto) }

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) ∈ pertype(λas,bs. ((as ∈ U List) ∧ (bs ∈ U List) ∧ permutation(U;as;bs)))
9. L ∈ U List
10. mapfilter(f;λx.(P x);as) ∈ U List
11. permutation(U;L;mapfilter(f;λx.(P x);as))
12. (x ∈ L)
13. ∀a:U. ((a ∈ L) ⇐⇒ (a ∈ mapfilter(f;λx.(P x);as)))
⊢ Ax ∈ ↓∃v@0:{x:T| ↑(P x)} . (v@0 ↓∈ as ∧ (x = (f v@0) ∈ U))

---

Latex:

---

Latex:

1.  T  :  Type
2.  U  :  Type
3.  P  :  T  {}\mrightarrow{}  \mBbbB{}
4.  x  :  U
5.  f  :  \{x:T|  \muparrow{}(P  x)\}    {}\mrightarrow{}  U
6.  as  :  T  List
7.  L  :  U  List
8.  L  =  mapfilter(f;\mlambda{}x.(P  x);as)
9.  (x  \mmember{}  L)
\mvdash{}  Ax  \mmember{}  \mdownarrow{}\mexists{}v@0:\{x:T|  \muparrow{}(P  x)\}  .  (v@0  \mdownarrow{}\mmember{}  as  \mwedge{}  (x  =  (f  v@0)))


By

---

Latex:
((EqTypeHD  (-2)  THEN  Auto)  THEN  FLemma  `member-permutation`  [-2]  THEN  Auto)

---

Home Index