mathlib3
c04daaf4
- feat(measure_theory): typeclass for measures positive on nonempty opens (#11652)
Go
Login via GitHub
Home
Pricing
FAQ
Install
Login
via GitHub
Commit
View On
GitHub
Commit
3 years ago
feat(measure_theory): typeclass for measures positive on nonempty opens (#11652) Add a typeclass for measures positive on nonempty opens, migrate `is(_add?)_haar_measure` to this API. Co-authored-by: Floris van Doorn <fpvdoorn@gmail.com>
Author
urkud
Parents
d6440a84
Loading