---

Step * of Lemma member-fset-mapfilter

∀[T:Type]. ∀[eqT:EqDecider(T)]. ∀[P:T ⟶ 𝔹]. ∀[X:Type]. ∀[eqX:EqDecider(X)]. ∀[f:{x:T| ↑(P x)}  ⟶ X]. ∀[s:fset(T)].
∀[x:X].
  uiff(x ∈ fset-mapfilter(f;P;s);↓∃y:T. (y ∈ s ∧ (↑(P y)) ∧ (x = (f y) ∈ X)))
BY
{ Auto }

1
1. T : Type
2. eqT : EqDecider(T)
3. P : T ⟶ 𝔹
4. X : Type
5. eqX : EqDecider(X)
6. f : {x:T| ↑(P x)}  ⟶ X
7. s : fset(T)
8. x : X
9. x ∈ fset-mapfilter(f;P;s)
⊢ ↓∃y:T. (y ∈ s ∧ (↑(P y)) ∧ (x = (f y) ∈ X))

2
1. T : Type
2. eqT : EqDecider(T)
3. P : T ⟶ 𝔹
4. X : Type
5. eqX : EqDecider(X)
6. f : {x:T| ↑(P x)}  ⟶ X
7. s : fset(T)
8. x : X
9. ↓∃y:T. (y ∈ s ∧ (↑(P y)) ∧ (x = (f y) ∈ X))
⊢ x ∈ fset-mapfilter(f;P;s)

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[eqT:EqDecider(T)].  \mforall{}[P:T  {}\mrightarrow{}  \mBbbB{}].  \mforall{}[X:Type].  \mforall{}[eqX:EqDecider(X)].
\mforall{}[f:\{x:T|  \muparrow{}(P  x)\}    {}\mrightarrow{}  X].  \mforall{}[s:fset(T)].  \mforall{}[x:X].
    uiff(x  \mmember{}  fset-mapfilter(f;P;s);\mdownarrow{}\mexists{}y:T.  (y  \mmember{}  s  \mwedge{}  (\muparrow{}(P  y))  \mwedge{}  (x  =  (f  y))))


By

---

Latex:
Auto

---

Home Index