Source indexedlemma · leanprover/lean4:v4.32.0

TileStructure.Forest.pairwiseDisjoint_rowDecomp

Carleson.ForestOperator.Forests · Carleson/ForestOperator/Forests.lean:329 to 344

Source documentation

Part of Lemma 7.7.1

Exact Lean statement

lemma pairwiseDisjoint_rowDecomp :
    (Iio (2 ^ n)).PairwiseDisjoint (rowDecomp t · : ℕ → Set (𝔓 X))

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma pairwiseDisjoint_rowDecomp :    (Iio (2 ^ n)).PairwiseDisjoint (rowDecomp t · : ℕ → Set (𝔓 X)) := by  intro i hi j hj hne  rw [onFun_apply,Set.disjoint_iff]  wlog hij : i < j  · rw [Set.inter_comm]    apply this hj hi hne.symm    lia  intro x hx  obtain ⟨hx₁,hx₂⟩ := hx  revert hx₁  simp only [mem_𝔘, mem_empty_iff_false, imp_false]  rw [rowDecomp_𝔘_eq t j] at hx₂  have := ((rowDecomp_𝔘_subset t j) hx₂).right  simp_rw [mem_iUnion, exists_prop, not_exists, not_and] at this  exact this i hij