---

Step * 1 2 of Lemma restrict_perm_using_txpose


1. n : {1...}
2. p : Sym(n)
3. (txpose_perm(n - 1;p.f (n - 1)) O p.f (n - 1)) = (n - 1) ∈ ℕn
⊢ p = txpose_perm(n - 1;p.f (n - 1)) O ↑{n - 1}(restrict_perm(txpose_perm(n - 1;p.f (n - 1)) O p;n - 1)) ∈ Sym(n)
BY
{ (RWH (LemmaC `extend_restrict_perm_cancel`) 0 THENA Auto) }

1
1. n : {1...}
2. p : Sym(n)
3. (txpose_perm(n - 1;p.f (n - 1)) O p.f (n - 1)) = (n - 1) ∈ ℕn
⊢ p = txpose_perm(n - 1;p.f (n - 1)) O txpose_perm(n - 1;p.f (n - 1)) O p ∈ Sym(n)

---

Latex:

---

Latex:

1.  n  :  \{1...\}
2.  p  :  Sym(n)
3.  (txpose\_perm(n  -  1;p.f  (n  -  1))  O  p.f  (n  -  1))  =  (n  -  1)
\mvdash{}  p
=  txpose\_perm(n  -  1
                            ;p.f  (n  -  1))
      O  \muparrow{}\{n  -  1\}(restrict\_perm(txpose\_perm(n  -  1
                                                                                ;p.f  (n  -  1))
                                                          O  p;n  -  1))


By

---

Latex:
(RWH  (LemmaC  `extend\_restrict\_perm\_cancel`)  0  THENA  Auto)

---

Home Index