Zulip Chat Archive

Stream: maths

Topic: range of cos


view this post on Zulip Johan Commelin (Sep 25 2020 at 06:41):

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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Johan Commelin (Sep 25 2020 at 07:29):

@Floris van Doorn Thanks, I'll try.

view this post on Zulip Johan Commelin (Sep 25 2020 at 07:35):

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

view this post on Zulip Mario Carneiro (Sep 25 2020 at 12:23):

Isn't there an arccos function?

view this post on Zulip Mario Carneiro (Sep 25 2020 at 12:23):

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

view this post on Zulip Johan Commelin (Sep 25 2020 at 12:38):

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

view this post on Zulip Mario Carneiro (Sep 25 2020 at 12:42):

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

view this post on Zulip Mario Carneiro (Sep 25 2020 at 12:43):

See http://us.metamath.org/mpeuni/df-acos.html and http://us.metamath.org/mpeuni/df-asin.html


Last updated: May 18 2021 at 08:14 UTC