Limits and continuity for real.logb
#11388
Labels
feature-request
This issue is a feature request, either for mathematics, tactics, or CI
good-first-project
PR #11246 defines
real.logb
: the logarithm baseb
. Many lemmas about this are provided inanalysis/special_functions/logb.lean
, roughly analogous to the lemmas for the natural logarithm inanalysis/special_functions/log.lean
. But lemmas about the limits and continuity ofreal.logb
should be added to round out the API.The text was updated successfully, but these errors were encountered: