---

Step * of Lemma arctangent0

arctangent(r0) = r0
BY
{ (Unfold `arctangent` 0 THEN Using [`I', ⌜(-∞, ∞)⌝ ] (BLemma `integral-same-endpoints`)⋅ THEN Auto) }

1
λt.(r1/r1 + t^2) ∈ {f:(-∞, ∞) ⟶ℝ| ∀x,y:{a:ℝ| True} .  ((x = y) ⇒ ((f x) = (f y)))} 

---

Latex:

---

Latex:
arctangent(r0)  =  r0


By

---

Latex:
(Unfold  `arctangent`  0  THEN  Using  [`I',  \mkleeneopen{}(-\minfty{},  \minfty{})\mkleeneclose{}  ]  (BLemma  `integral-same-endpoints`)\mcdot{}  THEN  Auto)

---

Home Index