Step * of Lemma restrict_perm_using_txpose

n:{1...}. ∀p:Sym(n).  ∃q:Sym(n 1). ∃i,j:ℕn. (p txpose_perm(i;j) O ↑{n 1}(q) ∈ Sym(n))
BY
(UnivCD THENA Auto) }

1
1. {1...}
2. Sym(n)
⊢ ∃q:Sym(n 1). ∃i,j:ℕn. (p txpose_perm(i;j) O ↑{n 1}(q) ∈ Sym(n))


Latex:


Latex:
\mforall{}n:\{1...\}.  \mforall{}p:Sym(n).    \mexists{}q:Sym(n  -  1).  \mexists{}i,j:\mBbbN{}n.  (p  =  txpose\_perm(i;j)  O  \muparrow{}\{n  -  1\}(q))


By


Latex:
(UnivCD  THENA  Auto)




Home Index