Mathlib.Measure­Theory.Function.Analytic

Universal measurability of analytic-set constructions.

Universal­Measurability 8 core · 14 supporting · 3 submodules This module gathers the Choquet-capacity proof that analytic events in Polish Borel spaces are measurable for every completed finite measure, together with the corresponding completed measurability and outer-integral bri