---

Step * 2 2 1 of Lemma equipollent-filter


1. A : Type
2. P : A ⟶ 𝔹
3. ys : A List
4. y : A
5. {x:ℕ||ys||| ↑P[ys[x]]}  ~ ℕ||filter(P;ys)||
6. ¬↑(P y)
⊢ {x:ℕ1 + ||ys||| ↑P[ys @ [y][x]]}  ≡ {x:ℕ||ys||| ↑P[ys[x]]} 
BY
{ (RepeatFor 2 (D 0) THEN Auto THEN DSetVars⋅) }

1
1. A : Type
2. P : A ⟶ 𝔹
3. ys : A List
4. y : A
5. {x:ℕ||ys||| ↑P[ys[x]]}  ~ ℕ||filter(P;ys)||
6. ¬↑(P y)
7. x : ℕ1 + ||ys||
8. ↑P[ys @ [y][x]]
⊢ x ∈ {x:ℕ||ys||| ↑P[ys[x]]} 

---

Latex:

---

Latex:

1.  A  :  Type
2.  P  :  A  {}\mrightarrow{}  \mBbbB{}
3.  ys  :  A  List
4.  y  :  A
5.  \{x:\mBbbN{}||ys|||  \muparrow{}P[ys[x]]\}    \msim{}  \mBbbN{}||filter(P;ys)||
6.  \mneg{}\muparrow{}(P  y)
\mvdash{}  \{x:\mBbbN{}1  +  ||ys|||  \muparrow{}P[ys  @  [y][x]]\}    \mequiv{}  \{x:\mBbbN{}||ys|||  \muparrow{}P[ys[x]]\} 


By

---

Latex:
(RepeatFor  2  (D  0)  THEN  Auto  THEN  DSetVars\mcdot{})

---

Home Index