---

Step * of Lemma rsqrt-1-plus-ip-positive

∀rv:InnerProductSpace. ∀h:Point.  (r0 < rsqrt(r1 + h^2))
BY
{ (Auto THEN BLemma `rsqrt-positive` THEN Auto THEN MemTypeCD THEN Auto THEN RWO "rv-ip-nonneg<" 0 THEN Auto) }

---

Latex:

---

Latex:
\mforall{}rv:InnerProductSpace.  \mforall{}h:Point.    (r0  <  rsqrt(r1  +  h\^{}2))


By

---

Latex:
(Auto
  THEN  BLemma  `rsqrt-positive`
  THEN  Auto
  THEN  MemTypeCD
  THEN  Auto
  THEN  RWO  "rv-ip-nonneg<"  0
  THEN  Auto)

---

Home Index