Source indexedlemma · leanprover/lean4:v4.32.0

URel.eq

Carleson.Discrete.ForestUnion · Carleson/Discrete/ForestUnion.lean:196 to 205

Source documentation

Lemma 5.4.1, part 1.

Exact Lean statement

lemma URel.eq (hu : u ∈ 𝔘₂ k n j) (hu' : u' ∈ 𝔘₂ k n j) (huu' : URel k n j u u') : 𝓘 u = 𝓘 u'

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma URel.eq (hu : u ∈ 𝔘₂ k n j) (hu' : u' ∈ 𝔘₂ k n j) (huu' : URel k n j u u') : 𝓘 u = 𝓘 u' := by  by_cases e : u = u'; · rw [e]  have ndj := not_disjoint hu hu' huu'  have n₁ := (hu.1.2 _ hu'.1.1).mt ndj  rw [disjoint_comm] at ndj  have n₂ := (hu'.1.2 _ hu.1.1).mt ndj  simp_rw [URel, e, false_or, 𝔗₁, mem_setOf] at huu'; obtain ⟨p, ⟨_, _, sl₁⟩, sl₂⟩ := huu'  rcases le_or_gt (𝔰 u) (𝔰 u') with h | h  · exact eq_of_le_of_not_lt (Grid.le_dyadic h sl₁.1 sl₂.1) n₁  · exact (eq_of_le_of_not_lt (Grid.le_dyadic h.le sl₂.1 sl₁.1) n₂).symm