---

Step * 2 2 1 1 1 1 of Lemma cyclic-map-equipollent

.....equality..... 
1. n : ℕ+
2. ∀L:Combination(n - 1;ℕn - 1). ([n - 1 / L] ∈ Combination(n;ℕn))
3. b : cyclic-map(ℕn)
4. orbit : ℕn List
5. (0 ∈ orbit)
6. orbit(ℕn;b;orbit)
7. ∀y:ℕn. (y ∈ orbit)
⊢ b = cycle(orbit) ∈ cyclic-map(ℕn)
BY
{ (RepeatFor 2 (DVar `b') THEN EqTypeCD THEN Auto THEN (EqTypeCD THEN Auto)⋅) }

1
1. n : ℕ+
2. ∀L:Combination(n - 1;ℕn - 1). ([n - 1 / L] ∈ Combination(n;ℕn))
3. b : ℕn ⟶ ℕn
4. Inj(ℕn;ℕn;b)
5. ∀x,y:ℕn.  ∃n@0:ℕ. ((b^n@0 x) = y ∈ ℕn)
6. orbit : ℕn List
7. (0 ∈ orbit)
8. orbit(ℕn;b;orbit)
9. ∀y:ℕn. (y ∈ orbit)
⊢ b = cycle(orbit) ∈ (ℕn ⟶ ℕn)

---

Latex:

---

Latex:
.....equality..... 
1.  n  :  \mBbbN{}\msupplus{}
2.  \mforall{}L:Combination(n  -  1;\mBbbN{}n  -  1).  ([n  -  1  /  L]  \mmember{}  Combination(n;\mBbbN{}n))
3.  b  :  cyclic-map(\mBbbN{}n)
4.  orbit  :  \mBbbN{}n  List
5.  (0  \mmember{}  orbit)
6.  orbit(\mBbbN{}n;b;orbit)
7.  \mforall{}y:\mBbbN{}n.  (y  \mmember{}  orbit)
\mvdash{}  b  =  cycle(orbit)


By

---

Latex:
(RepeatFor  2  (DVar  `b')  THEN  EqTypeCD  THEN  Auto  THEN  (EqTypeCD  THEN  Auto)\mcdot{})

---

Home Index