Source indexedlemma · leanprover/lean4:v4.32.0

pairwiseDisjoint_ℭ₁'

Carleson.Discrete.Defs · Carleson/Discrete/Defs.lean:146 to 155

Mathematical statement

Exact Lean statement

lemma pairwiseDisjoint_ℭ₁' :
    (univ : Set (ℕ × ℕ × ℕ)).PairwiseDisjoint (fun knj ↦ ℭ₁ (X := X) knj.1 knj.2.1 knj.2.2)

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma pairwiseDisjoint_ℭ₁' :    (univ : Set (ℕ × ℕ × ℕ)).PairwiseDisjoint (fun knj ↦ ℭ₁ (X := X) knj.1 knj.2.1 knj.2.2) := by  rintro ⟨k, n, j⟩ - ⟨k', n', j'⟩ - h  rcases ne_or_eq k k' with hkk' | rfl  · have := pairwiseDisjoint_ℭ (X := X) (mem_univ (k, n)) (mem_univ (k', n')) (by simp [hkk'])    exact this.mono ℭ₁_subset_ℭ ℭ₁_subset_ℭ  rcases ne_or_eq n n' with hnn' | rfl  · have := pairwiseDisjoint_ℭ (X := X) (mem_univ (k, n)) (mem_univ (k, n')) (by simp [hnn'])    exact this.mono ℭ₁_subset_ℭ ℭ₁_subset_ℭ  exact disjoint_ℭ₁_of_ne (by simpa using h)