---

Step * of Lemma equipollent-distinct-representatives

∀[A:Type]. ∀[E:A ⟶ A ⟶ ℙ].
  (EquivRel(A;x,y.E[x;y]) ⇒ (∀L:A List. (∀a:A. (∃b∈L. E[a;b])) ⇒ x,y:A//E[x;y] ~ ℕ||L|| supposing (∀a,b∈L.  ¬E[a;b])))
BY
{ 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. (∃b∈L. E[a;b])
⊢ x,y:A//E[x;y] ~ ℕ||L||

---

Latex:

---

Latex:
\mforall{}[A:Type].  \mforall{}[E:A  {}\mrightarrow{}  A  {}\mrightarrow{}  \mBbbP{}].
    (EquivRel(A;x,y.E[x;y])
    {}\mRightarrow{}  (\mforall{}L:A  List.  (\mforall{}a:A.  (\mexists{}b\mmember{}L.  E[a;b]))  {}\mRightarrow{}  x,y:A//E[x;y]  \msim{}  \mBbbN{}||L||  supposing  (\mforall{}a,b\mmember{}L.    \mneg{}E[a;b])))


By

---

Latex:
Auto

---

Home Index