Assumptions:
TeX:
\operatorname{atan}(z) = -\frac{i}{2} \log\!\left(\frac{1 + i z}{1 - i z}\right) z \in \mathbb{C} \;\mathbin{\operatorname{and}}\; z i \notin \left[1, \infty\right)
Definitions:
Fungrim symbol | Notation | Short description |
---|---|---|
Atan | Inverse tangent | |
ConstI | Imaginary unit | |
Log | Natural logarithm | |
CC | Complex numbers | |
ClosedOpenInterval | Closed-open interval | |
Infinity | Positive infinity |
Source code for this entry:
Entry(ID("12765e"), Formula(Equal(Atan(z), Mul(Neg(Div(ConstI, 2)), Log(Div(Add(1, Mul(ConstI, z)), Sub(1, Mul(ConstI, z))))))), Variables(z), Assumptions(And(Element(z, CC), NotElement(Mul(z, ConstI), ClosedOpenInterval(1, Infinity)))))