α : Type u_1
β : Type ?u.262207
E : Type ?u.262210
F : Type ?u.262213
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
f✝ g : α → E
s t : Set α
μ ν : Measure α
l l' : Filter α
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
f : α → ℝ
hf : 0 ≤ᵐ[Measure.restrict μ s] f
hfi : IntegrableOn f s
⊢ NullMeasurableSet (support f)
α : Type u_1
β : Type ?u.262207
E : Type ?u.262210
F : Type ?u.262213
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
f✝ g : α → E
s t : Set α
μ ν : Measure α
l l' : Filter α
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
f : α → ℝ
hf : 0 ≤ᵐ[Measure.restrict μ s] f
hfi : IntegrableOn f s
⊢ (0 < ∫ (x : α) in s, f x ∂μ) ↔ 0 < ↑↑μ (support f ∩ s)
rw [integral_pos_iff_support_of_nonneg_ae hf hfi, Measure.restrict_apply₀]
α : Type u_1
β : Type ?u.262207
E : Type ?u.262210
F : Type ?u.262213
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
f✝ g : α → E
s t : Set α
μ ν : Measure α
l l' : Filter α
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
f : α → ℝ
hf : 0 ≤ᵐ[Measure.restrict μ s] f
hfi : IntegrableOn f s
⊢ NullMeasurableSet (f ⁻¹' {0}ᶜ)
α : Type u_1
β : Type ?u.262207
E : Type ?u.262210
F : Type ?u.262213
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
f✝ g : α → E
s t : Set α
μ ν : Measure α
l l' : Filter α
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
f : α → ℝ
hf : 0 ≤ᵐ[Measure.restrict μ s] f
hfi : IntegrableOn f s
⊢ NullMeasurableSet (support f)
rw [support_eq_preimage]
no goals
α : Type u_1
β : Type ?u.262207
E : Type ?u.262210
F : Type ?u.262213
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
f✝ g : α → E
s t : Set α
μ ν : Measure α
l l' : Filter α
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
f : α → ℝ
hf : 0 ≤ᵐ[Measure.restrict μ s] f
hfi : IntegrableOn f s
⊢ NullMeasurableSet (f ⁻¹' {0}ᶜ)
exact hfi.aestronglyMeasurable.aemeasurable.nullMeasurable (measurableSet_singleton 0).compl