Disjoint indexed families of sets

This file studies indexed unions of disjoint families of sets. It includes criteria for an indexed or set-indexed union to be disjoint from another set, a complement formula for a partition, and the natural maps and equivalences between an indexed union and the corresponding dependent sum.

Disjoint sets

@[simp]

theorem Set.disjoint_iUnion_left {α : Type u_1} {t : Set α} {ι : Sort u_5} {s : ι → Set α} : Disjoint (⋃ (i : ι), s i) t ↔ ∀ (i : ι), Disjoint (s i) t

@[simp]

theorem Set.disjoint_iUnion_right {α : Type u_1} {t : Set α} {ι : Sort u_5} {s : ι → Set α} : Disjoint t (⋃ (i : ι), s i) ↔ ∀ (i : ι), Disjoint t (s i)

theorem Set.disjoint_iUnion₂_left {α : Type u_1} {ι : Sort u_3} {κ : ι → Sort u_4} {s : (i : ι) → κ i → Set α} {t : Set α} : Disjoint (⋃ (i : ι), ⋃ (j : κ i), s i j) t ↔ ∀ (i : ι) (j : κ i), Disjoint (s i j) t

theorem Set.disjoint_iUnion₂_right {α : Type u_1} {ι : Sort u_3} {κ : ι → Sort u_4} {s : Set α} {t : (i : ι) → κ i → Set α} : Disjoint s (⋃ (i : ι), ⋃ (j : κ i), t i j) ↔ ∀ (i : ι) (j : κ i), Disjoint s (t i j)

@[simp]

theorem Set.disjoint_sUnion_left {α : Type u_1} {S : Set (Set α)} {t : Set α} : Disjoint (⋃₀ S) t ↔ ∀ s ∈ S, Disjoint s t

@[simp]

theorem Set.disjoint_sUnion_right {α : Type u_1} {s : Set α} {S : Set (Set α)} : Disjoint s (⋃₀ S) ↔ ∀ t ∈ S, Disjoint s t

theorem Set.biUnion_compl_eq_of_pairwise_disjoint_of_iUnion_eq_univ {α : Type u_1} {ι : Type u_5} {Es : ι → Set α} (Es_union : ⋃ (i : ι), Es i = univ) (Es_disj : Pairwise fun (i j : ι) => Disjoint (Es i) (Es j)) (I : Set ι) : (⋃ i ∈ I, Es i)ᶜ = ⋃ i ∈ Iᶜ, Es i

def Set.sigmaToiUnion {α : Type u_1} {β : Type u_2} (t : α → Set β) (x : (i : α) × ↑(t i)) : ↑(⋃ (i : α), t i)

If t is an indexed family of sets, then there is a natural map from Σ i, t i to ⋃ i, t i sending ⟨i, x⟩ to x.

Equations

• Set.sigmaToiUnion t x = ⟨↑x.snd, ⋯⟩

theorem Set.sigmaToiUnion_surjective {α : Type u_1} {β : Type u_2} (t : α → Set β) : Function.Surjective (sigmaToiUnion t)

theorem Set.sigmaToiUnion_injective {α : Type u_1} {β : Type u_2} (t : α → Set β) (h : Pairwise (Function.onFun Disjoint t)) : Function.Injective (sigmaToiUnion t)

theorem Set.sigmaToiUnion_bijective {α : Type u_1} {β : Type u_2} (t : α → Set β) (h : Pairwise (Function.onFun Disjoint t)) : Function.Bijective (sigmaToiUnion t)

noncomputable def Set.sigmaEquiv {α : Type u_1} {β : Type u_2} (s : α → Set β) (hs : ∀ (b : β), ∃! i : α, b ∈ s i) : (i : α) × ↑(s i) ≃ β

Equivalence from the disjoint union of a family of sets forming a partition of β, to β itself.

Equations

• Set.sigmaEquiv s hs = { toFun := fun (x : (i : α) × ↑(s i)) => match x with | ⟨fst, b⟩ => ↑b, invFun := fun (b : β) => ⟨Exists.choose ⋯, ⟨b, ⋯⟩⟩, left_inv := ⋯, right_inv := ⋯ }

noncomputable def Set.unionEqSigmaOfDisjoint {α : Type u_1} {β : Type u_2} {t : α → Set β} (h : Pairwise (Function.onFun Disjoint t)) : ↑(⋃ (i : α), t i) ≃ (i : α) × ↑(t i)

Equivalence between a disjoint union and a dependent sum.

Equations

• Set.unionEqSigmaOfDisjoint h = (Equiv.ofBijective (Set.sigmaToiUnion t) ⋯).symm

@[simp]

theorem Set.coe_unionEqSigmaOfDisjoint_symm_apply {α : Type u_5} {β : Type u_6} {t : α → Set β} (h : Pairwise (Function.onFun Disjoint t)) (x : (i : α) × ↑(t i)) : ↑((unionEqSigmaOfDisjoint h).symm x) = ↑x.snd

@[simp]

theorem Set.coe_snd_unionEqSigmaOfDisjoint {α : Type u_5} {β : Type u_6} {t : α → Set β} (h : Pairwise (Function.onFun Disjoint t)) (x : ↑(⋃ (i : α), t i)) : ↑((unionEqSigmaOfDisjoint h) x).snd = ↑x