---

Step * of Lemma map-filter

∀[T,A:Type]. ∀[f:T ⟶ A]. ∀[P:T ⟶ 𝔹]. ∀[Q:A ⟶ 𝔹].
  ∀[L:T List]. (map(f;filter(P;L)) ~ filter(Q;map(f;L))) supposing ∀x:T. Q (f x) = P x
BY
{ (InductionOnList
   THEN Reduce 0
   THEN Try (Trivial)
   THEN RepeatFor 2 ((SplitOnConclITE THENA Auto))
   THEN Reduce 0
   THEN Try (Complete ((EqCD THEN Auto)))
   THEN (RWO "6" (-1) THEN Auto)⋅) }

---

Latex:

---

Latex:
\mforall{}[T,A:Type].  \mforall{}[f:T  {}\mrightarrow{}  A].  \mforall{}[P:T  {}\mrightarrow{}  \mBbbB{}].  \mforall{}[Q:A  {}\mrightarrow{}  \mBbbB{}].
    \mforall{}[L:T  List].  (map(f;filter(P;L))  \msim{}  filter(Q;map(f;L)))  supposing  \mforall{}x:T.  Q  (f  x)  =  P  x


By

---

Latex:
(InductionOnList
  THEN  Reduce  0
  THEN  Try  (Trivial)
  THEN  RepeatFor  2  ((SplitOnConclITE  THENA  Auto))
  THEN  Reduce  0
  THEN  Try  (Complete  ((EqCD  THEN  Auto)))
  THEN  (RWO  "6"  (-1)  THEN  Auto)\mcdot{})

---

Home Index