α : Type u_1
β : Type ?u.1651966
E : Type u_2
F : Type ?u.1651972
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
f g : α → E
s t : Set α
μ ν : Measure α
hf : IntegrableOn f s
h't : ∀ᵐ (x : α) ∂μ, ¬x ∈ s → f x = 0
⊢ IntegrableOn f univ
α : Type u_1
β : Type ?u.1651966
E : Type u_2
F : Type ?u.1651972
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
f g : α → E
s t : Set α
μ ν : Measure α
hf : IntegrableOn f s
h't : ∀ᵐ (x : α) ∂μ, ¬x ∈ s → f x = 0
⊢ Integrable f
rw [← integrableOn_univ]
α : Type u_1
β : Type ?u.1651966
E : Type u_2
F : Type ?u.1651972
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
f g : α → E
s t : Set α
μ ν : Measure α
hf : IntegrableOn f s
h't : ∀ᵐ (x : α) ∂μ, ¬x ∈ s → f x = 0
⊢ ∀ᵐ (x : α) ∂μ, x ∈ univ \ s → f x = 0
α : Type u_1
β : Type ?u.1651966
E : Type u_2
F : Type ?u.1651972
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
f g : α → E
s t : Set α
μ ν : Measure α
hf : IntegrableOn f s
h't : ∀ᵐ (x : α) ∂μ, ¬x ∈ s → f x = 0
⊢ IntegrableOn f univ
apply hf.of_ae_diff_eq_zero nullMeasurableSet_univ
no goals
α : Type u_1
β : Type ?u.1651966
E : Type u_2
F : Type ?u.1651972
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
f g : α → E
s t : Set α
μ ν : Measure α
hf : IntegrableOn f s
h't : ∀ᵐ (x : α) ∂μ, ¬x ∈ s → f x = 0
⊢ ∀ᵐ (x : α) ∂μ, x ∈ univ \ s → f x = 0
filter_upwards [h't]with x hx h'x using hx h'x.2