---

Step * of Lemma extend_restrict_perm_cancel

∀n:{1...}. ∀p:Sym(n).  (((p.f (n - 1)) = (n - 1) ∈ ℕn) ⇒ (↑{n - 1}(restrict_perm(p;n - 1)) = p ∈ Sym(n)))
BY
{ (UnivCD THENA Auto) }

1
1. n : {1...}
2. p : Sym(n)
3. (p.f (n - 1)) = (n - 1) ∈ ℕn
⊢ ↑{n - 1}(restrict_perm(p;n - 1)) = p ∈ Sym(n)

---

Latex:

---

Latex:
\mforall{}n:\{1...\}.  \mforall{}p:Sym(n).    (((p.f  (n  -  1))  =  (n  -  1))  {}\mRightarrow{}  (\muparrow{}\{n  -  1\}(restrict\_perm(p;n  -  1))  =  p))


By

---

Latex:
(UnivCD  THENA  Auto)

---

Home Index