Step * 1 2 1 1 of Lemma restrict_perm_using_txpose


1. {1...}
2. Sym(n)
3. (txpose_perm(n 1;p.f (n 1)) p.f (n 1)) (n 1) ∈ ℕn
⊢ id_perm() p ∈ Sym(n)
BY
(RWH (GenLemmaC `perm_ident`) THEN Auto) }


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  =  id\_perm()  O  p


By


Latex:
(RWH  (GenLemmaC  2  `perm\_ident`)  0  THEN  Auto)




Home Index