α : Type u_2
β : Type ?u.795368
γ : Type ?u.795371
δ : Type ?u.795374
m : MeasurableSpace α
μ ν : Measure α
ι : Type u_1
f : α → ℝ≥0∞
h : (∫⁻ (x : α), f x ∂μ) ≠ ⊤
l : Filter ι
s : ι → Set α
hl : ∀ (i : ℝ≥0∞), 0 < i → ∀ᶠ (a : ι) in l, (↑↑μ ∘ s) a < i
⊢ ∀ (i : ℝ≥0∞), 0 < i → ∀ᶠ (a : ι) in l, (∫⁻ (x : α) in s a, f x ∂μ) < i
α : Type u_2
β : Type ?u.795368
γ : Type ?u.795371
δ : Type ?u.795374
m : MeasurableSpace α
μ ν : Measure α
ι : Type u_1
f : α → ℝ≥0∞
h : (∫⁻ (x : α), f x ∂μ) ≠ ⊤
l : Filter ι
s : ι → Set α
hl : Tendsto (↑↑μ ∘ s) l (𝓝 0)
⊢ Tendsto (fun i => ∫⁻ (x : α) in s i, f x ∂μ) l (𝓝 0)
simp only [ENNReal.nhds_zero, tendsto_iInf, tendsto_principal, mem_Iio,
  ← pos_iff_ne_zero] at hl ⊢
α : Type u_2
β : Type ?u.795368
γ : Type ?u.795371
δ : Type ?u.795374
m : MeasurableSpace α
μ ν : Measure α
ι : Type u_1
f : α → ℝ≥0∞
h : (∫⁻ (x : α), f x ∂μ) ≠ ⊤
l : Filter ι
s : ι → Set α
hl : ∀ (i : ℝ≥0∞), 0 < i → ∀ᶠ (a : ι) in l, (↑↑μ ∘ s) a < i
ε : ℝ≥0∞
ε0 : 0 < ε
⊢ ∀ᶠ (a : ι) in l, (∫⁻ (x : α) in s a, f x ∂μ) < ε
α : Type u_2
β : Type ?u.795368
γ : Type ?u.795371
δ : Type ?u.795374
m : MeasurableSpace α
μ ν : Measure α
ι : Type u_1
f : α → ℝ≥0∞
h : (∫⁻ (x : α), f x ∂μ) ≠ ⊤
l : Filter ι
s : ι → Set α
hl : ∀ (i : ℝ≥0∞), 0 < i → ∀ᶠ (a : ι) in l, (↑↑μ ∘ s) a < i
⊢ ∀ (i : ℝ≥0∞), 0 < i → ∀ᶠ (a : ι) in l, (∫⁻ (x : α) in s a, f x ∂μ) < i
intro ε ε0
case intro.intro
α : Type u_2
β : Type ?u.795368
γ : Type ?u.795371
δ✝ : Type ?u.795374
m : MeasurableSpace α
μ ν : Measure α
ι : Type u_1
f : α → ℝ≥0∞
h : (∫⁻ (x : α), f x ∂μ) ≠ ⊤
l : Filter ι
s : ι → Set α
hl : ∀ (i : ℝ≥0∞), 0 < i → ∀ᶠ (a : ι) in l, (↑↑μ ∘ s) a < i
ε : ℝ≥0∞
ε0 : 0 < ε
δ : ℝ≥0∞
δ0 : δ > 0
hδ : ∀ (s : Set α), ↑↑μ s < δ → (∫⁻ (x : α) in s, f x ∂μ) < ε
⊢ ∀ᶠ (a : ι) in l, (∫⁻ (x : α) in s a, f x ∂μ) < ε
α : Type u_2
β : Type ?u.795368
γ : Type ?u.795371
δ : Type ?u.795374
m : MeasurableSpace α
μ ν : Measure α
ι : Type u_1
f : α → ℝ≥0∞
h : (∫⁻ (x : α), f x ∂μ) ≠ ⊤
l : Filter ι
s : ι → Set α
hl : ∀ (i : ℝ≥0∞), 0 < i → ∀ᶠ (a : ι) in l, (↑↑μ ∘ s) a < i
ε : ℝ≥0∞
ε0 : 0 < ε
⊢ ∀ᶠ (a : ι) in l, (∫⁻ (x : α) in s a, f x ∂μ) < ε
rcases exists_pos_set_lintegral_lt_of_measure_lt h ε0.ne' with ⟨δ, δ0, hδ⟩
no goals
case intro.intro
α : Type u_2
β : Type ?u.795368
γ : Type ?u.795371
δ✝ : Type ?u.795374
m : MeasurableSpace α
μ ν : Measure α
ι : Type u_1
f : α → ℝ≥0∞
h : (∫⁻ (x : α), f x ∂μ) ≠ ⊤
l : Filter ι
s : ι → Set α
hl : ∀ (i : ℝ≥0∞), 0 < i → ∀ᶠ (a : ι) in l, (↑↑μ ∘ s) a < i
ε : ℝ≥0∞
ε0 : 0 < ε
δ : ℝ≥0∞
δ0 : δ > 0
hδ : ∀ (s : Set α), ↑↑μ s < δ → (∫⁻ (x : α) in s, f x ∂μ) < ε
⊢ ∀ᶠ (a : ι) in l, (∫⁻ (x : α) in s a, f x ∂μ) < ε
exact (hl δ δ0).mono fun i => hδ _