---

Step * of Lemma restrict_perm_wf

∀n:ℕ. ∀p:Sym(n + 1).  (((p.f n) = n ∈ ℕn + 1) ⇒ (restrict_perm(p;n) ∈ Sym(n)))
BY
{ (Unfold `sym_grp` 0 THEN (UnivCD THENA Auto)) }

1
1. n : ℕ
2. p : Perm(ℕn + 1)
3. (p.f n) = n ∈ ℕn + 1
⊢ restrict_perm(p;n) ∈ Perm(ℕn)

---

Latex:

---

Latex:
\mforall{}n:\mBbbN{}.  \mforall{}p:Sym(n  +  1).    (((p.f  n)  =  n)  {}\mRightarrow{}  (restrict\_perm(p;n)  \mmember{}  Sym(n)))


By

---

Latex:
(Unfold  `sym\_grp`  0  THEN  (UnivCD  THENA  Auto))

---

Home Index