---

Step * of Lemma rv-norm-eq-iff

∀[rv:InnerProductSpace]. ∀[x:Point]. ∀[r:ℝ].  uiff(||x|| = r;x^2 = r^2) supposing r0 ≤ r
BY
{ Auto }

1
1. rv : InnerProductSpace
2. x : Point
3. r : ℝ
4. r0 ≤ r
5. ||x|| = r
⊢ x^2 = r^2

2
1. rv : InnerProductSpace
2. x : Point
3. r : ℝ
4. r0 ≤ r
5. x^2 = r^2
⊢ ||x|| = r

---

Latex:

---

Latex:
\mforall{}[rv:InnerProductSpace].  \mforall{}[x:Point].  \mforall{}[r:\mBbbR{}].    uiff(||x||  =  r;x\^{}2  =  r\^{}2)  supposing  r0  \mleq{}  r


By

---

Latex:
Auto

---

Home Index