Step
*
2
2
1
1
1
of Lemma
cyclic-map-equipollent
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)
⊢ ∃a:Combination(n - 1;ℕn - 1). (cycle([n - 1 / a]) = b ∈ cyclic-map(ℕn))
BY
{ xxx(Subst ⌜b = cycle(orbit) ∈ cyclic-map(ℕn)⌝ 0⋅ THEN Auto)xxx }
1
.....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)
2
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)
⊢ ∃a:Combination(n - 1;ℕn - 1). (cycle([n - 1 / a]) = cycle(orbit) ∈ cyclic-map(ℕn))
Latex:
Latex:
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{} \mexists{}a:Combination(n - 1;\mBbbN{}n - 1). (cycle([n - 1 / a]) = b)
By
Latex:
xxx(Subst \mkleeneopen{}b = cycle(orbit)\mkleeneclose{} 0\mcdot{} THEN Auto)xxx
Home
Index