---

Step * 2 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)
⊢ {x:ℕ||ys|| + 1| ↑P[ys @ [y][x]]}  ~ ℕ||filter(P;ys)|| + 0
BY
{ ((RW IntNormC 0 THENM RWO "-2<" 0 THENM BLemma `equipollent_weakening_ext-eq`) 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)
⊢ {x:ℕ1 + ||ys||| ↑P[ys @ [y][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{}||ys||  +  1|  \muparrow{}P[ys  @  [y][x]]\}    \msim{}  \mBbbN{}||filter(P;ys)||  +  0


By

---

Latex:
((RW  IntNormC  0  THENM  RWO  "-2<"  0  THENM  BLemma  `equipollent\_weakening\_ext-eq`)  THENA  Auto)

---

Home Index