---

Step * of Lemma hyptrans_decomp

∀rv:InnerProductSpace. ∀e,x:Point.
  ∃h:Point. ∃tau:ℝ. ((h ⋅ e = r0) ∧ x ≡ h + sinh(tau) * rsqrt(r1 + h^2)*e) supposing e^2 = r1
BY
{ Auto }

1
1. rv : InnerProductSpace
2. e : Point
3. x : Point
4. e^2 = r1
⊢ ∃h:Point. ∃tau:ℝ. ((h ⋅ e = r0) ∧ x ≡ h + sinh(tau) * rsqrt(r1 + h^2)*e)

---

Latex:

---

Latex:
\mforall{}rv:InnerProductSpace.  \mforall{}e,x:Point.
    \mexists{}h:Point.  \mexists{}tau:\mBbbR{}.  ((h  \mcdot{}  e  =  r0)  \mwedge{}  x  \mequiv{}  h  +  sinh(tau)  *  rsqrt(r1  +  h\^{}2)*e)  supposing  e\^{}2  =  r1


By

---

Latex:
Auto

---

Home Index