---

Step * of Lemma restrict_perm_using_txpose

∀n:{1...}. ∀p:Sym(n).  ∃q:Sym(n - 1). ∃i,j:ℕn. (p = txpose_perm(i;j) O ↑{n - 1}(q) ∈ Sym(n))
BY
{ (UnivCD THENA Auto) }

1
1. n : {1...}
2. p : Sym(n)
⊢ ∃q:Sym(n - 1). ∃i,j:ℕn. (p = txpose_perm(i;j) O ↑{n - 1}(q) ∈ Sym(n))

---

Latex:

---

Latex:
\mforall{}n:\{1...\}.  \mforall{}p:Sym(n).    \mexists{}q:Sym(n  -  1).  \mexists{}i,j:\mBbbN{}n.  (p  =  txpose\_perm(i;j)  O  \muparrow{}\{n  -  1\}(q))


By

---

Latex:
(UnivCD  THENA  Auto)

---

Home Index