---

Step * 1 of Lemma derivative-arctangent


1. ∀x:ℝ. (r0 < (r1 + x^2))
⊢ λx.(r1/r1 + x^2) ∈ {f:(-∞, ∞) ⟶ℝ| ∀x,y:{a:ℝ| True} .  ((x = y) ⇒ ((f x) = (f y)))} 
BY
{ ((MemTypeCD THEN Reduce 0 THEN Auto) THEN RWO  "-1" 0 THEN Auto) }

---

Latex:

---

Latex:

1.  \mforall{}x:\mBbbR{}.  (r0  <  (r1  +  x\^{}2))
\mvdash{}  \mlambda{}x.(r1/r1  +  x\^{}2)  \mmember{}  \{f:(-\minfty{},  \minfty{})  {}\mrightarrow{}\mBbbR{}|  \mforall{}x,y:\{a:\mBbbR{}|  True\}  .    ((x  =  y)  {}\mRightarrow{}  ((f  x)  =  (f  y)))\} 


By

---

Latex:
((MemTypeCD  THEN  Reduce  0  THEN  Auto)  THEN  RWO    "-1"  0  THEN  Auto)

---

Home Index