Step * of Lemma txpose_perm_id

n:ℕ. ∀i,j:ℕn.  ((i j ∈ ℤ (txpose_perm(i;j) id_perm() ∈ Sym(n)))
BY
Auto }

1
1. : ℕ
2. : ℕn
3. : ℕn
4. j ∈ ℤ
⊢ txpose_perm(i;j) id_perm() ∈ Sym(n)


Latex:


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


By


Latex:
Auto




Home Index