This file contains the following definitions: • π, arcsin, arccos, arctan • argument of a complex number • logarithm on real and complex numbers • complex and real power function
The following functions are shown to be continuous: • complex and real exponential function • sin, cos, tan, sinh, cosh • logarithm on real numbers • real power function • square root function
exp, log, sin, cos, tan, arcsin, arccos, arctan, angle, argument, power, square root,
Three forms of the continuity of real.log is provided. For the other two forms, see real.continuous_log' and real.continuous_at_log
The type of angles
Inverse of the sin function, returns values in the range -π / 2 ≤ arcsin x and arcsin x ≤ π / 2. If the argument is not between -1 and 1 it defaults to 0
Inverse of the cos function, returns values in the range 0 ≤ arccos x and arccos x ≤ π. If the argument is not between -1 and 1 it defaults to π / 2
Inverse of the tan function, returns values in the range -π / 2 < arctan x and arctan x < π / 2
arg returns values in the range (-π, π], such that for x ≠ 0, sin (arg x) = x.im / x.abs and cos (arg x) = x.re / x.abs, arg 0 defaults to 0
Inverse of the exp function. Returns values such that (log x).im > - π and (log x).im ≤ π. log 0 = 0
real.rpow is continuous at all points except for the lower half of the y-axis. In other words, the function λp:ℝ×ℝ, p.1^p.2 is continuous at (x, y) if x ≠ 0 or y > 0.
Multiple forms of the claim is provided in the current section.