Assumptions:
TeX:
\operatorname{atan}\!\left(\overline{z}\right) = \overline{\operatorname{atan}(z)} z \in \mathbb{C} \;\mathbin{\operatorname{and}}\; i z \notin \left(-\infty, -1\right) \cup \left(1, \infty\right)
Definitions:
Fungrim symbol | Notation | Short description |
---|---|---|
Atan | Inverse tangent | |
Conjugate | Complex conjugate | |
CC | Complex numbers | |
ConstI | Imaginary unit | |
OpenInterval | Open interval | |
Infinity | Positive infinity |
Source code for this entry:
Entry(ID("632063"), Formula(Equal(Atan(Conjugate(z)), Conjugate(Atan(z)))), Variables(z), Assumptions(And(Element(z, CC), NotElement(Mul(ConstI, z), Union(OpenInterval(Neg(Infinity), -1), OpenInterval(1, Infinity))))))