---

Step * 2 2 of Lemma no_repeats_iff


1. T : Type
2. l : T List
3. ∀[x,y:T].
     ¬(x = y ∈ T) 
     supposing ∃f:ℕ||[x; y]|| ⟶ ℕ||l||. (increasing(f;||[x; y]||) ∧ (∀j:ℕ||[x; y]||. ([x; y][j] = l[f j] ∈ T)))
4. i : ℕ
5. j : ℕ
6. i < ||l||
7. j < ||l||
8. ¬(i = j ∈ ℕ)
9. ¬i < j
⊢ ¬(l[i] = l[j] ∈ T)
BY
{ Assert ¬(l[j] = l[i] ∈ T) }

1
.....assertion..... 
1. T : Type
2. l : T List
3. ∀[x,y:T].
     ¬(x = y ∈ T) 
     supposing ∃f:ℕ||[x; y]|| ⟶ ℕ||l||. (increasing(f;||[x; y]||) ∧ (∀j:ℕ||[x; y]||. ([x; y][j] = l[f j] ∈ T)))
4. i : ℕ
5. j : ℕ
6. i < ||l||
7. j < ||l||
8. ¬(i = j ∈ ℕ)
9. ¬i < j
⊢ ¬(l[j] = l[i] ∈ T)

2
1. T : Type
2. l : T List
3. ∀[x,y:T].
     ¬(x = y ∈ T) 
     supposing ∃f:ℕ||[x; y]|| ⟶ ℕ||l||. (increasing(f;||[x; y]||) ∧ (∀j:ℕ||[x; y]||. ([x; y][j] = l[f j] ∈ T)))
4. i : ℕ
5. j : ℕ
6. i < ||l||
7. j < ||l||
8. ¬(i = j ∈ ℕ)
9. ¬i < j
10. ¬(l[j] = l[i] ∈ T)
⊢ ¬(l[i] = l[j] ∈ T)

---

Latex:

---

Latex:

1.  T  :  Type
2.  l  :  T  List
3.  \mforall{}[x,y:T].
          \mneg{}(x  =  y) 
          supposing  \mexists{}f:\mBbbN{}||[x;  y]||  {}\mrightarrow{}  \mBbbN{}||l||
                                (increasing(f;||[x;  y]||)  \mwedge{}  (\mforall{}j:\mBbbN{}||[x;  y]||.  ([x;  y][j]  =  l[f  j])))
4.  i  :  \mBbbN{}
5.  j  :  \mBbbN{}
6.  i  <  ||l||
7.  j  <  ||l||
8.  \mneg{}(i  =  j)
9.  \mneg{}i  <  j
\mvdash{}  \mneg{}(l[i]  =  l[j])


By

---

Latex:
Assert  \mneg{}(l[j]  =  l[i])

---

Home Index