---

Step * of Lemma real-vec-norm-is-0

∀[n:ℕ]. ∀[x:ℝ^n].  uiff(||x|| = r0;req-vec(n;x;λi.r0))
BY
{ Auto }

1
1. n : ℕ
2. x : ℝ^n
3. ||x|| = r0
⊢ req-vec(n;x;λi.r0)

2
1. n : ℕ
2. x : ℝ^n
3. req-vec(n;x;λi.r0)
⊢ ||x|| = r0

---

Latex:

---

Latex:
\mforall{}[n:\mBbbN{}].  \mforall{}[x:\mBbbR{}\^{}n].    uiff(||x||  =  r0;req-vec(n;x;\mlambda{}i.r0))


By

---

Latex:
Auto

---

Home Index