Measures positive on nonempty opens #
In this file we define a typeclass for measures that are positive on nonempty opens, see
MeasureTheory.Measure.IsOpenPosMeasure. Examples include (additive) Haar measures, as well as
measures that have positive density with respect to a Haar measure. We also prove some basic facts
about these measures.
If two functions are a.e. equal on an open set and are continuous on this set, then they are equal on this set.
If two continuous functions are a.e. equal, then they are equal.