Analytic sets: compact capacity equals measure #
Headline corollary of Choquet capacitability. For any finite Borel measure on
a Polish space and any analytic s, compactCap μ s = μ s.
theorem
MeasureTheory.AnalyticSet.compactCap_eq
{α : Type u_1}
[TopologicalSpace α]
[MeasurableSpace α]
[BorelSpace α]
[PolishSpace α]
{μ : Measure α}
[IsFiniteMeasure μ]
{s : Set α}
(hs : AnalyticSet s)
:
For analytic sets, compact capacity equals measure.