---

Step * of Lemma real-vec-norm_functionality

∀[n:ℕ]. ∀[x,y:ℝ^n].  ||x|| = ||y|| supposing req-vec(n;x;y)
BY
{ (Auto THEN Unfold `real-vec-norm` 0 THEN (Assert x ⋅ x = y ⋅ y BY (BLemma `dot-product_functionality` THEN Auto))) }

1
1. n : ℕ
2. x : ℝ^n
3. y : ℝ^n
4. req-vec(n;x;y)
5. x ⋅ x = y ⋅ y
⊢ rsqrt(x ⋅ x) = rsqrt(y ⋅ y)

---

Latex:

---

Latex:
\mforall{}[n:\mBbbN{}].  \mforall{}[x,y:\mBbbR{}\^{}n].    ||x||  =  ||y||  supposing  req-vec(n;x;y)


By

---

Latex:
(Auto
  THEN  Unfold  `real-vec-norm`  0
  THEN  (Assert  x  \mcdot{}  x  =  y  \mcdot{}  y  BY
                          (BLemma  `dot-product\_functionality`  THEN  Auto)))

---

Home Index