---

Step * of Lemma quotient-equipollent-nat

∀[A:Type]. ∀[k:ℕ].
  (finite-type(A)
  ⇒ (∀E:A ⟶ A ⟶ ℙ. x,y:A//E[x;y] ~ ℕk ⇐⇒ A ~ ℕk mod (a1,a2.E[a1;a2]) supposing EquivRel(A;x,y.E[x;y])))
BY
{ ((UnivCD THENA Auto) THEN RWO "quotient-equipollent" 0⋅ THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[A:Type].  \mforall{}[k:\mBbbN{}].
    (finite-type(A)
    {}\mRightarrow{}  (\mforall{}E:A  {}\mrightarrow{}  A  {}\mrightarrow{}  \mBbbP{}
                x,y:A//E[x;y]  \msim{}  \mBbbN{}k  \mLeftarrow{}{}\mRightarrow{}  A  \msim{}  \mBbbN{}k  mod  (a1,a2.E[a1;a2])  supposing  EquivRel(A;x,y.E[x;y])))


By

---

Latex:
((UnivCD  THENA  Auto)  THEN  RWO  "quotient-equipollent"  0\mcdot{}  THEN  Auto)

---

Home Index