Measure for some σ-algebra

Stream: maths

[Yury G. Kudryashov]

Is there a nice description of ⋃ (_ : MeasurableSpace α), Set.range fun μ : Measure α ↦ μ.toOuterMeasure?

[Bjørn Kjos-Hanssen]

What's the definition of μ.toOuterMeasure?

[Yury G. Kudryashov]

Projection from docs#MeasureTheory.Measure to docs#MeasureTheory.OuterMeasure

[Etienne Marion]

It is the greatest outer measure which coincides with mu on measurable sets.

[Bjørn Kjos-Hanssen]

If I understand this right, for example if α has two elements a, b, then the outer measures are all functions μ determined by ENNReal numbers x=μ{a}, y=μ{b}, z=μ{a,b} with x,y <= z<=x+y. Such a function is obtained from toOuterMeasure if x+y=z (with the sigma-algebra being the powerset) or x=y=z (for the sigma-algebra being trivial). So in this case the answer is {(x,y,z) | x+y=z or x=y=z}.