Theorem Real.monotoneOn_posLog

Modification history

2025-01-31 20:04
Mathlib/Analysis/SpecialFunctions/Log/PosLog.lean
feat: add function log⁺ (=positive part of the logarithm) and prove standard estimates (#21289) …
Added Real.monotoneOn_posLogView on Github →