Source indexedlemma · leanprover/lean4:v4.32.0

czBall_subset_czPartition

Carleson.TwoSidedCarleson.WeakCalderonZygmund · Carleson/TwoSidedCarleson/WeakCalderonZygmund.lean:573 to 584

Mathematical statement

Exact Lean statement

lemma czBall_subset_czPartition {hX : GeneralCase f α} {i : ℕ} :
    czBall hX i ⊆ czPartition hX i

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma czBall_subset_czPartition {hX : GeneralCase f α} {i : ℕ} :    czBall hX i ⊆ czPartition hX i := by  intro r hr  rw [mem_ball] at hr  unfold czPartition  apply mem_sdiff_of_mem (by rw [mem_ball]; linarith [dist_nonneg.trans_lt hr])  simp only [mem_union, mem_iUnion, mem_ball, not_or, not_exists, not_lt]  refine ⟨?_, fun j hj ↦ by    refine le_of_not_gt (disjoint_left.mp (czBall_pairwiseDisjoint ?_ ?_ hj.ne) hr) <;> tauto⟩  unfold czPartition  simp only [Set.mem_sdiff, mem_ball, mem_union, mem_iUnion, not_or, not_and, not_not]  exact fun _ _ _ _ ↦ by use i