Theorems · Theorem · measure theory

MeasureTheory.tendsto_measure_of_le_liminf_measure_of_limsup_measure_le

∀ {Ω : Type u_1} [inst : MeasurableSpace Ω] {ι : Type u_2} {L : Filter ι} {μ : MeasureTheory.Measure Ω}
  {μs : ι → MeasureTheory.Measure Ω} {E₀ E E₁ : Set Ω},
  E₀ ⊆ E →
    E ⊆ E₁ →
      μ (E₁ \ E₀) = 0 →
        μ E₀ ≤ Filter.liminf (fun i => (μs i) E₀) L →
          Filter.limsup (fun i => (μs i) E₁) L ≤ μ E₁ → Filter.Tendsto (fun i => (μs i) E) L (nhds (μ E))

Defined in

Mathlib.MeasureTheory.Measure.Portmanteau

Cited by

1 results in Mathlib

Foundations

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

Assumes

MeasurableSpace