---

Step * 2 1 of Lemma filter_is_singleton2


1. [T] : Type
2. P : T ⟶ 𝔹
3. u : T
4. v : T List
5. ¬↑(P u)
6. ||filter(P;v)|| = 1 ∈ ℤ
7. i : ℕ||v||
8. ↑(P v[i])
9. ∀j:ℕ||v||. i = j ∈ ℤ supposing ↑(P v[j])
⊢ ∃i:ℕ||v|| + 1. ((↑(P [u / v][i])) ∧ (∀j:ℕ||v|| + 1. i = j ∈ ℤ supposing ↑(P [u / v][j])))
BY
{ (InstConcl [i + 1] THEN Auto') }

1
1. T : Type
2. P : T ⟶ 𝔹
3. u : T
4. v : T List
5. ¬↑(P u)
6. ||filter(P;v)|| = 1 ∈ ℤ
7. i : ℕ||v||
8. ↑(P v[i])
9. ∀j:ℕ||v||. i = j ∈ ℤ supposing ↑(P v[j])
10. ↑(P [u / v][i + 1])
11. j : ℕ||v|| + 1
12. ↑(P [u / v][j])
⊢ (i + 1) = j ∈ ℤ

---

Latex:

---

Latex:

1.  [T]  :  Type
2.  P  :  T  {}\mrightarrow{}  \mBbbB{}
3.  u  :  T
4.  v  :  T  List
5.  \mneg{}\muparrow{}(P  u)
6.  ||filter(P;v)||  =  1
7.  i  :  \mBbbN{}||v||
8.  \muparrow{}(P  v[i])
9.  \mforall{}j:\mBbbN{}||v||.  i  =  j  supposing  \muparrow{}(P  v[j])
\mvdash{}  \mexists{}i:\mBbbN{}||v||  +  1.  ((\muparrow{}(P  [u  /  v][i]))  \mwedge{}  (\mforall{}j:\mBbbN{}||v||  +  1.  i  =  j  supposing  \muparrow{}(P  [u  /  v][j])))


By

---

Latex:
(InstConcl  [i  +  1]  THEN  Auto')

---

Home Index