Step
*
of Lemma
permutation-sign_wf
∀[n:ℕ]. ∀[f:ℕn ⟶ ℕn]. (permutation-sign(n;f) ∈ {s:ℤ| |s| = 1 ∈ ℤ} )
BY
{ ((InductionOnNat THEN ProveWfLemma) THEN MemTypeCD THEN Auto) }
1
.....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 ∈ ℤ
Latex:
Latex:
\mforall{}[n:\mBbbN{}]. \mforall{}[f:\mBbbN{}n {}\mrightarrow{} \mBbbN{}n]. (permutation-sign(n;f) \mmember{} \{s:\mBbbZ{}| |s| = 1\} )
By
Latex:
((InductionOnNat THEN ProveWfLemma) THEN MemTypeCD THEN Auto)
Home
Index