---

Step * of Lemma filter_map

∀[T1,T2:Type]. ∀[f:T1 ⟶ T2]. ∀[Q:T2 ⟶ 𝔹]. ∀[L:T1 List].  (filter(Q;map(f;L)) ~ map(f;filter(Q o f;L)))
BY
{ (InductionOnList THEN Reduce 0 THEN Try (Trivial) THEN AutoSplit THEN EqCD THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[T1,T2:Type].  \mforall{}[f:T1  {}\mrightarrow{}  T2].  \mforall{}[Q:T2  {}\mrightarrow{}  \mBbbB{}].  \mforall{}[L:T1  List].
    (filter(Q;map(f;L))  \msim{}  map(f;filter(Q  o  f;L)))


By

---

Latex:
(InductionOnList  THEN  Reduce  0  THEN  Try  (Trivial)  THEN  AutoSplit  THEN  EqCD  THEN  Auto)

---

Home Index