regular measure

Stream: maths

[Sebastien Gouezel]

@Floris van Doorn , regular measures are defined in mathlib using the inner condition that for any open set U, its measure is the supremum of the measures of compact sets it contains. However, most authors require this for all measurable sets, not only open sets (and indeed for many approximation arguments it is important to have it for all measurable sets). Would you mind if I change the definition to the more standard one?

[Sebastien Gouezel]

(The definitions are equivalent in most reasonable situations)

[Floris van Doorn]

Yes, feel free to change it.
The books I followed defined it this way (Wikipedia does so, too), but I've also seen the other definition.