Source indexedlemma · leanprover/lean4:v4.32.0

Complex.CartanBound.restrict_volume_Ioc_two_mul_diff_finset_ne_zero

PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.CartanBound · PrimeNumberTheoremAnd/Mathlib/Analysis/Complex/CartanBound.lean:612 to 622

Mathematical statement

Exact Lean statement

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

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma restrict_volume_Ioc_two_mul_diff_finset_ne_zero (bad : Finset ℝ) {R : ℝ} (hR : 0 < R) :    (volume.restrict (Set.Ioc R (2 * R))) (Set.Ioc R (2 * R) \ (bad : Set ℝ)) ≠ 0 := by  have hsubset : Set.Ioc R (2 * R) \ (bad : Set ℝ) ⊆ Set.Ioc R (2 * R) := by    intro r hr    exact hr.1  have hinter :      (Set.Ioc R (2 * R) \ (bad : Set ℝ)) ∩ Set.Ioc R (2 * R)        = (Set.Ioc R (2 * R) \ (bad : Set ℝ)) := by    exact Set.inter_eq_left.mpr hsubset  simpa [MeasureTheory.Measure.restrict_apply, measurableSet_Ioc, hinter] using    volume_Ioc_two_mul_diff_finset_ne_zero bad hR