---

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