Theorem Real.tendstoLocallyUniformlyOn_rpow_sub_one_log

Modification history

2025-11-26 02:38
Mathlib/Analysis/SpecialFunctions/Log/RpowTendsto.lean
feat(CStarAlgebra): the log is operator monotone (#30894) …
Added Real.tendstoLocallyUniformlyOn_rpow_sub_one_logView on Github →