---

Step * 1 1 1 2 of Lemma equipollent-distinct-representatives


1. [A] : Type
2. [E] : A ⟶ A ⟶ ℙ
3. EquivRel(A;x,y.E[x;y])
4. L : A List
5. (∀a,b∈L.  ¬E[a;b])
6. ∀a:A. ∃i:ℕ||L||. E[a;L[i]]
7. rep : a:A ⟶ ℕ||L||
8. ∀a:A. E[a;L[rep a]]
9. ∀i,j:ℕ||L||.  (E[L[i];L[j]] ⇒ (i = j ∈ ℤ))
⊢ ∃f:A ⟶ ℕ||L||. ((∀a,b:A.  ((f a) = (f b) ∈ ℕ||L|| ⇐⇒ E[a;b])) ∧ (∀i:ℕ||L||. ∃a:A. ((f a) = i ∈ ℕ||L||)))
BY
{ (With ⌜rep⌝ (D 0)⋅ THEN Auto)⋅ }

1
1. [A] : Type
2. [E] : A ⟶ A ⟶ ℙ
3. EquivRel(A;x,y.E[x;y])
4. L : A List
5. (∀a,b∈L.  ¬E[a;b])
6. ∀a:A. ∃i:ℕ||L||. E[a;L[i]]
7. rep : a:A ⟶ ℕ||L||
8. ∀a:A. E[a;L[rep a]]
9. ∀i,j:ℕ||L||.  (E[L[i];L[j]] ⇒ (i = j ∈ ℤ))
10. a : A
11. b : A
12. (rep a) = (rep b) ∈ ℕ||L||
⊢ E[a;b]

2
1. A : Type
2. E : A ⟶ A ⟶ ℙ
3. EquivRel(A;x,y.E[x;y])
4. L : A List
5. (∀a,b∈L.  ¬E[a;b])
6. ∀a:A. ∃i:ℕ||L||. E[a;L[i]]
7. rep : a:A ⟶ ℕ||L||
8. ∀a:A. E[a;L[rep a]]
9. ∀i,j:ℕ||L||.  (E[L[i];L[j]] ⇒ (i = j ∈ ℤ))
10. a : A
11. b : A
12. E[a;b]
⊢ (rep a) = (rep b) ∈ ℕ||L||

3
1. [A] : Type
2. [E] : A ⟶ A ⟶ ℙ
3. EquivRel(A;x,y.E[x;y])
4. L : A List
5. (∀a,b∈L.  ¬E[a;b])
6. ∀a:A. ∃i:ℕ||L||. E[a;L[i]]
7. rep : a:A ⟶ ℕ||L||
8. ∀a:A. E[a;L[rep a]]
9. ∀i,j:ℕ||L||.  (E[L[i];L[j]] ⇒ (i = j ∈ ℤ))
10. ∀a,b:A.  ((rep a) = (rep b) ∈ ℕ||L|| ⇐⇒ E[a;b])
11. i : ℕ||L||
⊢ ∃a:A. ((rep a) = i ∈ ℕ||L||)

---

Latex:

---

Latex:

1.  [A]  :  Type
2.  [E]  :  A  {}\mrightarrow{}  A  {}\mrightarrow{}  \mBbbP{}
3.  EquivRel(A;x,y.E[x;y])
4.  L  :  A  List
5.  (\mforall{}a,b\mmember{}L.    \mneg{}E[a;b])
6.  \mforall{}a:A.  \mexists{}i:\mBbbN{}||L||.  E[a;L[i]]
7.  rep  :  a:A  {}\mrightarrow{}  \mBbbN{}||L||
8.  \mforall{}a:A.  E[a;L[rep  a]]
9.  \mforall{}i,j:\mBbbN{}||L||.    (E[L[i];L[j]]  {}\mRightarrow{}  (i  =  j))
\mvdash{}  \mexists{}f:A  {}\mrightarrow{}  \mBbbN{}||L||.  ((\mforall{}a,b:A.    ((f  a)  =  (f  b)  \mLeftarrow{}{}\mRightarrow{}  E[a;b]))  \mwedge{}  (\mforall{}i:\mBbbN{}||L||.  \mexists{}a:A.  ((f  a)  =  i)))


By

---

Latex:
(With  \mkleeneopen{}rep\mkleeneclose{}  (D  0)\mcdot{}  THEN  Auto)\mcdot{}

---

Home Index