Source indexedlemma · leanprover/lean4:v4.32.0

Complex.CartanBound.volume_Ioc_two_mul_diff_finset_ne_zero

PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.CartanBound · PrimeNumberTheoremAnd/Mathlib/Analysis/Complex/CartanBound.lean:600 to 610

Mathematical statement

Exact Lean statement

lemma volume_Ioc_two_mul_diff_finset_ne_zero (bad : Finset ℝ) {R : ℝ} (hR : 0 < R) :
    (volume : MeasureTheory.Measure ℝ) (Set.Ioc R (2 * R) \ (bad : Set ℝ)) ≠ 0

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma volume_Ioc_two_mul_diff_finset_ne_zero (bad : Finset ℝ) {R : ℝ} (hR : 0 < R) :    (volume : MeasureTheory.Measure ℝ) (Set.Ioc R (2 * R) \ (bad : Set ℝ)) ≠ 0 := by  have hbad_meas : (volume : MeasureTheory.Measure ℝ) (bad : Set ℝ) = 0 := by    simpa using (bad.measure_zero (μ := (volume : MeasureTheory.Measure ℝ)))  have hdiff :      (volume : MeasureTheory.Measure ℝ) (Set.Ioc R (2 * R) \ (bad : Set ℝ))        = (volume : MeasureTheory.Measure ℝ) (Set.Ioc R (2 * R)) := by    simpa [Set.sdiff_eq, Set.inter_assoc, Set.inter_left_comm, Set.inter_comm] using      (MeasureTheory.measure_sdiff_null (s := Set.Ioc R (2 * R)) (t := (bad : Set ℝ))        hbad_meas)  simpa [hdiff] using volume_Ioc_two_mul_ne_zero hR