Source indexedlemma · leanprover/lean4:v4.32.0

TileStructure.Forest.rowDecomp_zornset_chain_Union_bound

Carleson.ForestOperator.Forests · Carleson/ForestOperator/Forests.lean:167 to 177

Mathematical statement

Exact Lean statement

lemma rowDecomp_zornset_chain_Union_bound (s' : Set (𝔓 X)) {c : Set (Set (𝔓 X))} (hc : c ⊆ rowDecomp_zornset s')
    (hc_chain : IsChain (· ⊆ ·) c) :
    (⋃ s ∈ c,s) ∈ rowDecomp_zornset s' ∧ ∀ s ∈ c, s ⊆ ⋃ s'' ∈ c, s''

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma rowDecomp_zornset_chain_Union_bound (s' : Set (𝔓 X)) {c : Set (Set (𝔓 X))} (hc : c ⊆ rowDecomp_zornset s')    (hc_chain : IsChain (· ⊆ ·) c) :    (⋃ s ∈ c,s) ∈ rowDecomp_zornset s' ∧ ∀ s ∈ c, s ⊆ ⋃ s'' ∈ c, s'' := by  simp_rw [rowDecomp_zornset,subset_inter_iff] at hc ⊢  obtain ⟨⟨hc₁,hc₂⟩,hc₃⟩ := hc  simp_rw [mem_inter_iff,mem_setOf]  repeat constructor  · exact iUnion₂_subset_iff.mpr hc₁  · exact (hc_chain.pairwiseDisjoint_iUnion₂ _).mpr hc₂  · exact iUnion₂_subset_iff.mpr hc₃  · exact fun s hs ↦ subset_iUnion₂_of_subset s hs subset_rfl