---

Step * of Lemma filter_iseg

∀[T:Type]. ∀P:T ⟶ 𝔹. ∀L2,L1:T List.  (L1 ≤ L2 ⇒ filter(P;L1) ≤ filter(P;L2))
BY
{ (((RepeatFor 3 (D 0 THENA Auto) THEN ListInd (-1)) THENA Auto) THEN Reduce 0) }

1
1. [T] : Type
2. P : T ⟶ 𝔹
⊢ ∀L1:T List. (L1 ≤ [] ⇒ filter(P;L1) ≤ [])

2
1. [T] : Type
2. P : T ⟶ 𝔹
3. u : T
4. v : T List
5. ∀L1:T List. (L1 ≤ v ⇒ filter(P;L1) ≤ filter(P;v))
⊢ ∀L1:T List. (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{}P:T  {}\mrightarrow{}  \mBbbB{}.  \mforall{}L2,L1:T  List.    (L1  \mleq{}  L2  {}\mRightarrow{}  filter(P;L1)  \mleq{}  filter(P;L2))


By

---

Latex:
(((RepeatFor  3  (D  0  THENA  Auto)  THEN  ListInd  (-1))  THENA  Auto)  THEN  Reduce  0)

---

Home Index