---

Step * of Lemma rv-ip-positive

∀rv:InnerProductSpace. ∀x:Point.  (x # 0 ⇐⇒ r0 < x^2)
BY
{ ((D 0 THENA Auto)
   THEN (Assert rv ∈ InnerProductSpace BY
               Auto)
   THEN UseWitness ⌜rv."positive"⌝⋅
   THEN (D 1 THENA Auto)
   THEN Unfold `rv-ip` 0
   THEN Trivial) }

---

Latex:

---

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


By

---

Latex:
((D  0  THENA  Auto)
  THEN  (Assert  rv  \mmember{}  InnerProductSpace  BY
                          Auto)
  THEN  UseWitness  \mkleeneopen{}rv."positive"\mkleeneclose{}\mcdot{}
  THEN  (D  1  THENA  Auto)
  THEN  Unfold  `rv-ip`  0
  THEN  Trivial)

---

Home Index