---

Step * of Lemma interval-to-int-bounded

No Annotations
∀a:ℝ. ∀b:{b:ℝ| a ≤ b} . ∀f:{x:ℝ| x ∈ [a, b]}  ⟶ ℤ.
  ∃B:ℕ. ∀x:{x:ℝ| x ∈ [a, b]} . ∃y:{x:ℝ| x ∈ [a, b]} . ((x = y) ∧ (|f y| ≤ B))
BY
{ (Auto
   THEN (InstLemma `mcompact-interval` [⌜a⌝;⌜b⌝]⋅ THENA Auto)
   THEN D -1
   THEN RenameVar `c' (-2)
   THEN RenameVar `mtb' (-1)
   THEN (InstLemma `compact-metric-to-int-bounded` [⌜{x:ℝ| x ∈ [a, b]} ⌝;⌜rmetric()⌝;⌜c⌝;⌜mtb⌝;⌜f⌝]⋅ THENA Auto)
   THEN RepeatFor 3 (ParallelLast)
   THEN RWO "rmetric-meq" (-1)
   THEN Auto) }

---

Latex:

---

Latex:
No  Annotations
\mforall{}a:\mBbbR{}.  \mforall{}b:\{b:\mBbbR{}|  a  \mleq{}  b\}  .  \mforall{}f:\{x:\mBbbR{}|  x  \mmember{}  [a,  b]\}    {}\mrightarrow{}  \mBbbZ{}.
    \mexists{}B:\mBbbN{}.  \mforall{}x:\{x:\mBbbR{}|  x  \mmember{}  [a,  b]\}  .  \mexists{}y:\{x:\mBbbR{}|  x  \mmember{}  [a,  b]\}  .  ((x  =  y)  \mwedge{}  (|f  y|  \mleq{}  B))


By

---

Latex:
(Auto
  THEN  (InstLemma  `mcompact-interval`  [\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  D  -1
  THEN  RenameVar  `c'  (-2)
  THEN  RenameVar  `mtb'  (-1)
  THEN  (InstLemma  `compact-metric-to-int-bounded`  [\mkleeneopen{}\{x:\mBbbR{}|  x  \mmember{}  [a,  b]\}  \mkleeneclose{};\mkleeneopen{}rmetric()\mkleeneclose{};\mkleeneopen{}c\mkleeneclose{};\mkleeneopen{}mtb\mkleeneclose{};\mkleeneopen{}f\mkleeneclose{}]\mcdot{}
              THENA  Auto
              )
  THEN  RepeatFor  3  (ParallelLast)
  THEN  RWO  "rmetric-meq"  (-1)
  THEN  Auto)

---

Home Index