---

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


1. k : ℕ
2. ∀k:ℕk
     ∀[A:Type]
       (A ~ ℕk
       ⇒ (∀[E:A ⟶ A ⟶ ℙ]
             (EquivRel(A;x,y.E[x;y])
             ⇒ (∀x,y:A.  Dec(E[x;y]))
             ⇒ (∃L:A List. ((∀a,b∈L.  ¬E[a;b]) ∧ (∀a:A. (∃b∈L. E[a;b])) ∧ (||L|| ≤ k))))))
3. [A] : Type
4. A ~ ℕk
5. [E] : A ⟶ A ⟶ ℙ
6. EquivRel(A;x,y.E[x;y])
7. ∀x,y:A.  Dec(E[x;y])
8. ¬(k = 0 ∈ ℤ)
9. b : A
10. i : ℕ
11. j : ℕ
12. k = (i + j) ∈ ℤ
13. {a:A| E[b;a]}  ~ ℕi
14. {a:A| ¬E[b;a]}  ~ ℕj
15. ¬(i = 0 ∈ ℤ)
16. L : {a:A| ¬E[b;a]}  List
17. (∀a,b∈L.  ¬E[a;b]) ∧ (∀a:{a:A| ¬E[b;a]} . (∃b∈L. E[a;b])) ∧ (||L|| ≤ j)
⊢ (∀a:A. (∃b∈[b / L]. E[a;b])) ∧ (||[b / L]|| ≤ k)
BY
{ D 0 }

1
1. k : ℕ
2. ∀k:ℕk
     ∀[A:Type]
       (A ~ ℕk
       ⇒ (∀[E:A ⟶ A ⟶ ℙ]
             (EquivRel(A;x,y.E[x;y])
             ⇒ (∀x,y:A.  Dec(E[x;y]))
             ⇒ (∃L:A List. ((∀a,b∈L.  ¬E[a;b]) ∧ (∀a:A. (∃b∈L. E[a;b])) ∧ (||L|| ≤ k))))))
3. [A] : Type
4. A ~ ℕk
5. [E] : A ⟶ A ⟶ ℙ
6. EquivRel(A;x,y.E[x;y])
7. ∀x,y:A.  Dec(E[x;y])
8. ¬(k = 0 ∈ ℤ)
9. b : A
10. i : ℕ
11. j : ℕ
12. k = (i + j) ∈ ℤ
13. {a:A| E[b;a]}  ~ ℕi
14. {a:A| ¬E[b;a]}  ~ ℕj
15. ¬(i = 0 ∈ ℤ)
16. L : {a:A| ¬E[b;a]}  List
17. (∀a,b∈L.  ¬E[a;b]) ∧ (∀a:{a:A| ¬E[b;a]} . (∃b∈L. E[a;b])) ∧ (||L|| ≤ j)
⊢ ∀a:A. (∃b∈[b / L]. E[a;b])

2
1. k : ℕ
2. ∀k:ℕk
     ∀[A:Type]
       (A ~ ℕk
       ⇒ (∀[E:A ⟶ A ⟶ ℙ]
             (EquivRel(A;x,y.E[x;y])
             ⇒ (∀x,y:A.  Dec(E[x;y]))
             ⇒ (∃L:A List. ((∀a,b∈L.  ¬E[a;b]) ∧ (∀a:A. (∃b∈L. E[a;b])) ∧ (||L|| ≤ k))))))
3. [A] : Type
4. A ~ ℕk
5. [E] : A ⟶ A ⟶ ℙ
6. EquivRel(A;x,y.E[x;y])
7. ∀x,y:A.  Dec(E[x;y])
8. ¬(k = 0 ∈ ℤ)
9. b : A
10. i : ℕ
11. j : ℕ
12. k = (i + j) ∈ ℤ
13. {a:A| E[b;a]}  ~ ℕi
14. {a:A| ¬E[b;a]}  ~ ℕj
15. ¬(i = 0 ∈ ℤ)
16. L : {a:A| ¬E[b;a]}  List
17. (∀a,b∈L.  ¬E[a;b]) ∧ (∀a:{a:A| ¬E[b;a]} . (∃b∈L. E[a;b])) ∧ (||L|| ≤ j)
⊢ ||[b / L]|| ≤ k

---

Latex:

---

Latex:

1.  k  :  \mBbbN{}
2.  \mforall{}k:\mBbbN{}k
          \mforall{}[A:Type]
              (A  \msim{}  \mBbbN{}k
              {}\mRightarrow{}  (\mforall{}[E:A  {}\mrightarrow{}  A  {}\mrightarrow{}  \mBbbP{}]
                          (EquivRel(A;x,y.E[x;y])
                          {}\mRightarrow{}  (\mforall{}x,y:A.    Dec(E[x;y]))
                          {}\mRightarrow{}  (\mexists{}L:A  List.  ((\mforall{}a,b\mmember{}L.    \mneg{}E[a;b])  \mwedge{}  (\mforall{}a:A.  (\mexists{}b\mmember{}L.  E[a;b]))  \mwedge{}  (||L||  \mleq{}  k))))))
3.  [A]  :  Type
4.  A  \msim{}  \mBbbN{}k
5.  [E]  :  A  {}\mrightarrow{}  A  {}\mrightarrow{}  \mBbbP{}
6.  EquivRel(A;x,y.E[x;y])
7.  \mforall{}x,y:A.    Dec(E[x;y])
8.  \mneg{}(k  =  0)
9.  b  :  A
10.  i  :  \mBbbN{}
11.  j  :  \mBbbN{}
12.  k  =  (i  +  j)
13.  \{a:A|  E[b;a]\}    \msim{}  \mBbbN{}i
14.  \{a:A|  \mneg{}E[b;a]\}    \msim{}  \mBbbN{}j
15.  \mneg{}(i  =  0)
16.  L  :  \{a:A|  \mneg{}E[b;a]\}    List
17.  (\mforall{}a,b\mmember{}L.    \mneg{}E[a;b])  \mwedge{}  (\mforall{}a:\{a:A|  \mneg{}E[b;a]\}  .  (\mexists{}b\mmember{}L.  E[a;b]))  \mwedge{}  (||L||  \mleq{}  j)
\mvdash{}  (\mforall{}a:A.  (\mexists{}b\mmember{}[b  /  L].  E[a;b]))  \mwedge{}  (||[b  /  L]||  \mleq{}  k)


By

---

Latex:
D  0

---

Home Index