Theorem ENNReal.log_lt_one_iff

Modification history

2024-07-12 14:35

Mathlib/Analysis/SpecialFunctions/Log/ENNRealLog.lean

feat(SpecialFunctions/Log): Add extended exp (#14107) …

Deleted ENNReal.log_lt_one_iff View on Github →

2024-06-23 16:19

Mathlib/Analysis/SpecialFunctions/Log/ENNReal.lean

feat(SpecialFunctions/Log): add extended nonnegative real logarithm (#14018) …

Added ENNReal.log_lt_one_iff View on Github →