Source indexedlemma · leanprover/lean4:v4.32.0

ordConnected_C5

Carleson.Discrete.ForestUnion · Carleson/Discrete/ForestUnion.lean:111 to 118

Source documentation

Lemma 5.3.10

Exact Lean statement

lemma ordConnected_C5 : OrdConnected (ℭ₅ k n j : Set (𝔓 X))

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma ordConnected_C5 : 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'₁ : p' ∈ ℭ₄ (X := X) k n j := mem_of_mem_of_subset mp'    (ordConnected_C4.out mp₁ (mem_of_mem_of_subset mp'' ℭ₅_subset_ℭ₄))  simp_rw [ℭ₅, mem_sdiff, mp₁, mp'₁, true_and, 𝔏₄, mem_setOf,    mp₁, mp'₁, true_and] at mp ⊢  contrapose! mp; obtain ⟨u, mu, s𝓘u⟩ := mp; use u, mu, mp'.1.1.1.trans s𝓘u