# 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_6} {r : ααProp} {f : κSet α} (h : Directed (fun (x x_1 : Set α) => x x_1) f) :
(⋃ (n : κ), f n).Pairwise r ∀ (n : κ), (f n).Pairwise r
theorem Set.pairwise_sUnion {α : Type u_1} {r : ααProp} {s : Set (Set α)} (h : DirectedOn (fun (x x_1 : Set α) => x x_1) s) :
(⋃₀ s).Pairwise r as, a.Pairwise r
theorem Set.pairwiseDisjoint_iUnion {α : Type u_1} {ι : Type u_4} {ι' : Type u_5} [] [] {f : ια} {g : ι'Set ι} (h : Directed (fun (x x_1 : Set ι) => x x_1) g) :
(⋃ (n : ι'), g n).PairwiseDisjoint f ∀ ⦃n : ι'⦄, (g n).PairwiseDisjoint f
theorem Set.pairwiseDisjoint_sUnion {α : Type u_1} {ι : Type u_4} [] [] {f : ια} {s : Set (Set ι)} (h : DirectedOn (fun (x x_1 : Set ι) => x x_1) s) :
(⋃₀ s).PairwiseDisjoint f ∀ ⦃a : Set ι⦄, a sa.PairwiseDisjoint f
theorem Set.PairwiseDisjoint.biUnion {α : Type u_1} {ι : Type u_4} {ι' : Type u_5} [] {s : Set ι'} {g : ι'Set ι} {f : ια} (hs : s.PairwiseDisjoint fun (i' : ι') => ig i', f i) (hg : is, (g i).PairwiseDisjoint f) :
(⋃ is, 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_4} {ι' : Type u_5} [] {s : Set ι} {t : Set ι'} {f : ι × ι'α} (hs : s.PairwiseDisjoint fun (i : ι) => i't, f (i, i')) (ht : t.PairwiseDisjoint fun (i' : ι') => is, 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_4} {ι' : Type u_5} [] {s : Set ι} {t : Set ι'} {f : ι × ι'α} :
(s ×ˢ t).PairwiseDisjoint f (s.PairwiseDisjoint fun (i : ι) => i't, f (i, i')) t.PairwiseDisjoint fun (i' : ι') => is, f (i, i')
theorem Set.biUnion_diff_biUnion_eq {α : Type u_1} {ι : Type u_4} {s : Set ι} {t : Set ι} {f : ιSet α} (h : (s t).PairwiseDisjoint f) :
(⋃ is, f i) \ it, f i = is \ t, f i
noncomputable def Set.biUnionEqSigmaOfDisjoint {α : Type u_1} {ι : Type u_4} {s : Set ι} {f : ιSet α} (h : s.PairwiseDisjoint f) :
(⋃ is, f i) (i : s) × (f i)

Equivalence between a disjoint bounded union and a dependent sum.

Equations
Instances For
theorem Set.PairwiseDisjoint.subset_of_biUnion_subset_biUnion {α : Type u_1} {ι : Type u_4} {f : ιSet α} {s : Set ι} {t : Set ι} (h₀ : (s t).PairwiseDisjoint f) (h₁ : is, (f i).Nonempty) (h : is, f i it, f i) :
s t
theorem Pairwise.subset_of_biUnion_subset_biUnion {α : Type u_1} {ι : Type u_4} {f : ιSet α} {s : Set ι} {t : Set ι} (h₀ : Pairwise (Disjoint on f)) (h₁ : is, (f i).Nonempty) (h : is, f i it, f i) :
s t
theorem Pairwise.biUnion_injective {α : Type u_1} {ι : Type u_4} {f : ιSet α} (h₀ : Pairwise (Disjoint on f)) (h₁ : ∀ (i : ι), (f i).Nonempty) :
Function.Injective fun (s : Set ι) => is, f i
theorem pairwiseDisjoint_unique {α : Type u_1} {ι : Type u_4} {f : ιSet α} {s : Set ι} {y : α} (h_disjoint : s.PairwiseDisjoint f) (hy : y is, f i) :
∃! i : ι, i s y f i

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