---

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

No Annotations
∀[n:ℕ]. ∀[x:ℝ^n]. ∀[r:ℝ].  uiff(||x|| = r;(x⋅x = r^2) ∧ (r0 ≤ r))
BY
{ Auto }

1
1. n : ℕ
2. x : ℝ^n
3. r : ℝ
4. ||x|| = r
⊢ x⋅x = r^2

2
1. n : ℕ
2. x : ℝ^n
3. r : ℝ
4. ||x|| = r
⊢ r0 ≤ r

3
1. n : ℕ
2. x : ℝ^n
3. r : ℝ
4. x⋅x = r^2
5. r0 ≤ r
⊢ ||x|| = r

---

Latex:

---

Latex:
No  Annotations
\mforall{}[n:\mBbbN{}].  \mforall{}[x:\mBbbR{}\^{}n].  \mforall{}[r:\mBbbR{}].    uiff(||x||  =  r;(x\mcdot{}x  =  r\^{}2)  \mwedge{}  (r0  \mleq{}  r))


By

---

Latex:
Auto

---

Home Index