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 α} (h : Directed (fun (x1 x2 : Set α) => x1 ⊆ x2) 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 (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_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

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 = (Equiv.setCongr ⋯).trans (Set.unionEqSigmaOfDisjoint ⋯)

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 (Disjoint on 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 (Disjoint on 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.