Ω✝ : Type ?u.24613
inst✝⁴ : MeasurableSpace Ω✝
Ω : Type u_1
inst✝³ : MeasurableSpace Ω
inst✝² : PseudoEMetricSpace Ω
inst✝¹ : OpensMeasurableSpace Ω
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
F : Set Ω
F_closed : IsClosed F
δs : ℕ → ℝ
δs_pos : ∀ (n : ℕ), 0 < δs n
δs_lim : Tendsto δs atTop (𝓝 0)
⊢ Tendsto (fun n => ↑(thickenedIndicator (_ : 0 < δs n) F)) atTop (𝓝 (indicator F fun x => 1))
Ω✝ : Type ?u.24613
inst✝⁴ : MeasurableSpace Ω✝
Ω : Type u_1
inst✝³ : MeasurableSpace Ω
inst✝² : PseudoEMetricSpace Ω
inst✝¹ : OpensMeasurableSpace Ω
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
F : Set Ω
F_closed : IsClosed F
δs : ℕ → ℝ
δs_pos : ∀ (n : ℕ), 0 < δs n
δs_lim : Tendsto δs atTop (𝓝 0)
⊢ Tendsto (fun n => ∫⁻ (ω : Ω), ↑(↑(thickenedIndicator (_ : 0 < δs n) F) ω) ∂μ) atTop (𝓝 (↑↑μ F))
apply measure_of_cont_bdd_of_tendsto_indicator μ F_closed.measurableSet
  (fun n => thickenedIndicator (δs_pos n) F) fun n ω => thickenedIndicator_le_one (δs_pos n) F ω
Ω✝ : Type ?u.24613
inst✝⁴ : MeasurableSpace Ω✝
Ω : Type u_1
inst✝³ : MeasurableSpace Ω
inst✝² : PseudoEMetricSpace Ω
inst✝¹ : OpensMeasurableSpace Ω
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
F : Set Ω
F_closed : IsClosed F
δs : ℕ → ℝ
δs_pos : ∀ (n : ℕ), 0 < δs n
δs_lim : Tendsto δs atTop (𝓝 0)
key : Tendsto (fun n => ↑(thickenedIndicator (_ : 0 < δs n) F)) atTop (𝓝 (indicator (closure F) fun x => 1))
⊢ Tendsto (fun n => ↑(thickenedIndicator (_ : 0 < δs n) F)) atTop (𝓝 (indicator F fun x => 1))
Ω✝ : Type ?u.24613
inst✝⁴ : MeasurableSpace Ω✝
Ω : Type u_1
inst✝³ : MeasurableSpace Ω
inst✝² : PseudoEMetricSpace Ω
inst✝¹ : OpensMeasurableSpace Ω
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
F : Set Ω
F_closed : IsClosed F
δs : ℕ → ℝ
δs_pos : ∀ (n : ℕ), 0 < δs n
δs_lim : Tendsto δs atTop (𝓝 0)
⊢ Tendsto (fun n => ↑(thickenedIndicator (_ : 0 < δs n) F)) atTop (𝓝 (indicator F fun x => 1))
have key := thickenedIndicator_tendsto_indicator_closure δs_pos δs_lim F
no goals
Ω✝ : Type ?u.24613
inst✝⁴ : MeasurableSpace Ω✝
Ω : Type u_1
inst✝³ : MeasurableSpace Ω
inst✝² : PseudoEMetricSpace Ω
inst✝¹ : OpensMeasurableSpace Ω
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
F : Set Ω
F_closed : IsClosed F
δs : ℕ → ℝ
δs_pos : ∀ (n : ℕ), 0 < δs n
δs_lim : Tendsto δs atTop (𝓝 0)
key : Tendsto (fun n => ↑(thickenedIndicator (_ : 0 < δs n) F)) atTop (𝓝 (indicator (closure F) fun x => 1))
⊢ Tendsto (fun n => ↑(thickenedIndicator (_ : 0 < δs n) F)) atTop (𝓝 (indicator F fun x => 1))
rwa [F_closed.closure_eq] at key