Logarithm Injective / Surjective

Stream: new members

[James Arthur]

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?

[Bryan Gin-ge Chen]

There's docs#real.log_surjective at least.

[Yakov Pechersky]

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

[Alex J. Best]

and injectivity should follow from docs#real.log_lt_log_iff

[Yakov Pechersky]

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

[Bryan Gin-ge Chen]

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

[James Arthur]

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