---

Step * 2 2 of Lemma filter_is_singleton2


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

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

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

---

Latex:

---

Latex:

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


By

---

Latex:
CaseNat  0  `i'

---

Home Index