---

Step * of Lemma rsqrt-is-one

No Annotations
∀[x:ℝ]. uiff((r0 ≤ x) ∧ (rsqrt(x) = r1);x = r1)
BY
{ (Auto THEN Try (RepeatFor 2 (((RWO "2" 0 THEN Auto) THEN MemTypeCD THEN Auto)))) }

---

Latex:

---

Latex:
No  Annotations
\mforall{}[x:\mBbbR{}].  uiff((r0  \mleq{}  x)  \mwedge{}  (rsqrt(x)  =  r1);x  =  r1)


By

---

Latex:
(Auto  THEN  Try  (RepeatFor  2  (((RWO  "2"  0  THEN  Auto)  THEN  MemTypeCD  THEN  Auto))))

---

Home Index