Choquet capacitability for analytic sets

Kechris, Classical Descriptive Set Theory, Theorem 30.13: for any Choquet capacity cap on a Polish space and any analytic s, cap s equals the supremum of cap K over compact subsets K ⊆ s. The analytic set is parametrised as the continuous image of ℕ^ℕ, a sequence of truncation bounds N : ℕ → ℕ is built by diagonal induction using iUnion_nat, and iInter_closed is applied to the closures of cylinder images to collapse the intersection to a compact image via iInter_closure_image_cyl_eq.

theorem MeasureTheory.AnalyticSet.cap_eq_iSup_isCompact {α : Type u_1} [TopologicalSpace α] [MeasurableSpace α] [BorelSpace α] [PolishSpace α] {cap : Set α → ENNReal} (hcap : IsChoquetCapacity cap) {s : Set α} (hs : AnalyticSet s) : cap s = ⨆ (K : Set α), ⨆ (_ : IsCompact K), ⨆ (_ : K ⊆ s), cap K

Choquet capacitability. For analytic sets, capacity equals the supremum over compact subsets (Kechris 30.13).