---

Step * 1 of Lemma filter_is_singleton2

.....truecase..... 
1. [T] : Type
2. P : T ⟶ 𝔹
3. u : T
4. v : T List
5. ||filter(P;v)|| = 1 ∈ ℤ ⇐⇒ ∃i:ℕ||v||. ((↑(P v[i])) ∧ (∀j:ℕ||v||. i = j ∈ ℤ supposing ↑(P v[j])))
6. ↑(P u)
⊢ ||[u / filter(P;v)]|| = 1 ∈ ℤ
⇐⇒ ∃i:ℕ||v|| + 1. ((↑(P [u / v][i])) ∧ (∀j:ℕ||v|| + 1. i = j ∈ ℤ supposing ↑(P [u / v][j])))
BY
{ (((Thin (-2) THEN Reduce 0) THEN Auto') THEN ExRepD) }

1
1. [T] : Type
2. P : T ⟶ 𝔹
3. u : T
4. v : T List
5. ↑(P u)
6. (||filter(P;v)|| + 1) = 1 ∈ ℤ
⊢ ∃i:ℕ||v|| + 1. ((↑(P [u / v][i])) ∧ (∀j:ℕ||v|| + 1. i = j ∈ ℤ supposing ↑(P [u / 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])
⊢ (||filter(P;v)|| + 1) = 1 ∈ ℤ

---

Latex:

---

Latex:
.....truecase..... 
1.  [T]  :  Type
2.  P  :  T  {}\mrightarrow{}  \mBbbB{}
3.  u  :  T
4.  v  :  T  List
5.  ||filter(P;v)||  =  1  \mLeftarrow{}{}\mRightarrow{}  \mexists{}i:\mBbbN{}||v||.  ((\muparrow{}(P  v[i]))  \mwedge{}  (\mforall{}j:\mBbbN{}||v||.  i  =  j  supposing  \muparrow{}(P  v[j])))
6.  \muparrow{}(P  u)
\mvdash{}  ||[u  /  filter(P;v)]||  =  1
\mLeftarrow{}{}\mRightarrow{}  \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:
(((Thin  (-2)  THEN  Reduce  0)  THEN  Auto')  THEN  ExRepD)

---

Home Index