case mp
Ω : Type u_2
inst✝⁴ : MeasurableSpace Ω
inst✝³ : TopologicalSpace Ω
inst✝² : OpensMeasurableSpace Ω
ι : Type u_1
L : Filter ι
μ : Measure Ω
μs : ι → Measure Ω
inst✝¹ : IsProbabilityMeasure μ
inst✝ : ∀ (i : ι), IsProbabilityMeasure (μs i)
⊢ (∀ (F : Set Ω), IsClosed F → limsup (fun i => ↑↑(μs i) F) L ≤ ↑↑μ F) →
    ∀ (G : Set Ω), IsOpen G → ↑↑μ G ≤ liminf (fun i => ↑↑(μs i) G) L

case mpr
Ω : Type u_2
inst✝⁴ : MeasurableSpace Ω
inst✝³ : TopologicalSpace Ω
inst✝² : OpensMeasurableSpace Ω
ι : Type u_1
L : Filter ι
μ : Measure Ω
μs : ι → Measure Ω
inst✝¹ : IsProbabilityMeasure μ
inst✝ : ∀ (i : ι), IsProbabilityMeasure (μs i)
⊢ (∀ (G : Set Ω), IsOpen G → ↑↑μ G ≤ liminf (fun i => ↑↑(μs i) G) L) →
    ∀ (F : Set Ω), IsClosed F → limsup (fun i => ↑↑(μs i) F) L ≤ ↑↑μ F
Ω : Type u_2
inst✝⁴ : MeasurableSpace Ω
inst✝³ : TopologicalSpace Ω
inst✝² : OpensMeasurableSpace Ω
ι : Type u_1
L : Filter ι
μ : Measure Ω
μs : ι → Measure Ω
inst✝¹ : IsProbabilityMeasure μ
inst✝ : ∀ (i : ι), IsProbabilityMeasure (μs i)
⊢ (∀ (F : Set Ω), IsClosed F → limsup (fun i => ↑↑(μs i) F) L ≤ ↑↑μ F) ↔
    ∀ (G : Set Ω), IsOpen G → ↑↑μ G ≤ liminf (fun i => ↑↑(μs i) G) L
constructor
case mp
Ω : Type u_2
inst✝⁴ : MeasurableSpace Ω
inst✝³ : TopologicalSpace Ω
inst✝² : OpensMeasurableSpace Ω
ι : Type u_1
L : Filter ι
μ : Measure Ω
μs : ι → Measure Ω
inst✝¹ : IsProbabilityMeasure μ
inst✝ : ∀ (i : ι), IsProbabilityMeasure (μs i)
h : ∀ (F : Set Ω), IsClosed F → limsup (fun i => ↑↑(μs i) F) L ≤ ↑↑μ F
G : Set Ω
G_open : IsOpen G
⊢ ↑↑μ G ≤ liminf (fun i => ↑↑(μs i) G) L
case mp
Ω : Type u_2
inst✝⁴ : MeasurableSpace Ω
inst✝³ : TopologicalSpace Ω
inst✝² : OpensMeasurableSpace Ω
ι : Type u_1
L : Filter ι
μ : Measure Ω
μs : ι → Measure Ω
inst✝¹ : IsProbabilityMeasure μ
inst✝ : ∀ (i : ι), IsProbabilityMeasure (μs i)
⊢ (∀ (F : Set Ω), IsClosed F → limsup (fun i => ↑↑(μs i) F) L ≤ ↑↑μ F) →
    ∀ (G : Set Ω), IsOpen G → ↑↑μ G ≤ liminf (fun i => ↑↑(μs i) G) L
intro h G G_open
no goals
case mp
Ω : Type u_2
inst✝⁴ : MeasurableSpace Ω
inst✝³ : TopologicalSpace Ω
inst✝² : OpensMeasurableSpace Ω
ι : Type u_1
L : Filter ι
μ : Measure Ω
μs : ι → Measure Ω
inst✝¹ : IsProbabilityMeasure μ
inst✝ : ∀ (i : ι), IsProbabilityMeasure (μs i)
h : ∀ (F : Set Ω), IsClosed F → limsup (fun i => ↑↑(μs i) F) L ≤ ↑↑μ F
G : Set Ω
G_open : IsOpen G
⊢ ↑↑μ G ≤ liminf (fun i => ↑↑(μs i) G) L
exact le_measure_liminf_of_limsup_measure_compl_le
  G_open.measurableSet (h (Gᶜ) (isClosed_compl_iff.mpr G_open))
case mpr
Ω : Type u_2
inst✝⁴ : MeasurableSpace Ω
inst✝³ : TopologicalSpace Ω
inst✝² : OpensMeasurableSpace Ω
ι : Type u_1
L : Filter ι
μ : Measure Ω
μs : ι → Measure Ω
inst✝¹ : IsProbabilityMeasure μ
inst✝ : ∀ (i : ι), IsProbabilityMeasure (μs i)
h : ∀ (G : Set Ω), IsOpen G → ↑↑μ G ≤ liminf (fun i => ↑↑(μs i) G) L
F : Set Ω
F_closed : IsClosed F
⊢ limsup (fun i => ↑↑(μs i) F) L ≤ ↑↑μ F
case mpr
Ω : Type u_2
inst✝⁴ : MeasurableSpace Ω
inst✝³ : TopologicalSpace Ω
inst✝² : OpensMeasurableSpace Ω
ι : Type u_1
L : Filter ι
μ : Measure Ω
μs : ι → Measure Ω
inst✝¹ : IsProbabilityMeasure μ
inst✝ : ∀ (i : ι), IsProbabilityMeasure (μs i)
⊢ (∀ (G : Set Ω), IsOpen G → ↑↑μ G ≤ liminf (fun i => ↑↑(μs i) G) L) →
    ∀ (F : Set Ω), IsClosed F → limsup (fun i => ↑↑(μs i) F) L ≤ ↑↑μ F
intro h F F_closed
no goals
case mpr
Ω : Type u_2
inst✝⁴ : MeasurableSpace Ω
inst✝³ : TopologicalSpace Ω
inst✝² : OpensMeasurableSpace Ω
ι : Type u_1
L : Filter ι
μ : Measure Ω
μs : ι → Measure Ω
inst✝¹ : IsProbabilityMeasure μ
inst✝ : ∀ (i : ι), IsProbabilityMeasure (μs i)
h : ∀ (G : Set Ω), IsOpen G → ↑↑μ G ≤ liminf (fun i => ↑↑(μs i) G) L
F : Set Ω
F_closed : IsClosed F
⊢ limsup (fun i => ↑↑(μs i) F) L ≤ ↑↑μ F
exact limsup_measure_le_of_le_liminf_measure_compl
  F_closed.measurableSet (h (Fᶜ) (isOpen_compl_iff.mpr F_closed))