---

Step * 1 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) = 1 ∈ ℤ
⊢ ∃i:ℕ||v|| + 1. ((↑(P [u / v][i])) ∧ (∀j:ℕ||v|| + 1. i = j ∈ ℤ supposing ↑(P [u / v][j])))
BY
{ (AssertBY ↑null(filter(P;v)) (NullByLength THEN Auto)
   THEN (RWO "filter_is_empty" (-1) THENA Auto)
   THEN InstConcl [0]
   THEN Reduce 0
   THEN Auto
   THEN Auto') }

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

---

Latex:

---

Latex:

1.  [T]  :  Type
2.  P  :  T  {}\mrightarrow{}  \mBbbB{}
3.  u  :  T
4.  v  :  T  List
5.  \muparrow{}(P  u)
6.  (||filter(P;v)||  +  1)  =  1
\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:
(AssertBY  \muparrow{}null(filter(P;v))  (NullByLength  THEN  Auto)
  THEN  (RWO  "filter\_is\_empty"  (-1)  THENA  Auto)
  THEN  InstConcl  [0]
  THEN  Reduce  0
  THEN  Auto
  THEN  Auto')

---

Home Index