Step
*
of Lemma
txpose_perm_inv
∀n:ℕ. ∀i,j:ℕn. (inv_perm(txpose_perm(i;j)) = txpose_perm(i;j) ∈ Sym(n))
BY
{ Auto }
1
1. n : ℕ
2. i : ℕn
3. j : ℕn
⊢ inv_perm(txpose_perm(i;j)) = txpose_perm(i;j) ∈ Sym(n)
Latex:
Latex:
\mforall{}n:\mBbbN{}. \mforall{}i,j:\mBbbN{}n. (inv\_perm(txpose\_perm(i;j)) = txpose\_perm(i;j))
By
Latex:
Auto
Home
Index