Step
*
1
1
of Lemma
no_repeats_functionality_wrt_permutation
1. A : Type
2. as1 : A List
3. as2 : A List
4. f : ℕ||as1|| ⟶ ℕ||as1||
5. Inj(ℕ||as1||;ℕ||as1||;f)
6. as2 = (as1 o f) ∈ (A List)
7. ∀[i,j:ℕ]. (¬(as1[i] = as1[j] ∈ A)) supposing ((¬(i = j ∈ ℕ)) and j < ||as1|| and i < ||as1||)
⊢ ∀[i,j:ℕ]. (¬((as1 o f)[i] = (as1 o f)[j] ∈ A)) supposing ((¬(i = j ∈ ℕ)) and j < ||(as1 o f)|| and i < ||(as1 o f)||)
BY
{ (Auto THEN RWO "permute_list_select" 0 THEN Auto) }
1
1. A : Type
2. as1 : A List
3. as2 : A List
4. f : ℕ||as1|| ⟶ ℕ||as1||
5. Inj(ℕ||as1||;ℕ||as1||;f)
6. as2 = (as1 o f) ∈ (A List)
7. ∀[i,j:ℕ]. (¬(as1[i] = as1[j] ∈ A)) supposing ((¬(i = j ∈ ℕ)) and j < ||as1|| and i < ||as1||)
8. i : ℕ
9. j : ℕ
10. i < ||(as1 o f)||
11. j < ||(as1 o f)||
12. ¬(i = j ∈ ℕ)
⊢ ¬(as1[f i] = as1[f j] ∈ A)
Latex:
Latex:
1. A : Type
2. as1 : A List
3. as2 : A List
4. f : \mBbbN{}||as1|| {}\mrightarrow{} \mBbbN{}||as1||
5. Inj(\mBbbN{}||as1||;\mBbbN{}||as1||;f)
6. as2 = (as1 o f)
7. \mforall{}[i,j:\mBbbN{}]. (\mneg{}(as1[i] = as1[j])) supposing ((\mneg{}(i = j)) and j < ||as1|| and i < ||as1||)
\mvdash{} \mforall{}[i,j:\mBbbN{}].
(\mneg{}((as1 o f)[i] = (as1 o f)[j])) supposing
((\mneg{}(i = j)) and
j < ||(as1 o f)|| and
i < ||(as1 o f)||)
By
Latex:
(Auto THEN RWO "permute\_list\_select" 0 THEN Auto)
Home
Index