## Stream: maths

### Topic: range of cos

#### Johan Commelin (Sep 25 2020 at 06:41):

Do we know that complex.cos has infinite range? (That's all I need.)

#### Floris van Doorn (Sep 25 2020 at 07:06):

It's shouldn't be too hard with docs#real.range_cos, docs#cardinal.mk_Icc_real and definition of docs#real.cos. But presumably you want something shorter.

#### Kevin Buzzard (Sep 25 2020 at 07:22):

Presumably any function on the reals or complexes which is differentiable at some point with nonzero derivative has infinite image

#### Johan Commelin (Sep 25 2020 at 07:29):

@Floris van Doorn Thanks, I'll try.

#### Johan Commelin (Sep 25 2020 at 07:35):

@Floris van Doorn would you mind taking a look at #4241? It seems convenient (-;

#### Mario Carneiro (Sep 25 2020 at 12:23):

Isn't there an arccos function?

#### Mario Carneiro (Sep 25 2020 at 12:23):

that should prove pretty directly that the range of complex.cos is C

#### Johan Commelin (Sep 25 2020 at 12:38):

It seems that it's only there for real.cos

#### Mario Carneiro (Sep 25 2020 at 12:42):

Is complex.log there? It should just be some arithmetic of logs

#### Mario Carneiro (Sep 25 2020 at 12:43):

Last updated: May 18 2021 at 08:14 UTC