---

Step * of Lemma rotate-surjection

∀n:ℕ+. Surj(ℕn;ℕn;rot(n))
BY
{ (InstLemma `rotate-inverse1` [] THEN ParallelLast') }

1
1. n : ℕ+
2. (rot(n) o rot(n)^n - 1) = (λx.x) ∈ (ℕn ⟶ ℕn)
⊢ Surj(ℕn;ℕn;rot(n))

---

Latex:

---

Latex:
\mforall{}n:\mBbbN{}\msupplus{}.  Surj(\mBbbN{}n;\mBbbN{}n;rot(n))


By

---

Latex:
(InstLemma  `rotate-inverse1`  []  THEN  ParallelLast')

---

Home Index