---

Step * 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:ℕ||ys|| + 1| ↑P[ys @ [y][x]]}  ~ ℕ||filter(P;ys)|| + 1
BY
{ Assert ⌜ℕ||filter(P;ys)|| + ℕ1 ~ ℕ||filter(P;ys)|| + 1⌝⋅ }

1
.....assertion..... 
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)
⊢ ℕ||filter(P;ys)|| + ℕ1 ~ ℕ||filter(P;ys)|| + 1

2
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. ℕ||filter(P;ys)|| + ℕ1 ~ ℕ||filter(P;ys)|| + 1
⊢ {x:ℕ||ys|| + 1| ↑P[ys @ [y][x]]}  ~ ℕ||filter(P;ys)|| + 1

---

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.  \muparrow{}(P  y)
\mvdash{}  \{x:\mBbbN{}||ys||  +  1|  \muparrow{}P[ys  @  [y][x]]\}    \msim{}  \mBbbN{}||filter(P;ys)||  +  1


By

---

Latex:
Assert  \mkleeneopen{}\mBbbN{}||filter(P;ys)||  +  \mBbbN{}1  \msim{}  \mBbbN{}||filter(P;ys)||  +  1\mkleeneclose{}\mcdot{}

---

Home Index