Zulip Chat Archive

Stream: new members

Topic: premeasures?

Scott Morrison (Mar 03 2020 at 02:35):

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.

Last updated: Dec 20 2023 at 11:08 UTC