---

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

.....assertion..... 
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:ℝ| z ∈ [r0, r1)} . ∀t:{t:ℝ| t ∈ [z, r1]} . (g(f@t) < r)))
6. ∀i:ℕ||B||. ∃z:{z:ℝ| z ∈ [r0, r1)} . ∀t:{t:ℝ| (z ≤ t) ∧ (t ≤ r1)} . let g,r = B[i] in g(f@t) < r
7. Z : i:ℕ||B|| ⟶ {z:ℝ| z ∈ [r0, r1)} 
8. ∀i:ℕ||B||. ∀t:{t:ℝ| ((Z i) ≤ t) ∧ (t ≤ r1)} .  let g,r = B[i] in g(f@t) < r
⊢ ∃z:{z:ℝ| (r0 ≤ z) ∧ (z < r1)} . ∀i:ℕ||B||. ((Z i) ≤ z)
BY
{ (Thin (-1)
   THEN MoveToConcl (-1)
   THEN (GenConcl ⌜||B|| = k ∈ ℕ⌝⋅ THENA Auto)
   THEN All Thin
   THEN NatInd (-1)
   THEN Auto) }

1
1. Z : i:ℕ0 ⟶ {z:ℝ| z ∈ [r0, r1)} 
⊢ ∃z:{z:ℝ| (r0 ≤ z) ∧ (z < r1)} . ∀i:ℕ0. ((Z i) ≤ z)

2
1. k : ℤ
2. [%1] : 0 < k
3. ∀Z:i:ℕk - 1 ⟶ {z:ℝ| z ∈ [r0, r1)} . ∃z:{z:ℝ| (r0 ≤ z) ∧ (z < r1)} . ∀i:ℕk - 1. ((Z i) ≤ z)
4. Z : i:ℕk ⟶ {z:ℝ| z ∈ [r0, r1)} 
⊢ ∃z:{z:ℝ| (r0 ≤ z) ∧ (z < r1)} . ∀i:ℕk. ((Z i) ≤ z)

---

Latex:

---

Latex:
.....assertion..... 
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{}|  z  \mmember{}  [r0,  r1)\}  .  \mforall{}t:\{t:\mBbbR{}|  t  \mmember{}  [z,  r1]\}  .  (g(f@t)  <  r)))
6.  \mforall{}i:\mBbbN{}||B||.  \mexists{}z:\{z:\mBbbR{}|  z  \mmember{}  [r0,  r1)\}  .  \mforall{}t:\{t:\mBbbR{}|  (z  \mleq{}  t)  \mwedge{}  (t  \mleq{}  r1)\}  .  let  g,r  =  B[i]  in  g(f@t)  <  r
7.  Z  :  i:\mBbbN{}||B||  {}\mrightarrow{}  \{z:\mBbbR{}|  z  \mmember{}  [r0,  r1)\} 
8.  \mforall{}i:\mBbbN{}||B||.  \mforall{}t:\{t:\mBbbR{}|  ((Z  i)  \mleq{}  t)  \mwedge{}  (t  \mleq{}  r1)\}  .    let  g,r  =  B[i]  in  g(f@t)  <  r
\mvdash{}  \mexists{}z:\{z:\mBbbR{}|  (r0  \mleq{}  z)  \mwedge{}  (z  <  r1)\}  .  \mforall{}i:\mBbbN{}||B||.  ((Z  i)  \mleq{}  z)


By

---

Latex:
(Thin  (-1)
  THEN  MoveToConcl  (-1)
  THEN  (GenConcl  \mkleeneopen{}||B||  =  k\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  All  Thin
  THEN  NatInd  (-1)
  THEN  Auto)

---

Home Index