---

Step * of Lemma member-mapfilter-witness_wf

member-mapfilter-witness() ∈ ∀[T:Type]
                               ∀L:T List. ∀P:{x:T| (x ∈ L)}  ⟶ 𝔹.
                                 ∀[T':Type]
                                   ∀f:{x:T| (x ∈ L) c∧ (↑(P x))}  ⟶ T'. ∀x:T'.
                                     ((x ∈ mapfilter(f;P;L)) ⇐⇒ ∃y:T. ((y ∈ L) ∧ ((↑(P y)) c∧ (x = (f y) ∈ T'))))
BY
{ ((Assert TERMOF{member-mapfilter-univ:o, 1:l, i:l} ∈ ∀[T:Type]
                                                         ∀L:T List. ∀P:{x:T| (x ∈ L)}  ⟶ 𝔹.
                                                           ∀[T':Type]
                                                             ∀f:{x:T| (x ∈ L) c∧ (↑(P x))}  ⟶ T'. ∀x:T'.
                                                               ((x ∈ mapfilter(f;P;L))
                                                               ⇐⇒ ∃y:T. ((y ∈ L) ∧ ((↑(P y)) c∧ (x = (f y) ∈ T')))) BY
          Auto)⋅
   THEN (NthHypSq (-1) THEN EqCD THEN Try (Trivial) THEN All Thin)
   THEN Unfold `member-mapfilter-witness` 0) }

1
TERMOF{member-mapfilter-univ:o, 1:l, 1:l} ~ TERMOF{member-mapfilter-univ:o, 1:l, i:l}

---

Latex:

---

Latex:
member-mapfilter-witness()  \mmember{}  \mforall{}[T:Type]
                                                              \mforall{}L:T  List.  \mforall{}P:\{x:T|  (x  \mmember{}  L)\}    {}\mrightarrow{}  \mBbbB{}.
                                                                  \mforall{}[T':Type]
                                                                      \mforall{}f:\{x:T|  (x  \mmember{}  L)  c\mwedge{}  (\muparrow{}(P  x))\}    {}\mrightarrow{}  T'.  \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:
((Assert  TERMOF\{member-mapfilter-univ:o,  1:l,  i:l\}  \mmember{}  \mforall{}[T:Type]
                                                                                                              \mforall{}L:T  List.  \mforall{}P:\{x:T|  (x  \mmember{}  L)\}    {}\mrightarrow{}  \mBbbB{}.
                                                                                                                  \mforall{}[T':Type]
                                                                                                                      \mforall{}f:\{x:T|  (x  \mmember{}  L)  c\mwedge{}  (\muparrow{}(P  x))\}    {}\mrightarrow{}  T'.
                                                                                                                      \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
                Auto)\mcdot{}
  THEN  (NthHypSq  (-1)  THEN  EqCD  THEN  Try  (Trivial)  THEN  All  Thin)
  THEN  Unfold  `member-mapfilter-witness`  0)

---

Home Index