Stream: new members
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?
Bryan Gin-ge Chen (Nov 12 2020 at 21:58):
There's docs#real.log_surjective at least.
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
Alex J. Best (Nov 12 2020 at 22:41):
and injectivity should follow from docs#real.log_lt_log_iff
Yakov Pechersky (Nov 12 2020 at 22:43):
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).
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