α : Type u_1
β : Type ?u.38973
m : MeasurableSpace α
μ✝ ν✝ μ ν : Measure α
inst✝ : SigmaFinite μ
⊢ ∀ (n : ℕ), ∀ᵐ (x : α) ∂ν, x ∈ spanningSets μ n → rnDeriv μ ν x < ⊤
α : Type u_1
β : Type ?u.38973
m : MeasurableSpace α
μ✝ ν✝ μ ν : Measure α
inst✝ : SigmaFinite μ
⊢ ∀ᵐ (x : α) ∂ν, rnDeriv μ ν x < ⊤
suffices ∀ n, ∀ᵐ x ∂ν, x ∈ spanningSets μ n → μ.rnDeriv ν x < ∞ by
  filter_upwards [ae_all_iff.2 this] with _ hx using hx _ (mem_spanningSetsIndex _ _)
α : Type u_1
β : Type ?u.38973
m : MeasurableSpace α
μ✝ ν✝ μ ν : Measure α
inst✝ : SigmaFinite μ
n : ℕ
⊢ ∀ᵐ (x : α) ∂ν, x ∈ spanningSets μ n → rnDeriv μ ν x < ⊤
α : Type u_1
β : Type ?u.38973
m : MeasurableSpace α
μ✝ ν✝ μ ν : Measure α
inst✝ : SigmaFinite μ
⊢ ∀ (n : ℕ), ∀ᵐ (x : α) ∂ν, x ∈ spanningSets μ n → rnDeriv μ ν x < ⊤
intro n
α : Type u_1
β : Type ?u.38973
m : MeasurableSpace α
μ✝ ν✝ μ ν : Measure α
inst✝ : SigmaFinite μ
n : ℕ
⊢ ∀ᵐ (x : α) ∂restrict ν (spanningSets μ n), rnDeriv μ ν x < ⊤
α : Type u_1
β : Type ?u.38973
m : MeasurableSpace α
μ✝ ν✝ μ ν : Measure α
inst✝ : SigmaFinite μ
n : ℕ
⊢ ∀ᵐ (x : α) ∂ν, x ∈ spanningSets μ n → rnDeriv μ ν x < ⊤
rw [← ae_restrict_iff' (measurable_spanningSets _ _)]
α : Type u_1
β : Type ?u.38973
m : MeasurableSpace α
μ✝ ν✝ μ ν : Measure α
inst✝ : SigmaFinite μ
n : ℕ
⊢ (∫⁻ (x : α) in spanningSets μ n, rnDeriv μ ν x ∂ν) ≠ ⊤
α : Type u_1
β : Type ?u.38973
m : MeasurableSpace α
μ✝ ν✝ μ ν : Measure α
inst✝ : SigmaFinite μ
n : ℕ
⊢ ∀ᵐ (x : α) ∂restrict ν (spanningSets μ n), rnDeriv μ ν x < ⊤
apply ae_lt_top (measurable_rnDeriv _ _)
α : Type u_1
β : Type ?u.38973
m : MeasurableSpace α
μ✝ ν✝ μ ν : Measure α
inst✝ : SigmaFinite μ
n : ℕ
⊢ ↑↑μ (spanningSets μ n) ≠ ⊤
α : Type u_1
β : Type ?u.38973
m : MeasurableSpace α
μ✝ ν✝ μ ν : Measure α
inst✝ : SigmaFinite μ
n : ℕ
⊢ (∫⁻ (x : α) in spanningSets μ n, rnDeriv μ ν x ∂ν) ≠ ⊤
refine' (lintegral_rnDeriv_lt_top_of_measure_ne_top _ _).ne
no goals
α : Type u_1
β : Type ?u.38973
m : MeasurableSpace α
μ✝ ν✝ μ ν : Measure α
inst✝ : SigmaFinite μ
n : ℕ
⊢ ↑↑μ (spanningSets μ n) ≠ ⊤
exact (measure_spanningSets_lt_top _ _).ne
no goals
α : Type u_1
β : Type ?u.38973
m : MeasurableSpace α
μ✝ ν✝ μ ν : Measure α
inst✝ : SigmaFinite μ
this : ∀ (n : ℕ), ∀ᵐ (x : α) ∂ν, x ∈ spanningSets μ n → rnDeriv μ ν x < ⊤
⊢ ∀ᵐ (x : α) ∂ν, rnDeriv μ ν x < ⊤
filter_upwards [ae_all_iff.2 this] with _ hx using hx _ (mem_spanningSetsIndex _ _)