---

Step * of Lemma permutation-mapfilter

∀[A:Type]
  ∀L1,L2:A List.
    (permutation(A;L1;L2)
    ⇒ (∀p:A ⟶ 𝔹. ∀[B:Type]. ∀f:{a:A| ↑(p a)}  ⟶ B. permutation(B;mapfilter(f;p;L1);mapfilter(f;p;L2))))
BY
{ (Auto
   THEN Unfold `mapfilter` 0
   THEN (BLemma `permutation-map` THEN Auto)
   THEN BLemma `permutation-filter`
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[A:Type]
    \mforall{}L1,L2:A  List.
        (permutation(A;L1;L2)
        {}\mRightarrow{}  (\mforall{}p:A  {}\mrightarrow{}  \mBbbB{}
                    \mforall{}[B:Type].  \mforall{}f:\{a:A|  \muparrow{}(p  a)\}    {}\mrightarrow{}  B.  permutation(B;mapfilter(f;p;L1);mapfilter(f;p;L2))))


By

---

Latex:
(Auto
  THEN  Unfold  `mapfilter`  0
  THEN  (BLemma  `permutation-map`  THEN  Auto)
  THEN  BLemma  `permutation-filter`
  THEN  Auto)

---

Home Index