---

Step * of Lemma real-vec-angle-lemma2

∀n:ℕ. ∀x,z:ℝ^n.  (d(z;r(-1)*x) < d(z;x) ⇐⇒ x⋅z < r0)
BY
{ (Intros THEN (InstLemma `real-vec-angle-lemma` [⌜n⌝;⌜r(-1)*x⌝;⌜z⌝]⋅ THENA Auto)) }

1
1. n : ℕ
2. x : ℝ^n
3. z : ℝ^n
4. d(z;r(-1)*x) < d(z;r(-1)*r(-1)*x) ⇐⇒ r0 < r(-1)*x⋅z
⊢ d(z;r(-1)*x) < d(z;x) ⇐⇒ x⋅z < r0

---

Latex:

---

Latex:
\mforall{}n:\mBbbN{}.  \mforall{}x,z:\mBbbR{}\^{}n.    (d(z;r(-1)*x)  <  d(z;x)  \mLeftarrow{}{}\mRightarrow{}  x\mcdot{}z  <  r0)


By

---

Latex:
(Intros  THEN  (InstLemma  `real-vec-angle-lemma`  [\mkleeneopen{}n\mkleeneclose{};\mkleeneopen{}r(-1)*x\mkleeneclose{};\mkleeneopen{}z\mkleeneclose{}]\mcdot{}  THENA  Auto))

---

Home Index