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?

[Leo Du]

Hi! I have the same question -- did you end up finding a solution to this?

[Yury G. Kudryashov]

Could you please post the signature of the function you want to have in Lean, not in English?