---

Step * 2 of Lemma filter_is_singleton


1. T : Type
2. P : T ⟶ 𝔹
3. u : T
4. v : T List
5. ∀[x:T]. (filter(P;v) = [x] ∈ (T List)) supposing ((∀y∈v.(↑P[y]) ⇒ (y = x ∈ T)) and (↑P[x]) and (x ∈! v))
6. x : T
7. (x ∈! [u / v])
8. ↑P[x]
9. (∀y∈[u / v].(↑P[y]) ⇒ (y = x ∈ T))
⊢ filter(P;[u / v]) = [x] ∈ (T List)
BY
{ (((RWO "cons_member!" (-3)) THENA Auto) THEN ((RWO "l_all_cons" (-1)) THENA Auto)) }

1
1. T : Type
2. P : T ⟶ 𝔹
3. u : T
4. v : T List
5. ∀[x:T]. (filter(P;v) = [x] ∈ (T List)) supposing ((∀y∈v.(↑P[y]) ⇒ (y = x ∈ T)) and (↑P[x]) and (x ∈! v))
6. x : T
7. ((x = u ∈ T) ∧ (¬(x ∈ v))) ∨ ((x ∈! v) ∧ (¬(x = u ∈ T)))
8. ↑P[x]
9. ((↑P[u]) ⇒ (u = x ∈ T)) ∧ (∀y∈v.(↑P[y]) ⇒ (y = x ∈ T))
⊢ filter(P;[u / v]) = [x] ∈ (T List)

---

Latex:

---

Latex:

1.  T  :  Type
2.  P  :  T  {}\mrightarrow{}  \mBbbB{}
3.  u  :  T
4.  v  :  T  List
5.  \mforall{}[x:T].  (filter(P;v)  =  [x])  supposing  ((\mforall{}y\mmember{}v.(\muparrow{}P[y])  {}\mRightarrow{}  (y  =  x))  and  (\muparrow{}P[x])  and  (x  \mmember{}!  v))
6.  x  :  T
7.  (x  \mmember{}!  [u  /  v])
8.  \muparrow{}P[x]
9.  (\mforall{}y\mmember{}[u  /  v].(\muparrow{}P[y])  {}\mRightarrow{}  (y  =  x))
\mvdash{}  filter(P;[u  /  v])  =  [x]


By

---

Latex:
(((RWO  "cons\_member!"  (-3))  THENA  Auto)  THEN  ((RWO  "l\_all\_cons"  (-1))  THENA  Auto))

---

Home Index