---

Step * of Lemma finite-quotient-bound

∀A:Type. ∀R:A ⟶ A ⟶ ℙ. ∀n:ℕ.
  (A ~ ℕn ⇒ EquivRel(A;x,y.x R y) ⇒ (∀x,y:A.  Dec(x R y)) ⇒ (∃m:ℕ. ((m ≤ n) ∧ x,y:A//(x R y) ~ ℕm)))
BY
{ (Auto
   THEN (InstLemma `finite-quotient` [⌜A⌝;⌜R⌝]⋅ THENA (Auto THEN D 0 With ⌜n⌝  THEN Auto))
   THEN D -1
   THEN RenameVar `m' (-2)
   THEN D 0 With ⌜m⌝ 
   THEN Auto) }

1
1. A : Type
2. R : A ⟶ A ⟶ ℙ
3. n : ℕ
4. A ~ ℕn
5. EquivRel(A;x,y.x R y)
6. ∀x,y:A.  Dec(x R y)
7. m : ℕ
8. x,y:A//(x R y) ~ ℕm
⊢ m ≤ n

---

Latex:

---

Latex:
\mforall{}A:Type.  \mforall{}R:A  {}\mrightarrow{}  A  {}\mrightarrow{}  \mBbbP{}.  \mforall{}n:\mBbbN{}.
    (A  \msim{}  \mBbbN{}n
    {}\mRightarrow{}  EquivRel(A;x,y.x  R  y)
    {}\mRightarrow{}  (\mforall{}x,y:A.    Dec(x  R  y))
    {}\mRightarrow{}  (\mexists{}m:\mBbbN{}.  ((m  \mleq{}  n)  \mwedge{}  x,y:A//(x  R  y)  \msim{}  \mBbbN{}m)))


By

---

Latex:
(Auto
  THEN  (InstLemma  `finite-quotient`  [\mkleeneopen{}A\mkleeneclose{};\mkleeneopen{}R\mkleeneclose{}]\mcdot{}  THENA  (Auto  THEN  D  0  With  \mkleeneopen{}n\mkleeneclose{}    THEN  Auto))
  THEN  D  -1
  THEN  RenameVar  `m'  (-2)
  THEN  D  0  With  \mkleeneopen{}m\mkleeneclose{} 
  THEN  Auto)

---

Home Index