---

Step * 2 1 1 of Lemma equipollent-filter

.....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
BY
{ (BLemma `equipollent-add`  THEN Auto) }

---

Latex:

---

Latex:
.....assertion..... 
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{}  \mBbbN{}||filter(P;ys)||  +  \mBbbN{}1  \msim{}  \mBbbN{}||filter(P;ys)||  +  1


By

---

Latex:
(BLemma  `equipollent-add`    THEN  Auto)

---

Home Index