---

Step * 1 1 of Lemma compose-fpf-dom


1. [A] : Type
2. [B] : A ─→ Type
3. d : A List@i
4. f1 : x:{x:A| (x ∈ d)}  ─→ B[x]@i
5. [C] : Type
6. a : A ─→ (C?)@i
7. b : C ─→ A@i
8. y : C@i
⊢ (y ∈ mapfilter(λx.outl(a x);λx.isl(a x);d)) ⇐⇒ ∃x:A. ((x ∈ d) ∧ ((↑isl(a x)) c∧ (y = outl(a x) ∈ C)))
BY
{ ((RWO "member_map_filter" 0 THENA Auto) THEN All Reduce THEN Try (((D (-1)) THEN Unhide THEN Auto)) THEN Auto) }

---

Latex:



1.  [A]  :  Type
2.  [B]  :  A  {}\mrightarrow{}  Type
3.  d  :  A  List@i
4.  f1  :  x:\{x:A|  (x  \mmember{}  d)\}    {}\mrightarrow{}  B[x]@i
5.  [C]  :  Type
6.  a  :  A  {}\mrightarrow{}  (C?)@i
7.  b  :  C  {}\mrightarrow{}  A@i
8.  y  :  C@i
\mvdash{}  (y  \mmember{}  mapfilter(\mlambda{}x.outl(a  x);\mlambda{}x.isl(a  x);d))  \mLeftarrow{}{}\mRightarrow{}  \mexists{}x:A.  ((x  \mmember{}  d)  \mwedge{}  ((\muparrow{}isl(a  x))  c\mwedge{}  (y  =  outl(a  x))))


By

((RWO  "member\_map\_filter"  0  THENA  Auto)
  THEN  All  Reduce
  THEN  Try  (((D  (-1))  THEN  Unhide  THEN  Auto))
  THEN  Auto)

---

Home Index