---

Step * of Lemma sign-inverse

∀[n:ℕ]. ∀[f:{p:ℕn ⟶ ℕn| Inj(ℕn;ℕn;p)} ].  (permutation-sign(n;inv(f)) = permutation-sign(n;f) ∈ {s:ℤ| |s| = 1 ∈ ℤ} )
BY
{ (InstLemma `permutation-sign-compose` []
   THEN RepeatFor 2 (ParallelLast')
   THEN (InstHyp [⌜inv(f)⌝] (-1)⋅ THENA Auto)) }

1
1. n : ℕ
2. f : {p:ℕn ⟶ ℕn| Inj(ℕn;ℕn;p)} 
3. ∀[g:{p:ℕn ⟶ ℕn| Inj(ℕn;ℕn;p)} ]
     (permutation-sign(n;f o g) = (permutation-sign(n;f) * permutation-sign(n;g)) ∈ {s:ℤ| |s| = 1 ∈ ℤ} )
4. permutation-sign(n;f o inv(f)) = (permutation-sign(n;f) * permutation-sign(n;inv(f))) ∈ {s:ℤ| |s| = 1 ∈ ℤ} 
⊢ permutation-sign(n;inv(f)) = permutation-sign(n;f) ∈ {s:ℤ| |s| = 1 ∈ ℤ} 

---

Latex:

---

Latex:
\mforall{}[n:\mBbbN{}].  \mforall{}[f:\{p:\mBbbN{}n  {}\mrightarrow{}  \mBbbN{}n|  Inj(\mBbbN{}n;\mBbbN{}n;p)\}  ].    (permutation-sign(n;inv(f))  =  permutation-sign(n;f))


By

---

Latex:
(InstLemma  `permutation-sign-compose`  []
  THEN  RepeatFor  2  (ParallelLast')
  THEN  (InstHyp  [\mkleeneopen{}inv(f)\mkleeneclose{}]  (-1)\mcdot{}  THENA  Auto))

---

Home Index