---

Step * of Lemma ip-triangle-permute

No Annotations
∀rv:InnerProductSpace. ∀a,b,c:Point(rv).  (Δ(a;b;c) ⇒ Δ(c;a;b))
BY
{ (Auto THEN ParallelLast THEN (FLemma `ip-triangle-permute-lemma` [-1] THENA Auto)) }

1
1. rv : InnerProductSpace
2. a : Point(rv)
3. b : Point(rv)
4. c : Point(rv)
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:
No  Annotations
\mforall{}rv:InnerProductSpace.  \mforall{}a,b,c:Point(rv).    (\mDelta{}(a;b;c)  {}\mRightarrow{}  \mDelta{}(c;a;b))


By

---

Latex:
(Auto  THEN  ParallelLast  THEN  (FLemma  `ip-triangle-permute-lemma`  [-1]  THENA  Auto))

---

Home Index