Theorem Real.tendsto_log_nhdsWithin_zero_right

Modification history

2025-03-19 07:35

Mathlib/Analysis/SpecialFunctions/Log/Basic.lean

chore(SpecialFunctions/Log): rename some `Tendsto` lemmas (#23083) …

Deleted Real.tendsto_log_nhdsWithin_zero_right View on Github →

2023-11-27 15:05

Mathlib/Analysis/SpecialFunctions/Log/Basic.lean

feat(SpecialFunctions/Log): add `tendsto_log_nhdsWithin_zero_right` (#8554) …

Added Real.tendsto_log_nhdsWithin_zero_right View on Github →