Source indexedlemma · leanprover/lean4:v4.32.0

ordConnected_C3

Carleson.Discrete.ForestUnion · Carleson/Discrete/ForestUnion.lean:84 to 92

Source documentation

Lemma 5.3.8

Exact Lean statement

lemma ordConnected_C3 : OrdConnected (ℭ₃ k n j : Set (𝔓 X))

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma ordConnected_C3 : OrdConnected (ℭ₃ k n j : Set (𝔓 X)) := by  rw [ordConnected_def]; intro p mp p'' mp'' p' mp'  have mp₁ := mem_of_mem_of_subset mp ℭ₃_subset_ℭ₂  have mp''₁ := mem_of_mem_of_subset mp'' ℭ₃_subset_ℭ₂  have mp'₁ : p' ∈ ℭ₂ (X := X) k n j := mem_of_mem_of_subset mp' (ordConnected_C2.out mp₁ mp''₁)  rw [ℭ₃_def] at mp'' ⊢  obtain ⟨-, u, mu, 𝓘nu, su⟩ := mp''; refine ⟨mp'₁, ⟨u, mu, ?_⟩⟩  exact ⟨(mp'.2.1.trans_lt (lt_of_le_of_ne su.1 𝓘nu)).ne,    (wiggle_order_11_10 mp'.2 (C5_3_3_le (X := X).trans (by norm_num))).trans su⟩