premeasures

Stream: Is there code for X?

[Jason KY.]

I would like to show that for a set function defined on a ring of sets satisfying finite additivity and continuity from above, it is a premeasure (and induces a measure...). I found induced_outer_measurewhich seems to be relevant but I'm wondering if ring of sets/premeasures are defined explicitly anywhere?