Theorems · Theorem · measure theory

MeasureTheory.exists_measure_iUnion_gt_of_isCompact_closure

∀ {𝓧 : Type u_1} {m𝓧 : MeasurableSpace 𝓧} [inst : PseudoMetricSpace 𝓧] [inst_1 : OpensMeasurableSpace 𝓧]
  [SecondCountableTopology 𝓧] {S : Set (MeasureTheory.ProbabilityMeasure 𝓧)} (U : ℕ → Set 𝓧),
  (∀ (i : ℕ), IsOpen (U i)) →
    ⋃ i, U i = Set.univ →
      IsCompact (closure S) → ∀ (ε : ENNReal), 0 < ε → ε ≤ 1 → ∃ k, ∀ μ ∈ S, 1 - ε < ↑(μ (⋃ i, ⋃ (_ : i ≤ k), U i))

Defined in

Mathlib.MeasureTheory.Measure.Prokhorov

Cited by

1 results in Mathlib

Foundations

Depth 271 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

PseudoMetricSpaceOpensMeasurableSpaceSecondCountableTopology