Zulip Chat Archive

Stream: new members

Topic: Logarithm Injective / Surjective


view this post on Zulip James Arthur (Nov 12 2020 at 21:51):

I was proving a few lemmas about the injectivity ( > 0) and sujectivity of the logarithm function and went to look in mathlib and it seems that it isn't there. Is this PRable? / Is it needed?

view this post on Zulip Bryan Gin-ge Chen (Nov 12 2020 at 21:58):

There's docs#real.log_surjective at least.

view this post on Zulip Yakov Pechersky (Nov 12 2020 at 22:41):

And docs#subtype.restrict_injective, I don't know of a better way of expressing injectivity on a subset of a domain

view this post on Zulip Alex J. Best (Nov 12 2020 at 22:41):

and injectivity should follow from docs#real.log_lt_log_iff

view this post on Zulip Yakov Pechersky (Nov 12 2020 at 22:43):

Or use docs#function.left_inverse.injective with docs#real.exp

view this post on Zulip Bryan Gin-ge Chen (Nov 12 2020 at 23:11):

I forgot to say this earlier, but I think injectivity would definitely be PR-able (assuming we haven't missed it somewhere).

view this post on Zulip James Arthur (Nov 13 2020 at 09:53):

OK, I must have missed those in my search through the file. Thanks.


Last updated: May 12 2021 at 05:19 UTC