Step
*
1
1
1
1
1
of Lemma
rng_prod_plus
1. n : ℤ
2. 0 < n
3. filter(λ2p.(p (n - 1) =z 0);functions-list(n;2)) ∈ (ℕn ⟶ ℕ2) List
4. map(λf,i. if (i =z n - 1) then 0 else f i fi ;functions-list(n - 1;2)) ∈ (ℕn ⟶ ℕ2) List
⊢ permutation(ℕn ⟶ ℕ2;filter(λ2p.(p (n - 1) =z 0);functions-list(n;2));
map(λf,i. if (i =z n - 1) then 0 else f i fi ;functions-list(n - 1;2)))
BY
{ ((Assert no_repeats(ℕn ⟶ ℕ2;functions-list(n;2)) BY
(GenConclTerm ⌜functions-list(n;2)⌝⋅ THEN Auto))
THEN BLemma `permutation-when-no_repeats`
THEN Auto) }
1
1. n : ℤ
2. 0 < n
3. filter(λ2p.(p (n - 1) =z 0);functions-list(n;2)) ∈ (ℕn ⟶ ℕ2) List
4. map(λf,i. if (i =z n - 1) then 0 else f i fi ;functions-list(n - 1;2)) ∈ (ℕn ⟶ ℕ2) List
5. no_repeats(ℕn ⟶ ℕ2;functions-list(n;2))
6. x : ℕn ⟶ ℕ2
7. (x ∈ map(λf,i. if (i =z n - 1) then 0 else f i fi ;functions-list(n - 1;2)))
⊢ (x ∈ filter(λ2p.(p (n - 1) =z 0);functions-list(n;2)))
2
1. n : ℤ
2. 0 < n
3. filter(λ2p.(p (n - 1) =z 0);functions-list(n;2)) ∈ (ℕn ⟶ ℕ2) List
4. map(λf,i. if (i =z n - 1) then 0 else f i fi ;functions-list(n - 1;2)) ∈ (ℕn ⟶ ℕ2) List
5. no_repeats(ℕn ⟶ ℕ2;functions-list(n;2))
6. x : ℕn ⟶ ℕ2
7. (x ∈ filter(λ2p.(p (n - 1) =z 0);functions-list(n;2)))
⊢ (x ∈ map(λf,i. if (i =z n - 1) then 0 else f i fi ;functions-list(n - 1;2)))
3
1. n : ℤ
2. 0 < n
3. filter(λ2p.(p (n - 1) =z 0);functions-list(n;2)) ∈ (ℕn ⟶ ℕ2) List
4. map(λf,i. if (i =z n - 1) then 0 else f i fi ;functions-list(n - 1;2)) ∈ (ℕn ⟶ ℕ2) List
5. no_repeats(ℕn ⟶ ℕ2;functions-list(n;2))
⊢ no_repeats(ℕn ⟶ ℕ2;map(λf,i. if (i =z n - 1) then 0 else f i fi ;functions-list(n - 1;2)))
Latex:
Latex:
1. n : \mBbbZ{}
2. 0 < n
3. filter(\mlambda{}\msubtwo{}p.(p (n - 1) =\msubz{} 0);functions-list(n;2)) \mmember{} (\mBbbN{}n {}\mrightarrow{} \mBbbN{}2) List
4. map(\mlambda{}f,i. if (i =\msubz{} n - 1) then 0 else f i fi ;functions-list(n - 1;2)) \mmember{} (\mBbbN{}n {}\mrightarrow{} \mBbbN{}2) List
\mvdash{} permutation(\mBbbN{}n {}\mrightarrow{} \mBbbN{}2;filter(\mlambda{}\msubtwo{}p.(p (n - 1) =\msubz{} 0);functions-list(n;2));map(\mlambda{}f,i. if (i =\msubz{} n - 1)
then 0
else f i
fi ;functions-list(\000Cn
- 1;2)))
By
Latex:
((Assert no\_repeats(\mBbbN{}n {}\mrightarrow{} \mBbbN{}2;functions-list(n;2)) BY
(GenConclTerm \mkleeneopen{}functions-list(n;2)\mkleeneclose{}\mcdot{} THEN Auto))
THEN BLemma `permutation-when-no\_repeats`
THEN Auto)
Home
Index