Sets in sigma types

This file defines Set.sigma, the indexed sum of sets.

@[simp]

theorem Set.range_sigmaMk {ι : Type u_1} {α : ι → Type u_3} (i : ι) : Set.range (Sigma.mk i) = Sigma.fst ⁻¹' {i}

theorem Set.preimage_image_sigmaMk_of_ne {ι : Type u_1} {α : ι → Type u_3} {i : ι} {j : ι} (h : i ≠ j) (s : Set (α j)) : Sigma.mk i ⁻¹' (Sigma.mk j '' s) = ∅

theorem Set.image_sigmaMk_preimage_sigmaMap_subset {ι : Type u_1} {ι' : Type u_2} {α : ι → Type u_3} {β : ι' → Type u_5} (f : ι → ι') (g : (i : ι) → α i → β (f i)) (i : ι) (s : Set (β (f i))) : Sigma.mk i '' (g i ⁻¹' s) ⊆ Sigma.map f g ⁻¹' (Sigma.mk (f i) '' s)

theorem Set.image_sigmaMk_preimage_sigmaMap {ι : Type u_1} {ι' : Type u_2} {α : ι → Type u_3} {β : ι' → Type u_5} {f : ι → ι'} (hf : Function.Injective f) (g : (i : ι) → α i → β (f i)) (i : ι) (s : Set (β (f i))) : Sigma.mk i '' (g i ⁻¹' s) = Sigma.map f g ⁻¹' (Sigma.mk (f i) '' s)

def Set.sigma {ι : Type u_1} {α : ι → Type u_3} (s : Set ι) (t : (i : ι) → Set (α i)) : Set ((i : ι) × α i)

Indexed sum of sets. s.sigma t is the set of dependent pairs ⟨i, a⟩ such that i ∈ s and a ∈ t i.

Equations

• Set.sigma s t = {x : (i : ι) × α i | x.fst ∈ s ∧ x.snd ∈ t x.fst}

@[simp]

theorem Set.mem_sigma_iff {ι : Type u_1} {α : ι → Type u_3} {s : Set ι} {t : (i : ι) → Set (α i)} {x : (i : ι) × α i} : x ∈ Set.sigma s t ↔ x.fst ∈ s ∧ x.snd ∈ t x.fst

theorem Set.mk_sigma_iff {ι : Type u_1} {α : ι → Type u_3} {s : Set ι} {t : (i : ι) → Set (α i)} {i : ι} {a : α i} : { fst := i, snd := a } ∈ Set.sigma s t ↔ i ∈ s ∧ a ∈ t i

theorem Set.mk_mem_sigma {ι : Type u_1} {α : ι → Type u_3} {s : Set ι} {t : (i : ι) → Set (α i)} {i : ι} {a : α i} (hi : i ∈ s) (ha : a ∈ t i) : { fst := i, snd := a } ∈ Set.sigma s t

theorem Set.sigma_mono {ι : Type u_1} {α : ι → Type u_3} {s₁ : Set ι} {s₂ : Set ι} {t₁ : (i : ι) → Set (α i)} {t₂ : (i : ι) → Set (α i)} (hs : s₁ ⊆ s₂) (ht : ∀ (i : ι), t₁ i ⊆ t₂ i) : Set.sigma s₁ t₁ ⊆ Set.sigma s₂ t₂

theorem Set.sigma_subset_iff {ι : Type u_1} {α : ι → Type u_3} {s : Set ι} {t : (i : ι) → Set (α i)} {u : Set ((i : ι) × α i)} : Set.sigma s t ⊆ u ↔ ∀ ⦃i : ι⦄, i ∈ s → ∀ ⦃a : α i⦄, a ∈ t i → { fst := i, snd := a } ∈ u

theorem Set.forall_sigma_iff {ι : Type u_1} {α : ι → Type u_3} {s : Set ι} {t : (i : ι) → Set (α i)} {p : (i : ι) × α i → Prop} : (∀ x ∈ Set.sigma s t, p x) ↔ ∀ ⦃i : ι⦄, i ∈ s → ∀ ⦃a : α i⦄, a ∈ t i → p { fst := i, snd := a }

theorem Set.exists_sigma_iff {ι : Type u_1} {α : ι → Type u_3} {s : Set ι} {t : (i : ι) → Set (α i)} {p : (i : ι) × α i → Prop} : (∃ x ∈ Set.sigma s t, p x) ↔ ∃ i ∈ s, ∃ a ∈ t i, p { fst := i, snd := a }

@[simp]

theorem Set.sigma_empty {ι : Type u_1} {α : ι → Type u_3} {s : Set ι} : (Set.sigma s fun (i : ι) => ∅) = ∅

@[simp]

theorem Set.empty_sigma {ι : Type u_1} {α : ι → Type u_3} {t : (i : ι) → Set (α i)} : Set.sigma ∅ t = ∅

theorem Set.univ_sigma_univ {ι : Type u_1} {α : ι → Type u_3} {i : ι} : (Set.sigma Set.univ fun (x : ι) => Set.univ) = Set.univ

@[simp]

theorem Set.sigma_univ {ι : Type u_1} {α : ι → Type u_3} {s : Set ι} : (Set.sigma s fun (x : ι) => Set.univ) = Sigma.fst ⁻¹' s

@[simp]

theorem Set.singleton_sigma {ι : Type u_1} {α : ι → Type u_3} {t : (i : ι) → Set (α i)} {i : ι} {a : α i} : Set.sigma {i} t = Sigma.mk i '' t i

@[simp]

theorem Set.sigma_singleton {ι : Type u_1} {α : ι → Type u_3} {s : Set ι} {a : (i : ι) → α i} : (Set.sigma s fun (i : ι) => {a i}) = (fun (i : ι) => { fst := i, snd := a i }) '' s

theorem Set.singleton_sigma_singleton {ι : Type u_1} {α : ι → Type u_3} {i : ι} {a : (i : ι) → α i} : (Set.sigma {i} fun (i : ι) => {a i}) = {{ fst := i, snd := a i }}

@[simp]

theorem Set.union_sigma {ι : Type u_1} {α : ι → Type u_3} {s₁ : Set ι} {s₂ : Set ι} {t : (i : ι) → Set (α i)} : Set.sigma (s₁ ∪ s₂) t = Set.sigma s₁ t ∪ Set.sigma s₂ t

@[simp]

theorem Set.sigma_union {ι : Type u_1} {α : ι → Type u_3} {s : Set ι} {t₁ : (i : ι) → Set (α i)} {t₂ : (i : ι) → Set (α i)} : (Set.sigma s fun (i : ι) => t₁ i ∪ t₂ i) = Set.sigma s t₁ ∪ Set.sigma s t₂

theorem Set.sigma_inter_sigma {ι : Type u_1} {α : ι → Type u_3} {s₁ : Set ι} {s₂ : Set ι} {t₁ : (i : ι) → Set (α i)} {t₂ : (i : ι) → Set (α i)} : Set.sigma s₁ t₁ ∩ Set.sigma s₂ t₂ = Set.sigma (s₁ ∩ s₂) fun (i : ι) => t₁ i ∩ t₂ i

theorem biSup_sigma {ι : Type u_1} {α : ι → Type u_3} {β : Type u_5} [CompleteLattice β] (s : Set ι) (t : (i : ι) → Set (α i)) (f : Sigma α → β) : ⨆ ij ∈ Set.sigma s t, f ij = ⨆ i ∈ s, ⨆ j ∈ t i, f { fst := i, snd := j }

theorem biSup_sigma' {ι : Type u_1} {α : ι → Type u_3} {β : Type u_5} [CompleteLattice β] (s : Set ι) (t : (i : ι) → Set (α i)) (f : (i : ι) → α i → β) : ⨆ i ∈ s, ⨆ j ∈ t i, f i j = ⨆ ij ∈ Set.sigma s t, f ij.fst ij.snd

theorem biInf_sigma {ι : Type u_1} {α : ι → Type u_3} {β : Type u_5} [CompleteLattice β] (s : Set ι) (t : (i : ι) → Set (α i)) (f : Sigma α → β) : ⨅ ij ∈ Set.sigma s t, f ij = ⨅ i ∈ s, ⨅ j ∈ t i, f { fst := i, snd := j }

theorem biInf_sigma' {ι : Type u_1} {α : ι → Type u_3} {β : Type u_5} [CompleteLattice β] (s : Set ι) (t : (i : ι) → Set (α i)) (f : (i : ι) → α i → β) : ⨅ i ∈ s, ⨅ j ∈ t i, f i j = ⨅ ij ∈ Set.sigma s t, f ij.fst ij.snd

theorem Set.biUnion_sigma {ι : Type u_1} {α : ι → Type u_3} {β : Type u_6} (s : Set ι) (t : (i : ι) → Set (α i)) (f : Sigma α → Set β) : ⋃ ij ∈ Set.sigma s t, f ij = ⋃ i ∈ s, ⋃ j ∈ t i, f { fst := i, snd := j }

theorem Set.biUnion_sigma' {ι : Type u_1} {α : ι → Type u_3} {β : Type u_6} (s : Set ι) (t : (i : ι) → Set (α i)) (f : (i : ι) → α i → Set β) : ⋃ i ∈ s, ⋃ j ∈ t i, f i j = ⋃ ij ∈ Set.sigma s t, f ij.fst ij.snd

theorem Set.biInter_sigma {ι : Type u_1} {α : ι → Type u_3} {β : Type u_6} (s : Set ι) (t : (i : ι) → Set (α i)) (f : Sigma α → Set β) : ⋂ ij ∈ Set.sigma s t, f ij = ⋂ i ∈ s, ⋂ j ∈ t i, f { fst := i, snd := j }

theorem Set.biInter_sigma' {ι : Type u_1} {α : ι → Type u_3} {β : Type u_6} (s : Set ι) (t : (i : ι) → Set (α i)) (f : (i : ι) → α i → Set β) : ⋂ i ∈ s, ⋂ j ∈ t i, f i j = ⋂ ij ∈ Set.sigma s t, f ij.fst ij.snd

theorem Set.insert_sigma {ι : Type u_1} {α : ι → Type u_3} {s : Set ι} {t : (i : ι) → Set (α i)} {i : ι} {a : α i} : Set.sigma (insert i s) t = Sigma.mk i '' t i ∪ Set.sigma s t

theorem Set.sigma_insert {ι : Type u_1} {α : ι → Type u_3} {s : Set ι} {t : (i : ι) → Set (α i)} {a : (i : ι) → α i} : (Set.sigma s fun (i : ι) => insert (a i) (t i)) = (fun (i : ι) => { fst := i, snd := a i }) '' s ∪ Set.sigma s t

theorem Set.sigma_preimage_eq {ι : Type u_1} {ι' : Type u_2} {α : ι → Type u_3} {s : Set ι} {t : (i : ι) → Set (α i)} {β : ι → Type u_7} {f : ι' → ι} {g : (i : ι) → β i → α i} : (Set.sigma (f ⁻¹' s) fun (i : ι') => g (f i) ⁻¹' t (f i)) = (fun (p : (i : ι') × β (f i)) => { fst := f p.fst, snd := g (f p.fst) p.snd }) ⁻¹' Set.sigma s t

theorem Set.sigma_preimage_left {ι : Type u_1} {ι' : Type u_2} {α : ι → Type u_3} {s : Set ι} {t : (i : ι) → Set (α i)} {f : ι' → ι} : (Set.sigma (f ⁻¹' s) fun (i : ι') => t (f i)) = (fun (p : (i : ι') × α (f i)) => { fst := f p.fst, snd := p.snd }) ⁻¹' Set.sigma s t

theorem Set.sigma_preimage_right {ι : Type u_1} {α : ι → Type u_3} {s : Set ι} {t : (i : ι) → Set (α i)} {β : ι → Type u_7} {g : (i : ι) → β i → α i} : (Set.sigma s fun (i : ι) => g i ⁻¹' t i) = (fun (p : (i : ι) × β i) => { fst := p.fst, snd := g p.fst p.snd }) ⁻¹' Set.sigma s t

theorem Set.preimage_sigmaMap_sigma {ι : Type u_1} {ι' : Type u_2} {α : ι → Type u_3} {α' : ι' → Type u_8} (f : ι → ι') (g : (i : ι) → α i → α' (f i)) (s : Set ι') (t : (i : ι') → Set (α' i)) : Sigma.map f g ⁻¹' Set.sigma s t = Set.sigma (f ⁻¹' s) fun (i : ι) => g i ⁻¹' t (f i)

@[simp]

theorem Set.mk_preimage_sigma {ι : Type u_1} {α : ι → Type u_3} {s : Set ι} {t : (i : ι) → Set (α i)} {i : ι} (hi : i ∈ s) : Sigma.mk i ⁻¹' Set.sigma s t = t i

@[simp]

theorem Set.mk_preimage_sigma_eq_empty {ι : Type u_1} {α : ι → Type u_3} {s : Set ι} {t : (i : ι) → Set (α i)} {i : ι} (hi : i ∉ s) : Sigma.mk i ⁻¹' Set.sigma s t = ∅

theorem Set.mk_preimage_sigma_eq_if {ι : Type u_1} {α : ι → Type u_3} {s : Set ι} {t : (i : ι) → Set (α i)} {i : ι} [DecidablePred fun (x : ι) => x ∈ s] : Sigma.mk i ⁻¹' Set.sigma s t = if i ∈ s then t i else ∅

theorem Set.mk_preimage_sigma_fn_eq_if {ι : Type u_1} {α : ι → Type u_3} {s : Set ι} {t : (i : ι) → Set (α i)} {i : ι} {β : Type u_8} [DecidablePred fun (x : ι) => x ∈ s] (g : β → α i) : (fun (b : β) => { fst := i, snd := g b }) ⁻¹' Set.sigma s t = if i ∈ s then g ⁻¹' t i else ∅

theorem Set.sigma_univ_range_eq {ι : Type u_1} {α : ι → Type u_3} {β : ι → Type u_7} {f : (i : ι) → α i → β i} : (Set.sigma Set.univ fun (i : ι) => Set.range (f i)) = Set.range fun (x : (i : ι) × α i) => { fst := x.fst, snd := f x.fst x.snd }

theorem Set.Nonempty.sigma {ι : Type u_1} {α : ι → Type u_3} {s : Set ι} {t : (i : ι) → Set (α i)} : Set.Nonempty s → (∀ (i : ι), Set.Nonempty (t i)) → Set.Nonempty (Set.sigma s t)

theorem Set.Nonempty.sigma_fst {ι : Type u_1} {α : ι → Type u_3} {s : Set ι} {t : (i : ι) → Set (α i)} : Set.Nonempty (Set.sigma s t) → Set.Nonempty s

theorem Set.Nonempty.sigma_snd {ι : Type u_1} {α : ι → Type u_3} {s : Set ι} {t : (i : ι) → Set (α i)} : Set.Nonempty (Set.sigma s t) → ∃ i ∈ s, Set.Nonempty (t i)

theorem Set.sigma_nonempty_iff {ι : Type u_1} {α : ι → Type u_3} {s : Set ι} {t : (i : ι) → Set (α i)} : Set.Nonempty (Set.sigma s t) ↔ ∃ i ∈ s, Set.Nonempty (t i)

theorem Set.sigma_eq_empty_iff {ι : Type u_1} {α : ι → Type u_3} {s : Set ι} {t : (i : ι) → Set (α i)} : Set.sigma s t = ∅ ↔ ∀ i ∈ s, t i = ∅

theorem Set.image_sigmaMk_subset_sigma_left {ι : Type u_1} {α : ι → Type u_3} {s : Set ι} {t : (i : ι) → Set (α i)} {a : (i : ι) → α i} (ha : ∀ (i : ι), a i ∈ t i) : (fun (i : ι) => { fst := i, snd := a i }) '' s ⊆ Set.sigma s t

theorem Set.image_sigmaMk_subset_sigma_right {ι : Type u_1} {α : ι → Type u_3} {s : Set ι} {t : (i : ι) → Set (α i)} {i : ι} (hi : i ∈ s) : Sigma.mk i '' t i ⊆ Set.sigma s t

theorem Set.sigma_subset_preimage_fst {ι : Type u_1} {α : ι → Type u_3} (s : Set ι) (t : (i : ι) → Set (α i)) : Set.sigma s t ⊆ Sigma.fst ⁻¹' s

theorem Set.fst_image_sigma_subset {ι : Type u_1} {α : ι → Type u_3} (s : Set ι) (t : (i : ι) → Set (α i)) : Sigma.fst '' Set.sigma s t ⊆ s

theorem Set.fst_image_sigma {ι : Type u_1} {α : ι → Type u_3} {t : (i : ι) → Set (α i)} (s : Set ι) (ht : ∀ (i : ι), Set.Nonempty (t i)) : Sigma.fst '' Set.sigma s t = s

theorem Set.sigma_diff_sigma {ι : Type u_1} {α : ι → Type u_3} {s₁ : Set ι} {s₂ : Set ι} {t₁ : (i : ι) → Set (α i)} {t₂ : (i : ι) → Set (α i)} : Set.sigma s₁ t₁ \ Set.sigma s₂ t₂ = Set.sigma s₁ (t₁ \ t₂) ∪ Set.sigma (s₁ \ s₂) t₁