---

Step * of Lemma member_map_filter

∀[T:Type]
  ∀P:T ⟶ 𝔹
    ∀[T':Type]
      ∀f:{x:T| ↑(P x)}  ⟶ T'. ∀L:T List. ∀x:T'.
        ((x ∈ mapfilter(f;P;L)) ⇐⇒ ∃y:T. ((y ∈ L) ∧ ((↑(P y)) c∧ (x = (f y) ∈ T'))))
BY
{ ((UnivCD THENA Auto)
   THEN Unfold `mapfilter` 0
   THEN (GenConcl ⌜filter(P;L) = PL ∈ ({x:T| ↑(P x)}  List)⌝⋅
         THENA (Try (Complete (Auto)) THEN BLemma `filter_type` THEN Auto)
         )
   THEN RWO "member-map" 0
   THEN Auto
   THEN ParallelLast
   THEN Auto
   THEN D -1
   THEN (Eliminate ⌜PL⌝⋅
         THEN Auto
         THEN (Assert ⌜(y ∈ filter(P;L))⌝⋅
               THEN Try ((RWO "member_filter" (-1) THEN Complete (Auto)))
               THEN Try ((RWO "member_filter" (0) THEN Complete (Auto)))
               THEN Try ((Thin (-1) THEN RepeatFor 4 (ParallelLast))))⋅)⋅) }

---

Latex:

---

Latex:
\mforall{}[T:Type]
    \mforall{}P:T  {}\mrightarrow{}  \mBbbB{}
        \mforall{}[T':Type]
            \mforall{}f:\{x:T|  \muparrow{}(P  x)\}    {}\mrightarrow{}  T'.  \mforall{}L:T  List.  \mforall{}x:T'.
                ((x  \mmember{}  mapfilter(f;P;L))  \mLeftarrow{}{}\mRightarrow{}  \mexists{}y:T.  ((y  \mmember{}  L)  \mwedge{}  ((\muparrow{}(P  y))  c\mwedge{}  (x  =  (f  y)))))


By

---

Latex:
((UnivCD  THENA  Auto)
  THEN  Unfold  `mapfilter`  0
  THEN  (GenConcl  \mkleeneopen{}filter(P;L)  =  PL\mkleeneclose{}\mcdot{}
              THENA  (Try  (Complete  (Auto))  THEN  BLemma  `filter\_type`  THEN  Auto)
              )
  THEN  RWO  "member-map"  0
  THEN  Auto
  THEN  ParallelLast
  THEN  Auto
  THEN  D  -1
  THEN  (Eliminate  \mkleeneopen{}PL\mkleeneclose{}\mcdot{}
              THEN  Auto
              THEN  (Assert  \mkleeneopen{}(y  \mmember{}  filter(P;L))\mkleeneclose{}\mcdot{}
                          THEN  Try  ((RWO  "member\_filter"  (-1)  THEN  Complete  (Auto)))
                          THEN  Try  ((RWO  "member\_filter"  (0)  THEN  Complete  (Auto)))
                          THEN  Try  ((Thin  (-1)  THEN  RepeatFor  4  (ParallelLast))))\mcdot{})\mcdot{})

---

Home Index