---

Step * of Lemma hyp-dist_wf

∀[rv:InnerProductSpace]. ∀[x,y:Point].  (hyp (x,y) ∈ ℝ)
BY
{ ProveWfLemma }

1
1. rv : InnerProductSpace
2. x : Point
3. y : Point
⊢ (rsqrt(r1 + x^2) * rsqrt(r1 + y^2)) - x ⋅ y ∈ {x:ℝ| r1 ≤ x} 

---

Latex:

---

Latex:
\mforall{}[rv:InnerProductSpace].  \mforall{}[x,y:Point].    (hyp  (x,y)  \mmember{}  \mBbbR{})


By

---

Latex:
ProveWfLemma

---

Home Index