---

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

.....assertion..... 
1. X : SeparationSpace
2. f : Point(Path(X))
3. B : ss-basic(X)
4. f@r1 ∈ B
⊢ ∀g:Point(X ⟶ ℝ). ∀r:ℝ.  ((g(f@r1) < r) ⇒ (∃z:{z:ℝ| z ∈ [r0, r1)} . ∀t:{t:ℝ| t ∈ [z, r1]} . (g(f@t) < r)))
BY
{ (Auto
   THEN (Assert real-cont(λt.g(f@t);r0;r1) BY
               ((BLemma `real-fun-iff-continuous` THEN Try (Unfold `rfun` 0))
                THEN Auto
                THEN (D 0 THEN Auto)
                THEN Reduce 0
                THEN (Assert g(f@x) ≡ g(f@y) BY
                            (RWO "-1" 0 THEN Auto))
                THEN RWO "real-ss-eq" (-1)
                THEN Auto))
   THEN (InstLemma `small-reciprocal-real` [⌜r - g(f@r1)⌝]⋅ THENA Auto)
   THEN D -1
   THEN (D -3 With ⌜k⌝  THENA Auto)
   THEN D -1
   THEN D 0 With ⌜rmax(r0;r1 - d)⌝ 
   THEN Auto
   THEN Try (((DSetVars THEN All Reduce) THEN MemTypeCD THEN EAuto 1))
   THEN Reduce -2
   THEN (Assert t ∈ {x:ℝ| (r0 ≤ x) ∧ (x ≤ r1)}  BY
               ((DSetVars THEN All Reduce) THEN MemTypeCD THEN EAuto 1 THEN RWO "rmax_lb<" (-2) THEN Auto))
   THEN (Assert |t - r1| ≤ d BY
               (Thin (-1)
                THEN (DSetVars THEN (Unhide THENA Auto) THEN Reduce -1)
                THEN (RWO "rmax_lb<" (-1) THEN Auto)
                THEN BLemma `rabs-difference-bound-rleq`
                THEN Auto
                THEN RWO "-2" 0
                THEN Auto))) }

1
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

---

Latex:

---

Latex:
.....assertion..... 
1.  X  :  SeparationSpace
2.  f  :  Point(Path(X))
3.  B  :  ss-basic(X)
4.  f@r1  \mmember{}  B
\mvdash{}  \mforall{}g:Point(X  {}\mrightarrow{}  \mBbbR{}).  \mforall{}r:\mBbbR{}.
        ((g(f@r1)  <  r)  {}\mRightarrow{}  (\mexists{}z:\{z:\mBbbR{}|  z  \mmember{}  [r0,  r1)\}  .  \mforall{}t:\{t:\mBbbR{}|  t  \mmember{}  [z,  r1]\}  .  (g(f@t)  <  r)))


By

---

Latex:
(Auto
  THEN  (Assert  real-cont(\mlambda{}t.g(f@t);r0;r1)  BY
                          ((BLemma  `real-fun-iff-continuous`  THEN  Try  (Unfold  `rfun`  0))
                            THEN  Auto
                            THEN  (D  0  THEN  Auto)
                            THEN  Reduce  0
                            THEN  (Assert  g(f@x)  \mequiv{}  g(f@y)  BY
                                                    (RWO  "-1"  0  THEN  Auto))
                            THEN  RWO  "real-ss-eq"  (-1)
                            THEN  Auto))
  THEN  (InstLemma  `small-reciprocal-real`  [\mkleeneopen{}r  -  g(f@r1)\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  D  -1
  THEN  (D  -3  With  \mkleeneopen{}k\mkleeneclose{}    THENA  Auto)
  THEN  D  -1
  THEN  D  0  With  \mkleeneopen{}rmax(r0;r1  -  d)\mkleeneclose{} 
  THEN  Auto
  THEN  Try  (((DSetVars  THEN  All  Reduce)  THEN  MemTypeCD  THEN  EAuto  1))
  THEN  Reduce  -2
  THEN  (Assert  t  \mmember{}  \{x:\mBbbR{}|  (r0  \mleq{}  x)  \mwedge{}  (x  \mleq{}  r1)\}    BY
                          ((DSetVars  THEN  All  Reduce)
                            THEN  MemTypeCD
                            THEN  EAuto  1
                            THEN  RWO  "rmax\_lb<"  (-2)
                            THEN  Auto))
  THEN  (Assert  |t  -  r1|  \mleq{}  d  BY
                          (Thin  (-1)
                            THEN  (DSetVars  THEN  (Unhide  THENA  Auto)  THEN  Reduce  -1)
                            THEN  (RWO  "rmax\_lb<"  (-1)  THEN  Auto)
                            THEN  BLemma  `rabs-difference-bound-rleq`
                            THEN  Auto
                            THEN  RWO  "-2"  0
                            THEN  Auto)))

---

Home Index