---

Step * of Lemma pseudo-bounded-is-bounded

∀[S:{S:Type| S ⊆r ℕ} ]. ∀m:S. (pseudo-bounded(S) ⇒ ⇃(∃B:ℕ. ∀n:S. (n ≤ B)))
BY
{ ((Auto THEN (Assert S ⊆r ℕ BY (Unhide THEN Auto)) THEN PromoteHyp (-1) 2)
   THEN (Unfold `pseudo-bounded` -1 THEN (Skolemize (-1) `F' THENA Auto))
   THEN (InstLemma `weak-continuity-truncated` [⌜S⌝;⌜F⌝]⋅
         THENA (Auto THEN DSetVars THEN MemTypeCD THEN Auto THEN D 0 THEN Auto THEN UseWitness ⌜m⌝⋅ THEN Auto)
         )
   THEN ParallelLast
   THEN Auto) }

1
1. [S] : {S:Type| S ⊆r ℕ} 
2. S ⊆r ℕ
3. m : S
4. ∀f:ℕ ⟶ S. ∃k:ℕ. ∀n:{k...}. f n < n
5. F : f:(ℕ ⟶ S) ⟶ ℕ
6. ∀f:ℕ ⟶ S. ∀n:{F f...}.  f n < n
7. ∀f:ℕ ⟶ S. ∃n:ℕ. ∀g:ℕ ⟶ S. ((f = g ∈ (ℕn ⟶ S)) ⇒ ((F f) = (F g) ∈ ℕ))
⊢ ∃B:ℕ. ∀n:S. (n ≤ B)

---

Latex:

---

Latex:
\mforall{}[S:\{S:Type|  S  \msubseteq{}r  \mBbbN{}\}  ].  \mforall{}m:S.  (pseudo-bounded(S)  {}\mRightarrow{}  \00D9(\mexists{}B:\mBbbN{}.  \mforall{}n:S.  (n  \mleq{}  B)))


By

---

Latex:
((Auto  THEN  (Assert  S  \msubseteq{}r  \mBbbN{}  BY  (Unhide  THEN  Auto))  THEN  PromoteHyp  (-1)  2)
  THEN  (Unfold  `pseudo-bounded`  -1  THEN  (Skolemize  (-1)  `F'  THENA  Auto))
  THEN  (InstLemma  `weak-continuity-truncated`  [\mkleeneopen{}S\mkleeneclose{};\mkleeneopen{}F\mkleeneclose{}]\mcdot{}
              THENA  (Auto
                            THEN  DSetVars
                            THEN  MemTypeCD
                            THEN  Auto
                            THEN  D  0
                            THEN  Auto
                            THEN  UseWitness  \mkleeneopen{}m\mkleeneclose{}\mcdot{}
                            THEN  Auto)
              )
  THEN  ParallelLast
  THEN  Auto)

---

Home Index