---

Step * of Lemma rv-pos-angle-permute

∀n:ℕ. ∀a,b,c:ℝ^n.  (rv-pos-angle(n;a;b;c) ⇒ rv-pos-angle(n;c;a;b))
BY
{ (Auto THEN ParallelLast THEN (FLemma `rv-pos-angle-permute-lemma` [-1] THENA Auto)) }

1
1. n : ℕ
2. a : ℝ^n
3. b : ℝ^n
4. c : ℝ^n
5. |a - b⋅c - b| < (||a - b|| * ||c - b||)
6. |a - b⋅c - b - a - b| < (||a - b|| * ||c - b - a - b||)
⊢ |c - a⋅b - a| < (||c - a|| * ||b - a||)

---

Latex:

---

Latex:
\mforall{}n:\mBbbN{}.  \mforall{}a,b,c:\mBbbR{}\^{}n.    (rv-pos-angle(n;a;b;c)  {}\mRightarrow{}  rv-pos-angle(n;c;a;b))


By

---

Latex:
(Auto  THEN  ParallelLast  THEN  (FLemma  `rv-pos-angle-permute-lemma`  [-1]  THENA  Auto))

---

Home Index