---

Step * of Lemma inv-sinh_functionality

∀[x,y:ℝ].  inv-sinh(x) = inv-sinh(y) supposing x = y
BY
{ (Auto THEN (InstLemma `inv-sinh-domain` [⌜x⌝]⋅ THENA Auto)) }

1
1. x : ℝ
2. y : ℝ
3. x = y
4. (r0 ≤ ((x * x) + r1)) ∧ (r0 < (x + rsqrt((x * x) + r1)))
⊢ inv-sinh(x) = inv-sinh(y)

---

Latex:

---

Latex:
\mforall{}[x,y:\mBbbR{}].    inv-sinh(x)  =  inv-sinh(y)  supposing  x  =  y


By

---

Latex:
(Auto  THEN  (InstLemma  `inv-sinh-domain`  [\mkleeneopen{}x\mkleeneclose{}]\mcdot{}  THENA  Auto))

---

Home Index