---

Step * of Lemma extend_perm_wf

∀n:ℕ. ∀p:Sym(n).  (↑{n}(p) ∈ Sym(n + 1))
BY
{ ((Unfolds ``sym_grp extend_perm`` 0 THEN UnivCD) THENA Auto) }

1
1. n : ℕ
2. p : Perm(ℕn)
⊢ mk_perm(extend_permf(p.f;n);extend_permf(p.b;n)) ∈ Perm(ℕn + 1)

---

Latex:

---

Latex:
\mforall{}n:\mBbbN{}.  \mforall{}p:Sym(n).    (\muparrow{}\{n\}(p)  \mmember{}  Sym(n  +  1))


By

---

Latex:
((Unfolds  ``sym\_grp  extend\_perm``  0  THEN  UnivCD)  THENA  Auto)

---

Home Index