premeasures?

Stream: new members

[Scott Morrison]

I see we have outer measures, and Caratheodory extension for outer measures. Do we already have theorems about premeasures (sigma-additive functions on a ring of subsets)? There's the standard way to produce an outer measure from a premeasure (inf over ways to cover the set by sets in the ring), but I'm not finding this, and lemmas about it, in mathlib.