---

Step * of Lemma rv-between_functionality

∀n:ℕ. ∀a1,a2,b1,b2,c1,c2:ℝ^n.  (req-vec(n;a1;a2) ⇒ req-vec(n;b1;b2) ⇒ req-vec(n;c1;c2) ⇒ (a1-b1-c1 ⇐⇒ a2-b2-c2))
BY
{ (Auto THEN ParallelLast THEN ((RWO  "8 9 10" (-1) THEN Auto) ORELSE (RWO  "8< 9< 10<" (-1) THEN Auto))) }

---

Latex:

---

Latex:
\mforall{}n:\mBbbN{}.  \mforall{}a1,a2,b1,b2,c1,c2:\mBbbR{}\^{}n.
    (req-vec(n;a1;a2)  {}\mRightarrow{}  req-vec(n;b1;b2)  {}\mRightarrow{}  req-vec(n;c1;c2)  {}\mRightarrow{}  (a1-b1-c1  \mLeftarrow{}{}\mRightarrow{}  a2-b2-c2))


By

---

Latex:
(Auto
  THEN  ParallelLast
  THEN  ((RWO    "8  9  10"  (-1)  THEN  Auto)  ORELSE  (RWO    "8<  9<  10<"  (-1)  THEN  Auto)))

---

Home Index