---

Step * of Lemma member-partial-permutations-list

∀n:ℕ+. ∀i:ℤ. ∀f:ℕn →⟶ ℕn.  (f ∈ partial-permutations-list(n;i)) supposing (f (n - 1)) = i ∈ ℤ
BY
{ (Auto THEN Unfold `partial-permutations-list` 0 THEN BLemma `member_filter` THEN Auto) }

---

Latex:

---

Latex:
\mforall{}n:\mBbbN{}\msupplus{}.  \mforall{}i:\mBbbZ{}.  \mforall{}f:\mBbbN{}n  \mrightarrow{}{}\mrightarrow{}  \mBbbN{}n.    (f  \mmember{}  partial-permutations-list(n;i))  supposing  (f  (n  -  1))  =  i


By

---

Latex:
(Auto  THEN  Unfold  `partial-permutations-list`  0  THEN  BLemma  `member\_filter`  THEN  Auto)

---

Home Index