---

Step * 1 of Lemma path-comp-rel_wf


1. X : SeparationSpace
2. f : Point(Path(X))
3. g : Point(Path(X))
4. h : Point(Path(X))
5. ∀t:{x:ℝ| (r0 ≤ x) ∧ (x ≤ (r1/r(2)))} . h@t ≡ f@r(2) * t
6. ∀x:ℝ. (((r1/r(2)) ≤ x) ∧ (x ≤ r1) ∈ Type)
7. t : ℝ@i
8. r1 ≤ (r(2) * t)
9. t ≤ r1
10. r0 ≤ ((r(2) * t) - r1)
⊢ ((r(2) * t) - r1) ≤ r1
BY
{ (nRMul ⌜r(2)⌝ (-2)⋅ THEN Auto) }

---

Latex:

---

Latex:

1.  X  :  SeparationSpace
2.  f  :  Point(Path(X))
3.  g  :  Point(Path(X))
4.  h  :  Point(Path(X))
5.  \mforall{}t:\{x:\mBbbR{}|  (r0  \mleq{}  x)  \mwedge{}  (x  \mleq{}  (r1/r(2)))\}  .  h@t  \mequiv{}  f@r(2)  *  t
6.  \mforall{}x:\mBbbR{}.  (((r1/r(2))  \mleq{}  x)  \mwedge{}  (x  \mleq{}  r1)  \mmember{}  Type)
7.  t  :  \mBbbR{}@i
8.  r1  \mleq{}  (r(2)  *  t)
9.  t  \mleq{}  r1
10.  r0  \mleq{}  ((r(2)  *  t)  -  r1)
\mvdash{}  ((r(2)  *  t)  -  r1)  \mleq{}  r1


By

---

Latex:
(nRMul  \mkleeneopen{}r(2)\mkleeneclose{}  (-2)\mcdot{}  THEN  Auto)

---

Home Index