---

Step * 2 1 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 ∈ 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)
BY
{ (Reduce 0 THEN AutoSplit) }

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))
10. ↑(P u)
⊢ [u / filter(P;v)] = [x] ∈ (T List)

2
1. T : Type
2. P : T ⟶ 𝔹
3. u : T
4. ¬↑(P u)
5. v : T List
6. ∀[x:T]. (filter(P;v) = [x] ∈ (T List)) supposing ((∀y∈v.(↑P[y]) ⇒ (y = x ∈ T)) and (↑P[x]) and (x ∈! v))
7. x : T
8. ((x = u ∈ T) ∧ (¬(x ∈ v))) ∨ ((x ∈! v) ∧ (¬(x = u ∈ T)))
9. ↑P[x]
10. ((↑P[u]) ⇒ (u = x ∈ T)) ∧ (∀y∈v.(↑P[y]) ⇒ (y = x ∈ T))
⊢ filter(P;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  =  u)  \mwedge{}  (\mneg{}(x  \mmember{}  v)))  \mvee{}  ((x  \mmember{}!  v)  \mwedge{}  (\mneg{}(x  =  u)))
8.  \muparrow{}P[x]
9.  ((\muparrow{}P[u])  {}\mRightarrow{}  (u  =  x))  \mwedge{}  (\mforall{}y\mmember{}v.(\muparrow{}P[y])  {}\mRightarrow{}  (y  =  x))
\mvdash{}  filter(P;[u  /  v])  =  [x]


By

---

Latex:
(Reduce  0  THEN  AutoSplit)

---

Home Index