---

Step * 1 of Lemma rexp-unique


1. f : ℝ ⟶ ℝ
2. ∀x,y:ℝ.  ((x = y) ⇒ (f[x] = f[y]))
3. f[r0] = r1
4. d(f[x])/dx = λx.f[x] on (-∞, ∞)
5. x : ℝ
6. m : ℕ
⊢ ∃c:ℝ. ∃N:ℕ. ∀k:{N...}. ∀x:{x:ℝ| |x| ≤ r(m)} .  (|f[x]| ≤ c)
BY
{ ((D 0 With ⌜||f[x]||_x:[r(-m), r(m)]⌝  THENA Auto)
   THEN D 0 With ⌜0⌝ 
   THEN Auto
   THEN InstLemma `I-norm-bound` [⌜[r(-m), r(m)]⌝;⌜f⌝;⌜x1⌝]  ⋅
   THEN Auto
   THEN D -1
   THEN RWO "rabs-rleq-iff" (-1)
   THEN Auto) }

---

Latex:

---

Latex:

1.  f  :  \mBbbR{}  {}\mrightarrow{}  \mBbbR{}
2.  \mforall{}x,y:\mBbbR{}.    ((x  =  y)  {}\mRightarrow{}  (f[x]  =  f[y]))
3.  f[r0]  =  r1
4.  d(f[x])/dx  =  \mlambda{}x.f[x]  on  (-\minfty{},  \minfty{})
5.  x  :  \mBbbR{}
6.  m  :  \mBbbN{}
\mvdash{}  \mexists{}c:\mBbbR{}.  \mexists{}N:\mBbbN{}.  \mforall{}k:\{N...\}.  \mforall{}x:\{x:\mBbbR{}|  |x|  \mleq{}  r(m)\}  .    (|f[x]|  \mleq{}  c)


By

---

Latex:
((D  0  With  \mkleeneopen{}||f[x]||\_x:[r(-m),  r(m)]\mkleeneclose{}    THENA  Auto)
  THEN  D  0  With  \mkleeneopen{}0\mkleeneclose{} 
  THEN  Auto
  THEN  InstLemma  `I-norm-bound`  [\mkleeneopen{}[r(-m),  r(m)]\mkleeneclose{};\mkleeneopen{}f\mkleeneclose{};\mkleeneopen{}x1\mkleeneclose{}]    \mcdot{}
  THEN  Auto
  THEN  D  -1
  THEN  RWO  "rabs-rleq-iff"  (-1)
  THEN  Auto)

---

Home Index