Commit 2021-05-14 09:48 1199a3de
View on Github →feat(analysis/special_functions/exp_log): strengthen statement of continuous_log' (#7607)
The proof of continuous (λ x : {x : ℝ // 0 < x}, log x) also works for continuous (λ x : {x : ℝ // x ≠ 0}, log x).
I keep the preexisting lemma as well since it is used in a number of places and seems generally useful.