---

Step * of Lemma filter_iseg2

∀[T:Type]. ∀L2,L1:T List. ∀P:{x:T| (x ∈ L2)}  ⟶ 𝔹.  (L1 ≤ L2 ⇒ filter(P;L1) ≤ filter(P;L2))
BY
{ (InductionOnList THEN Reduce 0 THEN (UnivCD THENA Auto)) }

1
1. [T] : Type
2. L1 : T List
3. P : {x:T| (x ∈ [])}  ⟶ 𝔹
4. L1 ≤ []
⊢ filter(P;L1) ≤ []

2
1. [T] : Type
2. u : T
3. v : T List
4. ∀L1:T List. ∀P:{x:T| (x ∈ v)}  ⟶ 𝔹.  (L1 ≤ v ⇒ filter(P;L1) ≤ filter(P;v))
5. L1 : T List
6. P : {x:T| (x ∈ [u / v])}  ⟶ 𝔹
7. L1 ≤ [u / v]
⊢ filter(P;L1) ≤ if P u then [u / filter(P;v)] else filter(P;v) fi 

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}L2,L1:T  List.  \mforall{}P:\{x:T|  (x  \mmember{}  L2)\}    {}\mrightarrow{}  \mBbbB{}.    (L1  \mleq{}  L2  {}\mRightarrow{}  filter(P;L1)  \mleq{}  filter(P;L2))


By

---

Latex:
(InductionOnList  THEN  Reduce  0  THEN  (UnivCD  THENA  Auto))

---

Home Index