---

Step * of Lemma path-end-mem-open

No Annotations
∀X:SeparationSpace. ∀f:Point(Path(X)). ∀O:Open(X).
  (f@r1 ∈ O ⇒ (∃z:{z:ℝ| z ∈ [r0, r1)} . ∀t:{t:ℝ| t ∈ [z, r1]} . f@t ∈ O))
BY
{ (Auto
   THEN RepUR ``ss-mem-open`` -1
   THEN ExRepD
   THEN (FLemma `path-end-mem-basic` [-1] THENA Auto)
   THEN ParallelLast
   THEN Try ((DSetVars THEN All Reduce THEN MemTypeCD THEN Auto))
   THEN ParallelLast
   THEN D 0 With ⌜B⌝ 
   THEN Auto
   THEN Try ((DSetVars THEN All Reduce THEN MemTypeCD THEN Auto))) }

---

Latex:

---

Latex:
No  Annotations
\mforall{}X:SeparationSpace.  \mforall{}f:Point(Path(X)).  \mforall{}O:Open(X).
    (f@r1  \mmember{}  O  {}\mRightarrow{}  (\mexists{}z:\{z:\mBbbR{}|  z  \mmember{}  [r0,  r1)\}  .  \mforall{}t:\{t:\mBbbR{}|  t  \mmember{}  [z,  r1]\}  .  f@t  \mmember{}  O))


By

---

Latex:
(Auto
  THEN  RepUR  ``ss-mem-open``  -1
  THEN  ExRepD
  THEN  (FLemma  `path-end-mem-basic`  [-1]  THENA  Auto)
  THEN  ParallelLast
  THEN  Try  ((DSetVars  THEN  All  Reduce  THEN  MemTypeCD  THEN  Auto))
  THEN  ParallelLast
  THEN  D  0  With  \mkleeneopen{}B\mkleeneclose{} 
  THEN  Auto
  THEN  Try  ((DSetVars  THEN  All  Reduce  THEN  MemTypeCD  THEN  Auto)))

---

Home Index