---

Step * of Lemma unbounded-decidable-nset-infinite

∀K:Type. ((K ⊆r ℕ) ⇒ (∀l:ℕ. ((l ∈ K) ∨ (¬(l ∈ K)))) ⇒ (∀B:ℕ. ∃k:K. B < k) ⇒ (∃f:K ⟶ ℕ. Surj(K;ℕ;f)))
BY
{ (Auto
   THEN (Assert ∃d:ℕ ⟶ 𝔹. ∀l:ℕ. (l ∈ K ⇐⇒ ↑(d l)) BY
               (RenameVar `d' (-2)
                THEN (D 0 With ⌜λn.isl(d n)⌝  THENW Auto)
                THEN (D 0 THENA Auto)
                THEN Reduce 0
                THEN (GenConclTerm ⌜d l⌝⋅ THENA Auto)
                THEN D -2
                THEN Reduce 0
                THEN Auto))
   THEN D -1
   THEN (Assert λk.||filter(d;upto(k))|| ∈ K ⟶ ℕ BY
               Auto)
   THEN D 0 With ⌜λk.||filter(d;upto(k))||⌝ 
   THEN Auto) }

1
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 ⟶ ℕ
⊢ Surj(K;ℕ;λk.||filter(d;upto(k))||)

---

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{}.  \mexists{}k:K.  B  <  k)  {}\mRightarrow{}  (\mexists{}f:K  {}\mrightarrow{}  \mBbbN{}.  Surj(K;\mBbbN{};f)))


By

---

Latex:
(Auto
  THEN  (Assert  \mexists{}d:\mBbbN{}  {}\mrightarrow{}  \mBbbB{}.  \mforall{}l:\mBbbN{}.  (l  \mmember{}  K  \mLeftarrow{}{}\mRightarrow{}  \muparrow{}(d  l))  BY
                          (RenameVar  `d'  (-2)
                            THEN  (D  0  With  \mkleeneopen{}\mlambda{}n.isl(d  n)\mkleeneclose{}    THENW  Auto)
                            THEN  (D  0  THENA  Auto)
                            THEN  Reduce  0
                            THEN  (GenConclTerm  \mkleeneopen{}d  l\mkleeneclose{}\mcdot{}  THENA  Auto)
                            THEN  D  -2
                            THEN  Reduce  0
                            THEN  Auto))
  THEN  D  -1
  THEN  (Assert  \mlambda{}k.||filter(d;upto(k))||  \mmember{}  K  {}\mrightarrow{}  \mBbbN{}  BY
                          Auto)
  THEN  D  0  With  \mkleeneopen{}\mlambda{}k.||filter(d;upto(k))||\mkleeneclose{} 
  THEN  Auto)

---

Home Index