---

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


1. K : Type
2. K ⊆r ℕ
3. ∀l:ℕ. ((l ∈ K) ∨ (¬(l ∈ K)))
4. d : ℕ ⟶ 𝔹
5. ∀l:ℕ. (l ∈ K ⇐⇒ ↑(d l))
6. λk.||filter(d;upto(k))|| ∈ K ⟶ ℕ
7. n : ℕ
8. k : K
9. n < k
⊢ ∃k:K. ((n ≤ k) ∧ (∀j:ℕ. ((n ≤ j) ⇒ (j ∈ K) ⇒ (k ≤ j))))
BY
{ ((Assert ⌜∀D,n:ℕ. ∀k:K.  (n < k ⇒ (k ≤ (n + D)) ⇒ (∃k:K. ((n ≤ k) ∧ (∀j:ℕ. ((n ≤ j) ⇒ (j ∈ K) ⇒ (k ≤ j))))))⌝⋅
   THENM (InstHyp [⌜k - n⌝;⌜n⌝;⌜k⌝] (-1)⋅ THEN Auto)
   )
   THEN RepeatFor 6 (Thin (-1))
   THEN InductionOnNat
   THEN Auto) }

1
1. K : Type
2. K ⊆r ℕ
3. ∀l:ℕ. ((l ∈ K) ∨ (¬(l ∈ K)))
4. D : ℤ
5. [%3] : 0 < D
6. ∀n:ℕ. ∀k:K.  (n < k ⇒ (k ≤ (n + (D - 1))) ⇒ (∃k:K. ((n ≤ k) ∧ (∀j:ℕ. ((n ≤ j) ⇒ (j ∈ K) ⇒ (k ≤ j))))))
7. n : ℕ
8. k : K
9. n < k
10. k ≤ (n + D)
⊢ ∃k:K. ((n ≤ k) ∧ (∀j:ℕ. ((n ≤ j) ⇒ (j ∈ K) ⇒ (k ≤ j))))

---

Latex:

---

Latex:

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


By

---

Latex:
((Assert  \mkleeneopen{}\mforall{}D,n:\mBbbN{}.  \mforall{}k:K.
                        (n  <  k  {}\mRightarrow{}  (k  \mleq{}  (n  +  D))  {}\mRightarrow{}  (\mexists{}k:K.  ((n  \mleq{}  k)  \mwedge{}  (\mforall{}j:\mBbbN{}.  ((n  \mleq{}  j)  {}\mRightarrow{}  (j  \mmember{}  K)  {}\mRightarrow{}  (k  \mleq{}  j))))))\mkleeneclose{}
    \mcdot{}
  THENM  (InstHyp  [\mkleeneopen{}k  -  n\mkleeneclose{};\mkleeneopen{}n\mkleeneclose{};\mkleeneopen{}k\mkleeneclose{}]  (-1)\mcdot{}  THEN  Auto)
  )
  THEN  RepeatFor  6  (Thin  (-1))
  THEN  InductionOnNat
  THEN  Auto)

---

Home Index