---

Step * of Lemma real-vec-norm-equal-iff

∀[n:ℕ]. ∀[x,y:ℝ^n].  uiff(||x|| = ||y||;x⋅x = y⋅y)
BY
{ ((UnivCD THENA Auto) THEN (RWO "real-vec-norm-eq-iff" 0 THENA Auto)) }

1
1. n : ℕ
2. x : ℝ^n
3. y : ℝ^n
⊢ uiff((x⋅x = ||y||^2) ∧ (r0 ≤ ||y||);x⋅x = y⋅y)

---

Latex:

---

Latex:
\mforall{}[n:\mBbbN{}].  \mforall{}[x,y:\mBbbR{}\^{}n].    uiff(||x||  =  ||y||;x\mcdot{}x  =  y\mcdot{}y)


By

---

Latex:
((UnivCD  THENA  Auto)  THEN  (RWO  "real-vec-norm-eq-iff"  0  THENA  Auto))

---

Home Index