---

Step * of Lemma extend_perm_over_txpose

∀n:ℕ. ∀i,j:ℕn.  (↑{n}(txpose_perm(i;j)) = txpose_perm(i;j) ∈ Sym(n + 1))
BY
{ (UnivCD THENA Auto) }

1
1. n : ℕ@i
2. i : ℕn@i
3. j : ℕn@i
⊢ ↑{n}(txpose_perm(i;j)) = txpose_perm(i;j) ∈ Sym(n + 1)

---

Latex:

---

Latex:
\mforall{}n:\mBbbN{}.  \mforall{}i,j:\mBbbN{}n.    (\muparrow{}\{n\}(txpose\_perm(i;j))  =  txpose\_perm(i;j))


By

---

Latex:
(UnivCD  THENA  Auto)

---

Home Index