---

Step * 1 of Lemma permutation-sign_wf

.....set predicate..... 
1. n : ℤ
2. 0 < n
3. ∀[f:ℕn - 1 ⟶ ℕn - 1]. (permutation-sign(n - 1;f) ∈ {s:ℤ| |s| = 1 ∈ ℤ} )
4. f : ℕn ⟶ ℕn
5. j : ℕn
6. i : ℕj
⊢ |sign((f j) - f i)| = 1 ∈ ℤ
BY
{ (RepUR ``sign`` 0 THEN AutoSplit) }

---

Latex:

---

Latex:
.....set  predicate..... 
1.  n  :  \mBbbZ{}
2.  0  <  n
3.  \mforall{}[f:\mBbbN{}n  -  1  {}\mrightarrow{}  \mBbbN{}n  -  1].  (permutation-sign(n  -  1;f)  \mmember{}  \{s:\mBbbZ{}|  |s|  =  1\}  )
4.  f  :  \mBbbN{}n  {}\mrightarrow{}  \mBbbN{}n
5.  j  :  \mBbbN{}n
6.  i  :  \mBbbN{}j
\mvdash{}  |sign((f  j)  -  f  i)|  =  1


By

---

Latex:
(RepUR  ``sign``  0  THEN  AutoSplit)

---

Home Index