𝕜 : Type ?u.93658
M : Type ?u.93661
α : Type ?u.93664
G : Type u_1
E : Type ?u.93670
F : Type ?u.93673
inst✝¹⁰ : MeasurableSpace G
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace ℝ E
inst✝⁷ : CompleteSpace E
inst✝⁶ : NormedAddCommGroup F
μ : Measure G
f✝ : G → E
g : G
inst✝⁵ : TopologicalSpace G
inst✝⁴ : Group G
inst✝³ : TopologicalGroup G
inst✝² : BorelSpace G
inst✝¹ : IsMulLeftInvariant μ
inst✝ : Regular μ
hμ : μ ≠ 0
f : G → ℝ≥0∞
hf : Continuous f
this : IsOpenPosMeasure μ
⊢ (∫⁻ (x : G), f x ∂μ) = 0 ↔ f = 0
𝕜 : Type ?u.93658
M : Type ?u.93661
α : Type ?u.93664
G : Type u_1
E : Type ?u.93670
F : Type ?u.93673
inst✝¹⁰ : MeasurableSpace G
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace ℝ E
inst✝⁷ : CompleteSpace E
inst✝⁶ : NormedAddCommGroup F
μ : Measure G
f✝ : G → E
g : G
inst✝⁵ : TopologicalSpace G
inst✝⁴ : Group G
inst✝³ : TopologicalGroup G
inst✝² : BorelSpace G
inst✝¹ : IsMulLeftInvariant μ
inst✝ : Regular μ
hμ : μ ≠ 0
f : G → ℝ≥0∞
hf : Continuous f
⊢ (∫⁻ (x : G), f x ∂μ) = 0 ↔ f = 0
haveI := isOpenPosMeasure_of_mulLeftInvariant_of_regular hμ
no goals
𝕜 : Type ?u.93658
M : Type ?u.93661
α : Type ?u.93664
G : Type u_1
E : Type ?u.93670
F : Type ?u.93673
inst✝¹⁰ : MeasurableSpace G
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace ℝ E
inst✝⁷ : CompleteSpace E
inst✝⁶ : NormedAddCommGroup F
μ : Measure G
f✝ : G → E
g : G
inst✝⁵ : TopologicalSpace G
inst✝⁴ : Group G
inst✝³ : TopologicalGroup G
inst✝² : BorelSpace G
inst✝¹ : IsMulLeftInvariant μ
inst✝ : Regular μ
hμ : μ ≠ 0
f : G → ℝ≥0∞
hf : Continuous f
this : IsOpenPosMeasure μ
⊢ (∫⁻ (x : G), f x ∂μ) = 0 ↔ f = 0
rw [lintegral_eq_zero_iff hf.measurable, hf.ae_eq_iff_eq μ continuous_zero]