---

Step * of Lemma mapfilter-contains

∀[T,S:Type].  ∀as,bs:T List. ∀P:T ⟶ 𝔹. ∀f:{x:T| ↑(P x)}  ⟶ S.  (as ⊆ bs ⇒ mapfilter(f;P;as) ⊆ mapfilter(f;P;bs))
BY
{ ((Unfold `l_contains` 0 THEN Auto)
   THEN All (RWO "l_all_iff")
   THEN Auto
   THEN All (RWO "member-mapfilter")
   THEN Auto
   THEN RepeatFor 2 (ParallelLast)
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[T,S:Type].
    \mforall{}as,bs:T  List.  \mforall{}P:T  {}\mrightarrow{}  \mBbbB{}.  \mforall{}f:\{x:T|  \muparrow{}(P  x)\}    {}\mrightarrow{}  S.
        (as  \msubseteq{}  bs  {}\mRightarrow{}  mapfilter(f;P;as)  \msubseteq{}  mapfilter(f;P;bs))


By

---

Latex:
((Unfold  `l\_contains`  0  THEN  Auto)
  THEN  All  (RWO  "l\_all\_iff")
  THEN  Auto
  THEN  All  (RWO  "member-mapfilter")
  THEN  Auto
  THEN  RepeatFor  2  (ParallelLast)
  THEN  Auto)

---

Home Index