Choquet capacitability. For analytic sets, capacity equals the supremum over compact subsets (Kechris 30.13).
DeclMeasureTheory.AnalyticSet.cap_eq_iSup_isCompact
∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : MeasurableSpace α] [BorelSpace α] [PolishSpace α]
{cap : Set α → ENNReal},
MeasureTheory.IsChoquetCapacity cap →
∀ {s : Set α}, MeasureTheory.AnalyticSet s → cap s = ⨆ K, ⨆ (_ : IsCompact K), ⨆ (_ : K ⊆ s), cap KTopicAnalytic sets
Arguments
| DOI | Author | Date |
|---|---|---|
| MTH.R-2026-6018 | Dhruv Gupta | 2026-09-24T00:00:00Z |
DOIMTH.C-2026-6018
Cite
Verification
- Library
- ZPM.MeasureTheory.ChoquetCapacity.Capacitability
- Statement digest
- 1f2bb195896f
- First verified
- 2026-09-24T00:00:00Z