---

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


1. X : SeparationSpace
2. f : Point(Path(X))
3. B : (Point(X ⟶ ℝ) × ℝ) List
4. ∀i:ℕ||B||. let f@0,r = B[i] in f@0(f@r1) < r
5. ∀g:Point(X ⟶ ℝ). ∀r:ℝ.
     ((g(f@r1) < r) ⇒ (∃z:{z:ℝ| (r0 ≤ z) ∧ (z < r1)} . ∀t:{t:ℝ| (z ≤ t) ∧ (t ≤ r1)} . (g(f@t) < r)))
6. Z1 : i:ℕ||B|| ⟶ {z:ℝ| (r0 ≤ z) ∧ (z < r1)} 
7. i : ℕ||B||
8. t : ℝ
9. (Z1 i) ≤ t
10. t ≤ r1
11. g : Point(X ⟶ ℝ)
12. r : ℝ
13. B[i] = <g, r> ∈ (Point(X ⟶ ℝ) × ℝ)
⊢ r0 ≤ t
BY
{ (MoveToConcl (-5) THEN (GenConclTerm ⌜Z1 i⌝⋅ THENA Auto) THEN D -2 THEN Auto) }

---

Latex:

---

Latex:

1.  X  :  SeparationSpace
2.  f  :  Point(Path(X))
3.  B  :  (Point(X  {}\mrightarrow{}  \mBbbR{})  \mtimes{}  \mBbbR{})  List
4.  \mforall{}i:\mBbbN{}||B||.  let  f@0,r  =  B[i]  in  f@0(f@r1)  <  r
5.  \mforall{}g:Point(X  {}\mrightarrow{}  \mBbbR{}).  \mforall{}r:\mBbbR{}.
          ((g(f@r1)  <  r)  {}\mRightarrow{}  (\mexists{}z:\{z:\mBbbR{}|  (r0  \mleq{}  z)  \mwedge{}  (z  <  r1)\}  .  \mforall{}t:\{t:\mBbbR{}|  (z  \mleq{}  t)  \mwedge{}  (t  \mleq{}  r1)\}  .  (g(f@t)  <  r))\000C)
6.  Z1  :  i:\mBbbN{}||B||  {}\mrightarrow{}  \{z:\mBbbR{}|  (r0  \mleq{}  z)  \mwedge{}  (z  <  r1)\} 
7.  i  :  \mBbbN{}||B||
8.  t  :  \mBbbR{}
9.  (Z1  i)  \mleq{}  t
10.  t  \mleq{}  r1
11.  g  :  Point(X  {}\mrightarrow{}  \mBbbR{})
12.  r  :  \mBbbR{}
13.  B[i]  =  <g,  r>
\mvdash{}  r0  \mleq{}  t


By

---

Latex:
(MoveToConcl  (-5)  THEN  (GenConclTerm  \mkleeneopen{}Z1  i\mkleeneclose{}\mcdot{}  THENA  Auto)  THEN  D  -2  THEN  Auto)

---

Home Index