---

Step * of Lemma rv-norm-positive

∀rv:InnerProductSpace. ∀x:Point.  (x # 0 ⇒ (r0 < ||x||))
BY
{ (Auto THEN (FLemma `rv-ip-positive` [-1] THENA Auto) THEN Auto) }

---

Latex:

---

Latex:
\mforall{}rv:InnerProductSpace.  \mforall{}x:Point.    (x  \#  0  {}\mRightarrow{}  (r0  <  ||x||))


By

---

Latex:
(Auto  THEN  (FLemma  `rv-ip-positive`  [-1]  THENA  Auto)  THEN  Auto)

---

Home Index