---

Step * of Lemma length-filter-le

∀[T:Type]. ∀[P1,P2:T ⟶ 𝔹]. ∀[L:T List].  ||filter(P1;L)|| ≤ ||filter(P2;L)|| supposing (∀x∈L.(↑(P1 x)) ⇒ (↑(P2 x)))
BY
{ (InductionOnList
   THEN Reduce 0
   THEN Auto
   THEN (RWO "l_all_cons" (-1) THENA Auto)
   THEN RepeatFor 2 (AutoSplit)
   THEN (Auto THEN ThinTrivial THEN Auto)⋅) }

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[P1,P2:T  {}\mrightarrow{}  \mBbbB{}].  \mforall{}[L:T  List].
    ||filter(P1;L)||  \mleq{}  ||filter(P2;L)||  supposing  (\mforall{}x\mmember{}L.(\muparrow{}(P1  x))  {}\mRightarrow{}  (\muparrow{}(P2  x)))


By

---

Latex:
(InductionOnList
  THEN  Reduce  0
  THEN  Auto
  THEN  (RWO  "l\_all\_cons"  (-1)  THENA  Auto)
  THEN  RepeatFor  2  (AutoSplit)
  THEN  (Auto  THEN  ThinTrivial  THEN  Auto)\mcdot{})

---

Home Index