---

Step * of Lemma filter-union

∀[T:Type]. ∀eq:EqDecider(T). ∀as,bs:T List. ∀P:T ⟶ 𝔹.  (filter(P;as ⋃ bs) = filter(P;as) ⋃ filter(P;bs) ∈ (T List))
BY
{ ((UnivCD THENA Auto) THEN Unfold `l-union` 0 THEN ListInd (-2) THEN Reduce 0 THEN Auto THEN AutoSplit) }

1
1. T : Type
2. eq : EqDecider(T)
3. as : T List
4. P : T ⟶ 𝔹
5. u : T
6. v : T List
7. filter(P;reduce(λa,L. insert(a;L);as;v)) = reduce(λa,L. insert(a;L);filter(P;as);filter(P;v)) ∈ (T List)
8. ↑(P u)
⊢ filter(P;insert(u;reduce(λa,L. insert(a;L);as;v))) = insert(u;reduce(λa,L. insert(a;L);filter(P;as);filter(P;v))) ∈ (T\000C List)

2
1. T : Type
2. eq : EqDecider(T)
3. as : T List
4. P : T ⟶ 𝔹
5. u : T
6. ¬↑(P u)
7. v : T List
8. filter(P;reduce(λa,L. insert(a;L);as;v)) = reduce(λa,L. insert(a;L);filter(P;as);filter(P;v)) ∈ (T List)
⊢ filter(P;insert(u;reduce(λa,L. insert(a;L);as;v))) = reduce(λa,L. insert(a;L);filter(P;as);filter(P;v)) ∈ (T List)

---

Latex:

---

Latex:
\mforall{}[T:Type]
    \mforall{}eq:EqDecider(T).  \mforall{}as,bs:T  List.  \mforall{}P:T  {}\mrightarrow{}  \mBbbB{}.    (filter(P;as  \mcup{}  bs)  =  filter(P;as)  \mcup{}  filter(P;bs))


By

---

Latex:
((UnivCD  THENA  Auto)
  THEN  Unfold  `l-union`  0
  THEN  ListInd  (-2)
  THEN  Reduce  0
  THEN  Auto
  THEN  AutoSplit)

---

Home Index