---

Step * of Lemma bounded-decidable-nset-finite

∀K:Type. ((K ⊆r ℕ) ⇒ (∀l:ℕ. ((l ∈ K) ∨ (¬(l ∈ K)))) ⇒ (∀B:ℕ. ((∀k:K. (k ≤ B)) ⇒ finite(K))))
BY
{ (Auto THEN (RWO "finite-iff-listable" 0⋅ THENA Auto)) }

1
1. K : Type
2. K ⊆r ℕ
3. ∀l:ℕ. ((l ∈ K) ∨ (¬(l ∈ K)))
4. B : ℕ
5. ∀k:K. (k ≤ B)
⊢ ∃L:K List. (no_repeats(K;L) ∧ (∀x:K. (x ∈ L)))

---

Latex:

---

Latex:
\mforall{}K:Type.  ((K  \msubseteq{}r  \mBbbN{})  {}\mRightarrow{}  (\mforall{}l:\mBbbN{}.  ((l  \mmember{}  K)  \mvee{}  (\mneg{}(l  \mmember{}  K))))  {}\mRightarrow{}  (\mforall{}B:\mBbbN{}.  ((\mforall{}k:K.  (k  \mleq{}  B))  {}\mRightarrow{}  finite(K))))


By

---

Latex:
(Auto  THEN  (RWO  "finite-iff-listable"  0\mcdot{}  THENA  Auto))

---

Home Index