---

Step * 1 1 of Lemma unbounded-decidable-nset-infinite

.....assertion..... 
1. K : Type
2. K ⊆r ℕ
3. ∀l:ℕ. ((l ∈ K) ∨ (¬(l ∈ K)))
4. ∀B:ℕ. ∃k:K. B < k
5. d : ℕ ⟶ 𝔹
6. ∀l:ℕ. (l ∈ K ⇐⇒ ↑(d l))
7. λk.||filter(d;upto(k))|| ∈ K ⟶ ℕ
⊢ ∀n:ℤ. ∃k:K. (n < k ∧ (∀j:ℕ. (n < j ⇒ (j ∈ K) ⇒ (k ≤ j))))
BY
{ Assert ⌜∀n:ℕ. ∃k:K. ((n ≤ k) ∧ (∀j:ℕ. ((n ≤ j) ⇒ (j ∈ K) ⇒ (k ≤ j))))⌝⋅ }

1
.....assertion..... 
1. K : Type
2. K ⊆r ℕ
3. ∀l:ℕ. ((l ∈ K) ∨ (¬(l ∈ K)))
4. ∀B:ℕ. ∃k:K. B < k
5. d : ℕ ⟶ 𝔹
6. ∀l:ℕ. (l ∈ K ⇐⇒ ↑(d l))
7. λk.||filter(d;upto(k))|| ∈ K ⟶ ℕ
⊢ ∀n:ℕ. ∃k:K. ((n ≤ k) ∧ (∀j:ℕ. ((n ≤ j) ⇒ (j ∈ K) ⇒ (k ≤ j))))

2
1. K : Type
2. K ⊆r ℕ
3. ∀l:ℕ. ((l ∈ K) ∨ (¬(l ∈ K)))
4. ∀B:ℕ. ∃k:K. B < k
5. d : ℕ ⟶ 𝔹
6. ∀l:ℕ. (l ∈ K ⇐⇒ ↑(d l))
7. λk.||filter(d;upto(k))|| ∈ K ⟶ ℕ
8. ∀n:ℕ. ∃k:K. ((n ≤ k) ∧ (∀j:ℕ. ((n ≤ j) ⇒ (j ∈ K) ⇒ (k ≤ j))))
⊢ ∀n:ℤ. ∃k:K. (n < k ∧ (∀j:ℕ. (n < j ⇒ (j ∈ K) ⇒ (k ≤ j))))

---

Latex:

---

Latex:
.....assertion..... 
1.  K  :  Type
2.  K  \msubseteq{}r  \mBbbN{}
3.  \mforall{}l:\mBbbN{}.  ((l  \mmember{}  K)  \mvee{}  (\mneg{}(l  \mmember{}  K)))
4.  \mforall{}B:\mBbbN{}.  \mexists{}k:K.  B  <  k
5.  d  :  \mBbbN{}  {}\mrightarrow{}  \mBbbB{}
6.  \mforall{}l:\mBbbN{}.  (l  \mmember{}  K  \mLeftarrow{}{}\mRightarrow{}  \muparrow{}(d  l))
7.  \mlambda{}k.||filter(d;upto(k))||  \mmember{}  K  {}\mrightarrow{}  \mBbbN{}
\mvdash{}  \mforall{}n:\mBbbZ{}.  \mexists{}k:K.  (n  <  k  \mwedge{}  (\mforall{}j:\mBbbN{}.  (n  <  j  {}\mRightarrow{}  (j  \mmember{}  K)  {}\mRightarrow{}  (k  \mleq{}  j))))


By

---

Latex:
Assert  \mkleeneopen{}\mforall{}n:\mBbbN{}.  \mexists{}k:K.  ((n  \mleq{}  k)  \mwedge{}  (\mforall{}j:\mBbbN{}.  ((n  \mleq{}  j)  {}\mRightarrow{}  (j  \mmember{}  K)  {}\mRightarrow{}  (k  \mleq{}  j))))\mkleeneclose{}\mcdot{}

---

Home Index