α : Type u_1
β : Type ?u.1654027
E : Type u_2
F : Type ?u.1654033
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
f g : α → E
s t : Set α
μ ν : Measure α
h1s : support f ⊆ s
h : IntegrableOn f s
⊢ Integrable f
α : Type u_1
β : Type ?u.1654027
E : Type u_2
F : Type ?u.1654033
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
f g : α → E
s t : Set α
μ ν : Measure α
h1s : support f ⊆ s
⊢ IntegrableOn f s ↔ Integrable f
refine' ⟨fun h => _, fun h => h.integrableOn⟩
α : Type u_1
β : Type ?u.1654027
E : Type u_2
F : Type ?u.1654033
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
f g : α → E
s t : Set α
μ ν : Measure α
h1s : support f ⊆ s
h : IntegrableOn f s
x : α
hx : ¬x ∈ s
⊢ f x = 0
α : Type u_1
β : Type ?u.1654027
E : Type u_2
F : Type ?u.1654033
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
f g : α → E
s t : Set α
μ ν : Measure α
h1s : support f ⊆ s
h : IntegrableOn f s
⊢ Integrable f
refine h.integrable_of_forall_not_mem_eq_zero fun x hx => ?_
α : Type u_1
β : Type ?u.1654027
E : Type u_2
F : Type ?u.1654033
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
f g : α → E
s t : Set α
μ ν : Measure α
h1s : support f ⊆ s
h : IntegrableOn f s
x : α
hx : f x ≠ 0
⊢ x ∈ s
α : Type u_1
β : Type ?u.1654027
E : Type u_2
F : Type ?u.1654033
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
f g : α → E
s t : Set α
μ ν : Measure α
h1s : support f ⊆ s
h : IntegrableOn f s
x : α
hx : ¬x ∈ s
⊢ f x = 0
contrapose! hx
no goals
α : Type u_1
β : Type ?u.1654027
E : Type u_2
F : Type ?u.1654033
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
f g : α → E
s t : Set α
μ ν : Measure α
h1s : support f ⊆ s
h : IntegrableOn f s
x : α
hx : f x ≠ 0
⊢ x ∈ s
exact h1s (mem_support.2 hx)