Skip to main content
therefore
Sign inSign up
Open navigation
fpvandoorn/carleson
Source indexedlemma Β· leanprover/lean4:v4.32.0

forest_convex

Carleson.Discrete.ForestUnion Β· Carleson/Discrete/ForestUnion.lean:356 to 370

Source documentation

Lemma 5.4.5, verifying (2.0.33)

Exact Lean statement

lemma forest_convex : OrdConnected (𝔗₂ k n j u)

Complete declaration

Lean source

Canonical source
Full Lean sourceLean 4
lemma forest_convex : OrdConnected (𝔗₂ k n j u) := by  rw [ordConnected_def]; intro p mp p'' mp'' p' mp'  have mp'β‚… : p' ∈ β„­β‚… (X := X) k n j :=    (ordConnected_C5.out ((𝔗₂_subset_ℭ₆.trans ℭ₆_subset_β„­β‚…) mp)      ((𝔗₂_subset_ℭ₆.trans ℭ₆_subset_β„­β‚…) mp'')) mp'  have mp'₆ : p' ∈ ℭ₆ k n j := by    have hp := 𝔗₂_subset_ℭ₆ mp; rw [ℭ₆, mem_setOf] at hp ⊒    refine ⟨mp'β‚…, ?_⟩; have hpG := hp.2; contrapose! hpG    exact mp'.1.1.1.trans hpG  simp_rw [𝔗₂, mem_inter_iff, mp'₆, true_and, mem_iUnionβ‚‚, mem_iUnion] at mp'' ⊒  obtain ⟨u', mu', ru, _, np'', sl⟩ := mp''.2  have pnu : π“˜ p' < π“˜ u' := (mp'.2.1).trans_lt (lt_of_le_of_ne sl.1 np'')  use u', mu', ru; rw [𝔗₁, mem_setOf]  use (β„­β‚…_subset_β„­β‚„ |>.trans β„­β‚„_subset_ℭ₃ |>.trans ℭ₃_subset_β„­β‚‚ |>.trans β„­β‚‚_subset_ℭ₁) mp'β‚…, pnu.ne  exact (wiggle_order_11_10 mp'.2 (C5_3_3_le (X := X).trans (by norm_num))).trans sl