tendsto_log_at_top

Stream: general

[Benjamin Davidson]

I have been searching for a lemma that states tendsto log at_top at_top but have not been able to find anything in the documentation. Does anyone know if such a lemma exists? (Presumably, it would be named tendsto_log_at_top.)

[Floris van Doorn]

I don't think it exists yet, since it doesn't exist in the file
https://leanprover-community.github.io/mathlib_docs/analysis/special_functions/exp_log.html

[Benjamin Davidson]

That's what I figured :( thanks anyway!

[Anatole Dedecker]

I can work on it if you're interested

[Anatole Dedecker]

#3826

[Benjamin Davidson]

Brilliant, thanks!