Step
*
of Lemma
r2-det-convex2
∀[p,q,r,t,s:ℝ^2]. ∀[a,b,c:ℝ].
|a*p + b*q + c*rts| = ((a * |pts|) + (b * |qts|) + (c * |rts|)) supposing ((a + b + c) = r1) ∧ r1 - a ≠ r0
BY
{ Auto }
1
1. p : ℝ^2
2. q : ℝ^2
3. r : ℝ^2
4. t : ℝ^2
5. s : ℝ^2
6. a : ℝ
7. b : ℝ
8. c : ℝ
9. (a + b + c) = r1
10. r1 - a ≠ r0
⊢ |a*p + b*q + c*rts| = ((a * |pts|) + (b * |qts|) + (c * |rts|))
Latex:
Latex:
\mforall{}[p,q,r,t,s:\mBbbR{}\^{}2]. \mforall{}[a,b,c:\mBbbR{}].
|a*p + b*q + c*rts| = ((a * |pts|) + (b * |qts|) + (c * |rts|))
supposing ((a + b + c) = r1) \mwedge{} r1 - a \mneq{} r0
By
Latex:
Auto
Home
Index