---

Step * 1 2 1 of Lemma txpose_perm_id


1. n : ℕ
2. i : ℕn
3. j : ℕn
4. i = j ∈ ℤ
5. txpose_perm(i
               ;j) ∈ Sym(n)
⊢ InvFuns(ℕn;ℕn;txpose_perm(i
                            ;j).f;txpose_perm(i
                                              ;j).b)
BY
{ ((Unfold `sym_grp` 5 THEN MemTypeHD 5) THEN Auto) }

---

Latex:

---

Latex:

1.  n  :  \mBbbN{}
2.  i  :  \mBbbN{}n
3.  j  :  \mBbbN{}n
4.  i  =  j
5.  txpose\_perm(i
                              ;j)  \mmember{}  Sym(n)
\mvdash{}  InvFuns(\mBbbN{}n;\mBbbN{}n;txpose\_perm(i
                                                        ;j).f;txpose\_perm(i
                                                                                            ;j).b)


By

---

Latex:
((Unfold  `sym\_grp`  5  THEN  MemTypeHD  5)  THEN  Auto)

---

Home Index