---

Step * of Lemma bounded-ccc-nset-finite

∀K:Type. (CCCNSet(K) ⇒ (∀B:ℕ. ((∀k:K. (k ≤ B)) ⇒ finite(K))))
BY
{ (InstLemma `bounded-ccc-nset-decidable` []
   THEN RepeatFor 2 ((ParallelLast' THENA Auto))
   THEN D 2
   THEN RepeatFor 2 ((ParallelLast' THENA Auto))
   THEN InstLemma `bounded-decidable-nset-finite` [⌜K⌝;⌜B⌝]⋅
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}K:Type.  (CCCNSet(K)  {}\mRightarrow{}  (\mforall{}B:\mBbbN{}.  ((\mforall{}k:K.  (k  \mleq{}  B))  {}\mRightarrow{}  finite(K))))


By

---

Latex:
(InstLemma  `bounded-ccc-nset-decidable`  []
  THEN  RepeatFor  2  ((ParallelLast'  THENA  Auto))
  THEN  D  2
  THEN  RepeatFor  2  ((ParallelLast'  THENA  Auto))
  THEN  InstLemma  `bounded-decidable-nset-finite`  [\mkleeneopen{}K\mkleeneclose{};\mkleeneopen{}B\mkleeneclose{}]\mcdot{}
  THEN  Auto)

---

Home Index