---

Step * of Lemma count-quotient

∀k:ℕ
  ∀[A:Type]
    (A ~ ℕk
    ⇒ (∀[E:A ⟶ A ⟶ ℙ]. (EquivRel(A;x,y.E[x;y]) ⇒ (∀x,y:A.  Dec(E[x;y])) ⇒ (∃j:ℕ. ((j ≤ k) ∧ x,y:A//E[x;y] ~ ℕj)))))
BY
{ (InstLemma `distinct-representatives` []
   THEN (RepeatFor 2 ((ParallelLast' THENA Auto))⋅
         THEN (D 0 THENA Auto)
         THEN (D -2 THENA Auto)
         THEN RepeatFor 3 ((ParallelLast' THENA Auto))⋅)
   THEN ExRepD
   THEN InstLemma `equipollent-distinct-representatives` [⌜A⌝;⌜E⌝;⌜L⌝]⋅
   THEN Auto
   THEN InstConcl [⌜||L||⌝]⋅
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}k:\mBbbN{}
    \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{}j:\mBbbN{}.  ((j  \mleq{}  k)  \mwedge{}  x,y:A//E[x;y]  \msim{}  \mBbbN{}j)))))


By

---

Latex:
(InstLemma  `distinct-representatives`  []
  THEN  (RepeatFor  2  ((ParallelLast'  THENA  Auto))\mcdot{}
              THEN  (D  0  THENA  Auto)
              THEN  (D  -2  THENA  Auto)
              THEN  RepeatFor  3  ((ParallelLast'  THENA  Auto))\mcdot{})
  THEN  ExRepD
  THEN  InstLemma  `equipollent-distinct-representatives`  [\mkleeneopen{}A\mkleeneclose{};\mkleeneopen{}E\mkleeneclose{};\mkleeneopen{}L\mkleeneclose{}]\mcdot{}
  THEN  Auto
  THEN  InstConcl  [\mkleeneopen{}||L||\mkleeneclose{}]\mcdot{}
  THEN  Auto)

---

Home Index