---

Step * of Lemma derivative-rlog

d(rlog(x))/dx = λx.(r1/x) on (r0, ∞)
BY
{ (Unfold `rlog` 0 THEN BLemma `derivative-of-integral` THEN Auto) }

1
λx.(r1/x) ∈ {f:(r0, ∞) ⟶ℝ| ∀x,y:{a:ℝ| r0 < a} .  ((x = y) ⇒ ((f x) = (f y)))} 

---

Latex:

---

Latex:
d(rlog(x))/dx  =  \mlambda{}x.(r1/x)  on  (r0,  \minfty{})


By

---

Latex:
(Unfold  `rlog`  0  THEN  BLemma  `derivative-of-integral`  THEN  Auto)

---

Home Index