---

Step * 2 1 2 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)
7. ℕ||filter(P;ys)|| + ℕ1 ~ ℕ||filter(P;ys)|| + 1
⊢ {x:ℕ||ys|| + 1| ↑P[ys @ [y][x]]}  ~ ℕ||filter(P;ys)|| + 1
BY
{ (RWO "-1<" 0 THENA Auto) }

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


By

---

Latex:
(RWO  "-1<"  0  THENA  Auto)

---

Home Index