---

Step * of Lemma real-vec-perp-exists

∀n:{2...}. ∀x:ℝ^n.  (x ≠ λi.r0 ⇒ (∃y:ℝ^n. (y ≠ λi.r0 ∧ (x⋅y = r0))))
BY
{ (Auto THEN (FLemma `real-vec-sep-iff` [-1] THENA Auto) THEN D -1 THEN Reduce -1 THEN (nRNorm (-1) THENA Auto)) }

1
1. n : {2...}
2. x : ℝ^n
3. x ≠ λi.r0
4. i : ℕn
5. r0 < |x i|
⊢ ∃y:ℝ^n. (y ≠ λi.r0 ∧ (x⋅y = r0))

---

Latex:

---

Latex:
\mforall{}n:\{2...\}.  \mforall{}x:\mBbbR{}\^{}n.    (x  \mneq{}  \mlambda{}i.r0  {}\mRightarrow{}  (\mexists{}y:\mBbbR{}\^{}n.  (y  \mneq{}  \mlambda{}i.r0  \mwedge{}  (x\mcdot{}y  =  r0))))


By

---

Latex:
(Auto
  THEN  (FLemma  `real-vec-sep-iff`  [-1]  THENA  Auto)
  THEN  D  -1
  THEN  Reduce  -1
  THEN  (nRNorm  (-1)  THENA  Auto))

---

Home Index