Skip to main content
therefore
Sign inSign up
Open navigation
fpvandoorn/carleson
Source indexedlemma ยท leanprover/lean4:v4.32.0

exists_Eโ‚‚_volume_pos_of_mem_๐”“pos

Carleson.Discrete.ForestComplement ยท Carleson/Discrete/ForestComplement.lean:83 to 91

Mathematical statement

Exact Lean statement

lemma exists_Eโ‚‚_volume_pos_of_mem_๐”“pos (h : p โˆˆ ๐”“pos (X := X)) : โˆƒ r : โ„•, 0 < volume (Eโ‚‚ r p)

Complete declaration

Lean source

Canonical source
Full Lean sourceLean 4
lemma exists_Eโ‚‚_volume_pos_of_mem_๐”“pos (h : p โˆˆ ๐”“pos (X := X)) : โˆƒ r : โ„•, 0 < volume (Eโ‚‚ r p) := by  apply exists_measure_pos_of_not_measure_iUnion_null  change volume (โ‹ƒ n : โ„•, ๐“˜ p โˆฉ G โˆฉ Q โปยน' ball_(p) (๐’ฌ p) n) โ‰  0  rw [โ† inter_iUnion]  suffices โ‹ƒ i : โ„•, Q โปยน' ball_(p) (๐’ฌ p) i = univ by    rw [this, inter_univ, โ† pos_iff_ne_zero]    rw [๐”“pos, mem_setOf] at h; exact h.trans_le (measure_mono inter_subset_left)  simp_rw [iUnion_eq_univ_iff, mem_preimage]  exact fun x โ†ฆ exists_nat_gt (dist_(p) (Q x) (๐’ฌ p))