Relations holding pairwise

In this file we prove many facts about Pairwise and the set lattice.

theorem Set.pairwise_iUnion {α : Type u_1} {κ : Sort u_4} {r : α → α → Prop} {f : κ → Set α} (hd : Directed (fun (x1 x2 : Set α) => x1 ⊆ x2) f) : (⋃ (n : κ), f n).Pairwise r ↔ ∀ (n : κ), (f n).Pairwise r

theorem Set.pairwise_iUnion₂ {α : Type u_1} {s : Set (Set α)} (hd : DirectedOn (fun (x1 x2 : Set α) => x1 ⊆ x2) s) (r : α → α → Prop) (h : ∀ a ∈ s, a.Pairwise r) : (⋃ a ∈ s, a).Pairwise r

theorem Set.pairwise_iUnion₂_iff {α : Type u_1} {r : α → α → Prop} {s : Set (Set α)} (hd : DirectedOn (fun (x1 x2 : Set α) => x1 ⊆ x2) s) : (⋃ a ∈ s, a).Pairwise r ↔ ∀ a ∈ s, a.Pairwise r

theorem Set.pairwise_sUnion {α : Type u_1} {r : α → α → Prop} {s : Set (Set α)} (hd : DirectedOn (fun (x1 x2 : Set α) => x1 ⊆ x2) s) : (⋃₀ s).Pairwise r ↔ ∀ a ∈ s, a.Pairwise r

theorem Set.pairwiseDisjoint_iUnion {α : Type u_1} {ι : Type u_2} {ι' : Type u_3} [PartialOrder α] [OrderBot α] {f : ι → α} {g : ι' → Set ι} (h : Directed (fun (x1 x2 : Set ι) => x1 ⊆ x2) g) : (⋃ (n : ι'), g n).PairwiseDisjoint f ↔ ∀ ⦃n : ι'⦄, (g n).PairwiseDisjoint f

theorem Set.pairwiseDisjoint_sUnion {α : Type u_1} {ι : Type u_2} [PartialOrder α] [OrderBot α] {f : ι → α} {s : Set (Set ι)} (h : DirectedOn (fun (x1 x2 : Set ι) => x1 ⊆ x2) s) : (⋃₀ s).PairwiseDisjoint f ↔ ∀ ⦃a : Set ι⦄, a ∈ s → a.PairwiseDisjoint f

theorem Set.PairwiseDisjoint.biUnion {α : Type u_1} {ι : Type u_2} {ι' : Type u_3} [CompleteLattice α] {s : Set ι'} {g : ι' → Set ι} {f : ι → α} (hs : s.PairwiseDisjoint fun (i' : ι') => ⨆ i ∈ g i', f i) (hg : ∀ i ∈ s, (g i).PairwiseDisjoint f) : (⋃ i ∈ s, g i).PairwiseDisjoint f

Bind operation for Set.PairwiseDisjoint. If you want to only consider finsets of indices, you can use Set.PairwiseDisjoint.biUnion_finset.

theorem Set.PairwiseDisjoint.prod_left {α : Type u_1} {ι : Type u_2} {ι' : Type u_3} [CompleteLattice α] {s : Set ι} {t : Set ι'} {f : ι × ι' → α} (hs : s.PairwiseDisjoint fun (i : ι) => ⨆ i' ∈ t, f (i, i')) (ht : t.PairwiseDisjoint fun (i' : ι') => ⨆ i ∈ s, f (i, i')) : (s ×ˢ t).PairwiseDisjoint f

If the suprema of columns are pairwise disjoint and suprema of rows as well, then everything is pairwise disjoint. Not to be confused with Set.PairwiseDisjoint.prod.

theorem Set.pairwiseDisjoint_prod_left {α : Type u_1} {ι : Type u_2} {ι' : Type u_3} [Order.Frame α] {s : Set ι} {t : Set ι'} {f : ι × ι' → α} : (s ×ˢ t).PairwiseDisjoint f ↔ (s.PairwiseDisjoint fun (i : ι) => ⨆ i' ∈ t, f (i, i')) ∧ t.PairwiseDisjoint fun (i' : ι') => ⨆ i ∈ s, f (i, i')

theorem Set.biUnion_sdiff_biUnion_eq {α : Type u_1} {ι : Type u_2} {s t : Set ι} {f : ι → Set α} (h : (s ∪ t).PairwiseDisjoint f) : (⋃ i ∈ s, f i) \ ⋃ i ∈ t, f i = ⋃ i ∈ s \ t, f i

@[deprecated Set.biUnion_sdiff_biUnion_eq (since := "2026-06-03")]

theorem Set.biUnion_diff_biUnion_eq {α : Type u_1} {ι : Type u_2} {s t : Set ι} {f : ι → Set α} (h : (s ∪ t).PairwiseDisjoint f) : (⋃ i ∈ s, f i) \ ⋃ i ∈ t, f i = ⋃ i ∈ s \ t, f i

Alias of Set.biUnion_sdiff_biUnion_eq.

noncomputable def Set.biUnionEqSigmaOfDisjoint {α : Type u_1} {ι : Type u_2} {s : Set ι} {f : ι → Set α} (h : s.PairwiseDisjoint f) : ↑(⋃ i ∈ s, f i) ≃ (i : ↑s) × ↑(f ↑i)

Equivalence between a disjoint bounded union and a dependent sum.

Equations

• Set.biUnionEqSigmaOfDisjoint h = (Set.equivOfEq ⋯).trans (Set.unionEqSigmaOfDisjoint ⋯)

@[simp]

theorem Set.coe_biUnionEqSigmaOfDisjoint_symm_apply {α : Type u_5} {ι : Type u_6} {s : Set ι} {f : ι → Set α} (h : s.PairwiseDisjoint f) (x : (i : ↑s) × ↑(f ↑i)) : ↑((biUnionEqSigmaOfDisjoint h).symm x) = ↑x.snd

@[simp]

theorem Set.coe_snd_biUnionEqSigmaOfDisjoint {α : Type u_5} {ι : Type u_6} {s : Set ι} {f : ι → Set α} (h : s.PairwiseDisjoint f) (x : ↑(⋃ i ∈ s, f i)) : ↑((biUnionEqSigmaOfDisjoint h) x).snd = ↑x

theorem Set.pairwiseDisjoint_iff {α : Type u_1} {ι : Type u_2} {f : ι → Set α} {s : Set ι} : s.PairwiseDisjoint f ↔ ∀ ⦃i : ι⦄, i ∈ s → ∀ ⦃j : ι⦄, j ∈ s → (f i ∩ f j).Nonempty → i = j

theorem Set.pairwiseDisjoint_pair_insert {α : Type u_1} {s : Set α} {a : α} (ha : a ∉ s) : (𝒫 s).PairwiseDisjoint fun (t : Set α) => {t, insert a t}

theorem Set.PairwiseDisjoint.subset_of_biUnion_subset_biUnion {α : Type u_1} {ι : Type u_2} {f : ι → Set α} {s t : Set ι} (h₀ : (s ∪ t).PairwiseDisjoint f) (h₁ : ∀ i ∈ s, (f i).Nonempty) (h : ⋃ i ∈ s, f i ⊆ ⋃ i ∈ t, f i) : s ⊆ t

theorem Pairwise.subset_of_biUnion_subset_biUnion {α : Type u_1} {ι : Type u_2} {f : ι → Set α} {s t : Set ι} (h₀ : Pairwise (Function.onFun Disjoint f)) (h₁ : ∀ i ∈ s, (f i).Nonempty) (h : ⋃ i ∈ s, f i ⊆ ⋃ i ∈ t, f i) : s ⊆ t

theorem Pairwise.biUnion_injective {α : Type u_1} {ι : Type u_2} {f : ι → Set α} (h₀ : Pairwise (Function.onFun Disjoint f)) (h₁ : ∀ (i : ι), (f i).Nonempty) : Function.Injective fun (s : Set ι) => ⋃ i ∈ s, f i

theorem pairwiseDisjoint_unique {α : Type u_1} {ι : Type u_2} {f : ι → Set α} {s : Set ι} {y : α} (h_disjoint : s.PairwiseDisjoint f) (hy : y ∈ ⋃ i ∈ s, f i) : ∃! i : ι, i ∈ s ∧ y ∈ f i

In a disjoint union we can identify the unique set an element belongs to.