---

Step * 1 1 of Lemma ccc-nset-transparent

.....antecedent..... 
1. K : Type
2. K ⊆r ℕ
3. k0 : K
4. B : ℕ
⊢ ∀g:ℕ ⟶ K. ∃n:ℕ. ((n ∈ K) ∧ (B < n ∨ ((g n) ≤ B)))
BY
{ (Auto
   THEN ((Decide ⌜B < k0⌝⋅ THENA Auto)
         THENL [(D 0 With ⌜k0⌝  THEN Auto)
               ; ((Decide ⌜(g k0) ≤ B⌝⋅ THENA Auto) THENL [(D 0 With ⌜k0⌝  THEN Auto); (D 0 With ⌜g k0⌝  THEN Auto)])]
        )
   ) }

---

Latex:

---

Latex:
.....antecedent..... 
1.  K  :  Type
2.  K  \msubseteq{}r  \mBbbN{}
3.  k0  :  K
4.  B  :  \mBbbN{}
\mvdash{}  \mforall{}g:\mBbbN{}  {}\mrightarrow{}  K.  \mexists{}n:\mBbbN{}.  ((n  \mmember{}  K)  \mwedge{}  (B  <  n  \mvee{}  ((g  n)  \mleq{}  B)))


By

---

Latex:
(Auto
  THEN  ((Decide  \mkleeneopen{}B  <  k0\mkleeneclose{}\mcdot{}  THENA  Auto)
              THENL  [(D  0  With  \mkleeneopen{}k0\mkleeneclose{}    THEN  Auto)
                          ;  ((Decide  \mkleeneopen{}(g  k0)  \mleq{}  B\mkleeneclose{}\mcdot{}  THENA  Auto)
                                THENL  [(D  0  With  \mkleeneopen{}k0\mkleeneclose{}    THEN  Auto);  (D  0  With  \mkleeneopen{}g  k0\mkleeneclose{}    THEN  Auto)]
                          )]
            )
  )

---

Home Index