Commit 2023-11-27 15:05 b70e89f1
View on Github →feat(SpecialFunctions/Log): add tendsto_log_nhdsWithin_zero_right (#8554)
I use this lemma several times in an external project.
Also, this lemma doesn't rely on our non-canonical extension of Real.log to negative numbers.