Theorem Real.le_log_one_add_of_nonneg

Modification history

2025-02-17 23:56
Mathlib/Analysis/SpecialFunctions/Log/Deriv.lean
feat(Analysis): lower bound for `log (1 + x)` (#21671)
Added Real.le_log_one_add_of_nonnegView on Github →