---

Step * of Lemma cyclic-map-equipollent

∀n:ℕ+. Combination(n - 1;ℕn - 1) ~ cyclic-map(ℕn)
BY
{ xxx(Auto THEN Assert ⌜∀L:Combination(n - 1;ℕn - 1). ([n - 1 / L] ∈ Combination(n;ℕn))⌝⋅)xxx }

1
.....assertion..... 
1. n : ℕ+
⊢ ∀L:Combination(n - 1;ℕn - 1). ([n - 1 / L] ∈ Combination(n;ℕn))

2
1. n : ℕ+
2. ∀L:Combination(n - 1;ℕn - 1). ([n - 1 / L] ∈ Combination(n;ℕn))
⊢ Combination(n - 1;ℕn - 1) ~ cyclic-map(ℕn)

---

Latex:

---

Latex:
\mforall{}n:\mBbbN{}\msupplus{}.  Combination(n  -  1;\mBbbN{}n  -  1)  \msim{}  cyclic-map(\mBbbN{}n)


By

---

Latex:
xxx(Auto  THEN  Assert  \mkleeneopen{}\mforall{}L:Combination(n  -  1;\mBbbN{}n  -  1).  ([n  -  1  /  L]  \mmember{}  Combination(n;\mBbbN{}n))\mkleeneclose{}\mcdot{})xxx

---

Home Index