Source indexedlemma · leanprover/lean4:v4.32.0

pairwiseDisjoint_iteratedMaximalSubfamily

Carleson.TileStructure · Carleson/TileStructure.lean:550 to 564

Mathematical statement

Exact Lean statement

lemma pairwiseDisjoint_iteratedMaximalSubfamily (A : Set (𝔓 X)) :
    univ.PairwiseDisjoint (iteratedMaximalSubfamily A)

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma pairwiseDisjoint_iteratedMaximalSubfamily (A : Set (𝔓 X)) :    univ.PairwiseDisjoint (iteratedMaximalSubfamily A) := by  intro m hm n hn hmn  wlog h'mn : m < n generalizing m n with H  · exact (H (mem_univ n) (mem_univ m) hmn.symm (by lia)).symm  have : iteratedMaximalSubfamily A n      ⊆ A \ ⋃ (i : {i | i < n}), iteratedMaximalSubfamily A i := by    conv_lhs => rw [iteratedMaximalSubfamily]    apply (exists_maximal_disjoint_covering_subfamily _).choose_spec.2.1  apply subset_compl_iff_disjoint_left.1  rw [compl_eq_univ_sdiff]  apply this.trans  apply sdiff_subset_sdiff (subset_univ _)  apply subset_iUnion_of_subset ⟨m, h'mn⟩  simp