---

Step * of Lemma permutation-of-permutations-list

∀n:ℕ. ∀f:{p:ℕn ⟶ ℕn| Inj(ℕn;ℕn;p)}  ⟶ {p:ℕn ⟶ ℕn| Inj(ℕn;ℕn;p)} .
  (Bij({p:ℕn ⟶ ℕn| Inj(ℕn;ℕn;p)} ;{p:ℕn ⟶ ℕn| Inj(ℕn;ℕn;p)} ;f)
  ⇒ permutation({p:ℕn ⟶ ℕn| Inj(ℕn;ℕn;p)} ;permutations-list(n);map(f;permutations-list(n))))
BY
{ (Auto
   THEN BLemma `map-is-permutation-on-list-of-all`
   THEN Auto
   THEN GenConclTerm ⌜permutations-list(n)⌝⋅
   THEN Auto
   THEN D -2
   THEN Try ((Unhide THEN Auto))
   THEN InstHyp [⌜t⌝] (-2)⋅
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}n:\mBbbN{}.  \mforall{}f:\{p:\mBbbN{}n  {}\mrightarrow{}  \mBbbN{}n|  Inj(\mBbbN{}n;\mBbbN{}n;p)\}    {}\mrightarrow{}  \{p:\mBbbN{}n  {}\mrightarrow{}  \mBbbN{}n|  Inj(\mBbbN{}n;\mBbbN{}n;p)\}  .
    (Bij(\{p:\mBbbN{}n  {}\mrightarrow{}  \mBbbN{}n|  Inj(\mBbbN{}n;\mBbbN{}n;p)\}  ;\{p:\mBbbN{}n  {}\mrightarrow{}  \mBbbN{}n|  Inj(\mBbbN{}n;\mBbbN{}n;p)\}  ;f)
    {}\mRightarrow{}  permutation(\{p:\mBbbN{}n  {}\mrightarrow{}  \mBbbN{}n|  Inj(\mBbbN{}n;\mBbbN{}n;p)\}  ;permutations-list(n);map(f;permutations-list(n))))


By

---

Latex:
(Auto
  THEN  BLemma  `map-is-permutation-on-list-of-all`
  THEN  Auto
  THEN  GenConclTerm  \mkleeneopen{}permutations-list(n)\mkleeneclose{}\mcdot{}
  THEN  Auto
  THEN  D  -2
  THEN  Try  ((Unhide  THEN  Auto))
  THEN  InstHyp  [\mkleeneopen{}t\mkleeneclose{}]  (-2)\mcdot{}
  THEN  Auto)

---

Home Index