---

Step * 1 1 1 of Lemma path-end-mem-basic


1. X : SeparationSpace
2. f : Point(Path(X))
3. B : ss-basic(X)
4. f@r1 ∈ B
5. g : Point(X ⟶ ℝ)
6. r : ℝ
7. g(f@r1) < r
8. k : ℕ+
9. (r1/r(k)) < (r - g(f@r1))
10. d : {d:ℝ| r0 < d} 
11. ∀x,y:{x:ℝ| (r0 ≤ x) ∧ (x ≤ r1)} .  ((|x - y| ≤ d) ⇒ (|g(f@x) - g(f@y)| ≤ (r1/r(k))))
12. t : {t:ℝ| t ∈ [rmax(r0;r1 - d), r1]} 
13. t ∈ {x:ℝ| (r0 ≤ x) ∧ (x ≤ r1)} 
14. |t - r1| ≤ d
⊢ g(f@t) < r
BY
{ ((InstHyp [⌜t⌝;⌜r1⌝] (-4)⋅ THENA Auto)
   THEN RWO "rabs-difference-bound-rleq" (-1)
   THEN Auto
   THEN RWO "-1" 0
   THEN Auto) }

---

Latex:

---

Latex:

1.  X  :  SeparationSpace
2.  f  :  Point(Path(X))
3.  B  :  ss-basic(X)
4.  f@r1  \mmember{}  B
5.  g  :  Point(X  {}\mrightarrow{}  \mBbbR{})
6.  r  :  \mBbbR{}
7.  g(f@r1)  <  r
8.  k  :  \mBbbN{}\msupplus{}
9.  (r1/r(k))  <  (r  -  g(f@r1))
10.  d  :  \{d:\mBbbR{}|  r0  <  d\} 
11.  \mforall{}x,y:\{x:\mBbbR{}|  (r0  \mleq{}  x)  \mwedge{}  (x  \mleq{}  r1)\}  .    ((|x  -  y|  \mleq{}  d)  {}\mRightarrow{}  (|g(f@x)  -  g(f@y)|  \mleq{}  (r1/r(k))))
12.  t  :  \{t:\mBbbR{}|  t  \mmember{}  [rmax(r0;r1  -  d),  r1]\} 
13.  t  \mmember{}  \{x:\mBbbR{}|  (r0  \mleq{}  x)  \mwedge{}  (x  \mleq{}  r1)\} 
14.  |t  -  r1|  \mleq{}  d
\mvdash{}  g(f@t)  <  r


By

---

Latex:
((InstHyp  [\mkleeneopen{}t\mkleeneclose{};\mkleeneopen{}r1\mkleeneclose{}]  (-4)\mcdot{}  THENA  Auto)
  THEN  RWO  "rabs-difference-bound-rleq"  (-1)
  THEN  Auto
  THEN  RWO  "-1"  0
  THEN  Auto)

---

Home Index