mathlib3
5f6e827d - chore(measure_theory/measure/doubling): rename `is_doubling_measure` to `is_unif_loc_doubling_measure` (#18709)

Commit
2 years ago
chore(measure_theory/measure/doubling): rename `is_doubling_measure` to `is_unif_loc_doubling_measure` (#18709) With thanks to Jireh for highlighting our non-standard terminology. See also [Zulip conversation](https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/definition.20of.20doubling.20measures).
Author
Parents
Loading