Compact capacity equals measure on measurable sets #
The easy half of the Choquet capacitability statement: for Borel-measurable
sets s, compactCap μ s = μ s. The analytic-set half requires the
cylinder machinery and lives in AnalyticCompactCap.lean.
theorem
MeasureTheory.MeasurableSet.compactCap_eq
{α : Type u_1}
[TopologicalSpace α]
[MeasurableSpace α]
[BorelSpace α]
[PolishSpace α]
{μ : Measure α}
[IsFiniteMeasure μ]
{s : Set α}
(hs : MeasurableSet s)
:
For Borel-measurable sets, compact capacity equals measure. Two-sided
bound via monotonicity and Mathlib's MeasurableSet.exists_isCompact_lt_add.