---

Step * of Lemma atan-small_wf

∀[x:ℝ]. atan-small(x) ∈ {y:ℝ| arctangent(x) = y}  supposing |x| ≤ (r1/r(2))
BY
{ ProveWfLemma }

1
1. x : ℝ
2. |x| ≤ (r1/r(2))
⊢ |x| ≤ (r1/r(atan-size-bound(x)))

---

Latex:

---

Latex:
\mforall{}[x:\mBbbR{}].  atan-small(x)  \mmember{}  \{y:\mBbbR{}|  arctangent(x)  =  y\}    supposing  |x|  \mleq{}  (r1/r(2))


By

---

Latex:
ProveWfLemma

---

Home Index