Source indexedlemma · leanprover/lean4:v4.32.0

ordConnected_C

Carleson.Discrete.ForestUnion · Carleson/Discrete/ForestUnion.lean:36 to 45

Source documentation

Lemma 5.3.5

Exact Lean statement

lemma ordConnected_C : OrdConnected (ℭ k n : Set (𝔓 X))

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma ordConnected_C : OrdConnected (ℭ k n : Set (𝔓 X)) := by  rw [ordConnected_def]; intro p mp p'' mp'' p' mp'  rw [ℭ, mem_setOf] at mp mp'' ⊢  have z := mem_of_mem_of_subset mp' (ordConnected_tilesAt.out mp.1 mp''.1)  refine ⟨z, ?_⟩  have hk : ∀ q' ∈ TilesAt (X := X) k, ∀ q ≤ q', dens' k {q'} ≤ dens' k {q} := fun q' _ q hq ↦ by    simp_rw [dens', mem_singleton_iff, iSup_iSup_eq_left]; gcongr with l hl a _    exact iSup_const_mono fun h ↦      wiggle_order_11_10 hq (C5_3_3_le (X := X).trans (by norm_num) |>.trans hl) |>.trans h  exact ⟨mp''.2.1.trans_le (hk _ mp''.1 _ mp'.2), (hk _ z _ mp'.1).trans mp.2.2⟩