Source indexedlemma · leanprover/lean4:v4.32.0

mem_iUnion_iff_mem_of_mem_ℭ

Carleson.Discrete.ForestComplement · Carleson/Discrete/ForestComplement.lean:198 to 206

Source documentation

Lemma allowing to peel ⋃ (n : ℕ) (k ≤ n) from unions in the proof of Lemma 5.5.1.

Exact Lean statement

lemma mem_iUnion_iff_mem_of_mem_ℭ {f : ℕ → ℕ → Set (𝔓 X)} (hp : p ∈ ℭ k n ∧ k ≤ n)
    (hf : ∀ k n, f k n ⊆ ℭ k n) : p ∈ ⋃ (n : ℕ) (k ≤ n), f k n ↔ p ∈ f k n

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma mem_iUnion_iff_mem_of_mem_ℭ {f : ℕ → ℕ → Set (𝔓 X)} (hp : p ∈ ℭ k n ∧ k ≤ n)    (hf : ∀ k n, f k n ⊆ ℭ k n) : p ∈ ⋃ (n : ℕ) (k ≤ n), f k n ↔ p ∈ f k n := by  simp_rw [mem_iUnion]; constructor <;> intro h  · obtain ⟨n', k', _, mp⟩ := h    have e := pairwiseDisjoint_ℭ (X := X).elim (mem_univ (k, n)) (mem_univ (k', n'))      (not_disjoint_iff.mpr ⟨p, hp.1, hf k' n' mp⟩)    rw [Prod.mk_inj] at e    exact e.1 ▸ e.2 ▸ mp  · use n, k, hp.2