# Sets in sigma types #

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

source
@[simp]
theorem Set.range_sigmaMk {ι : Type u_1} {α : ι → Type u_3} (i : ι) :
range (Sigma.mk i) = Sigma.fst ⁻¹' {i}
source
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) = ∅
source
theorem Set.image_sigmaMk_preimage_sigmaMap_subset {ι : Type u_1} {ι' : Type u_2} {α : ι → Type u_3} {β : ι' → Type u_4} (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)
source
theorem Set.image_sigmaMk_preimage_sigmaMap {ι : Type u_1} {ι' : Type u_2} {α : ι → Type u_3} {β : ι' → Type u_4} {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)
source
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

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

Instances For

source
@[simp]
theorem Set.mem_sigma_iff {ι : Type u_1} {α : ι → Type u_3} {s : Set ι} {t : (i : ι) → Set (α i)} {x : (i : ι) × α i} :
x ∈ s.sigma t ↔ x.fst ∈ s ∧ x.snd ∈ t x.fst
source
theorem Set.mk_sigma_iff {ι : Type u_1} {α : ι → Type u_3} {s : Set ι} {t : (i : ι) → Set (α i)} {i : ι} {a : α i} :
⟨i, a⟩ ∈ s.sigma t ↔ i ∈ s ∧ a ∈ t i
source
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) :
⟨i, a⟩ ∈ s.sigma t
source
theorem Set.sigma_mono {ι : Type u_1} {α : ι → Type u_3} {s₁ s₂ : Set ι} {t₁ t₂ : (i : ι) → Set (α i)} (hs : s₁ ⊆ s₂) (ht : ∀ (i : ι), t₁ i ⊆ t₂ i) :
s₁.sigma t₁ ⊆ s₂.sigma t₂
source
theorem Set.sigma_subset_iff {ι : Type u_1} {α : ι → Type u_3} {s : Set ι} {t : (i : ι) → Set (α i)} {u : Set ((i : ι) × α i)} :
s.sigma t ⊆ u ↔ ∀ ⦃i : ι⦄, i ∈ s → ∀ ⦃a : α i⦄, a ∈ t i → ⟨i, a⟩ ∈ u
source
theorem Set.forall_sigma_iff {ι : Type u_1} {α : ι → Type u_3} {s : Set ι} {t : (i : ι) → Set (α i)} {p : (i : ι) × α i → Prop} :
(∀ x ∈ s.sigma t, p x) ↔ ∀ ⦃i : ι⦄, i ∈ s → ∀ ⦃a : α i⦄, a ∈ t i → p ⟨i, a⟩
source
theorem Set.exists_sigma_iff {ι : Type u_1} {α : ι → Type u_3} {s : Set ι} {t : (i : ι) → Set (α i)} {p : (i : ι) × α i → Prop} :
(∃ x ∈ s.sigma t, p x) ↔ ∃ i ∈ s, ∃ a ∈ t i, p ⟨i, a⟩
source
@[simp]
theorem Set.sigma_empty {ι : Type u_1} {α : ι → Type u_3} {s : Set ι} :
(s.sigma fun (i : ι) => ∅) = ∅
source
@[simp]
theorem Set.empty_sigma {ι : Type u_1} {α : ι → Type u_3} {t : (i : ι) → Set (α i)} :
∅.sigma t = ∅
source
theorem Set.univ_sigma_univ {ι : Type u_1} {α : ι → Type u_3} {i : ι} :
(univ.sigma fun (x : ι) => univ) = univ
source
@[simp]
theorem Set.sigma_univ {ι : Type u_1} {α : ι → Type u_3} {s : Set ι} :
(s.sigma fun (x : ι) => univ) = Sigma.fst ⁻¹' s
source
@[simp]
theorem Set.univ_sigma_preimage_mk {ι : Type u_1} {α : ι → Type u_3} (s : Set ((i : ι) × α i)) :
(univ.sigma fun (i : ι) => Sigma.mk i ⁻¹' s) = s
source
@[simp]
theorem Set.singleton_sigma {ι : Type u_1} {α : ι → Type u_3} {t : (i : ι) → Set (α i)} {i : ι} :
{i}.sigma t = Sigma.mk i '' t i
source
@[simp]
theorem Set.sigma_singleton {ι : Type u_1} {α : ι → Type u_3} {s : Set ι} {a : (i : ι) → α i} :
(s.sigma fun (i : ι) => {a i}) = (fun (i : ι) => ⟨i, a i⟩) '' s
source
theorem Set.singleton_sigma_singleton {ι : Type u_1} {α : ι → Type u_3} {i : ι} {a : (i : ι) → α i} :
({i}.sigma fun (i : ι) => {a i}) = {⟨i, a i⟩}
source
@[simp]
theorem Set.union_sigma {ι : Type u_1} {α : ι → Type u_3} {s₁ s₂ : Set ι} {t : (i : ι) → Set (α i)} :
(s₁ ∪ s₂).sigma t = s₁.sigma t ∪ s₂.sigma t
source
@[simp]
theorem Set.sigma_union {ι : Type u_1} {α : ι → Type u_3} {s : Set ι} {t₁ t₂ : (i : ι) → Set (α i)} :
(s.sigma fun (i : ι) => t₁ i ∪ t₂ i) = s.sigma t₁ ∪ s.sigma t₂
source
theorem Set.sigma_inter_sigma {ι : Type u_1} {α : ι → Type u_3} {s₁ s₂ : Set ι} {t₁ t₂ : (i : ι) → Set (α i)} :
s₁.sigma t₁ ∩ s₂.sigma t₂ = (s₁ ∩ s₂).sigma fun (i : ι) => t₁ i ∩ t₂ i
source
theorem biSup_sigma {ι : Type u_1} {α : ι → Type u_3} {β : Type u_4} [CompleteLattice β] (s : Set ι) (t : (i : ι) → Set (α i)) (f : Sigma α → β) :
⨆ ij ∈ s.sigma t, f ij = ⨆ i ∈ s, ⨆ j ∈ t i, f ⟨i, j⟩
source
theorem biSup_sigma' {ι : Type u_1} {α : ι → Type u_3} {β : Type u_4} [CompleteLattice β] (s : Set ι) (t : (i : ι) → Set (α i)) (f : (i : ι) → α i → β) :
⨆ i ∈ s, ⨆ j ∈ t i, f i j = ⨆ ij ∈ s.sigma t, f ij.fst ij.snd
source
theorem biInf_sigma {ι : Type u_1} {α : ι → Type u_3} {β : Type u_4} [CompleteLattice β] (s : Set ι) (t : (i : ι) → Set (α i)) (f : Sigma α → β) :
⨅ ij ∈ s.sigma t, f ij = ⨅ i ∈ s, ⨅ j ∈ t i, f ⟨i, j⟩
source
theorem biInf_sigma' {ι : Type u_1} {α : ι → Type u_3} {β : Type u_4} [CompleteLattice β] (s : Set ι) (t : (i : ι) → Set (α i)) (f : (i : ι) → α i → β) :
⨅ i ∈ s, ⨅ j ∈ t i, f i j = ⨅ ij ∈ s.sigma t, f ij.fst ij.snd
source
theorem Set.biUnion_sigma {ι : Type u_1} {α : ι → Type u_3} {β : Type u_5} (s : Set ι) (t : (i : ι) → Set (α i)) (f : Sigma α → Set β) :
⋃ ij ∈ s.sigma t, f ij = ⋃ i ∈ s, ⋃ j ∈ t i, f ⟨i, j⟩
source
theorem Set.biUnion_sigma' {ι : Type u_1} {α : ι → Type u_3} {β : Type u_5} (s : Set ι) (t : (i : ι) → Set (α i)) (f : (i : ι) → α i → Set β) :
⋃ i ∈ s, ⋃ j ∈ t i, f i j = ⋃ ij ∈ s.sigma t, f ij.fst ij.snd
source
theorem Set.biInter_sigma {ι : Type u_1} {α : ι → Type u_3} {β : Type u_5} (s : Set ι) (t : (i : ι) → Set (α i)) (f : Sigma α → Set β) :
⋂ ij ∈ s.sigma t, f ij = ⋂ i ∈ s, ⋂ j ∈ t i, f ⟨i, j⟩
source
theorem Set.biInter_sigma' {ι : Type u_1} {α : ι → Type u_3} {β : Type u_5} (s : Set ι) (t : (i : ι) → Set (α i)) (f : (i : ι) → α i → Set β) :
⋂ i ∈ s, ⋂ j ∈ t i, f i j = ⋂ ij ∈ s.sigma t, f ij.fst ij.snd
source
theorem Set.insert_sigma {ι : Type u_1} {α : ι → Type u_3} {s : Set ι} {t : (i : ι) → Set (α i)} {i : ι} :
(insert i s).sigma t = Sigma.mk i '' t i ∪ s.sigma t
source
theorem Set.sigma_insert {ι : Type u_1} {α : ι → Type u_3} {s : Set ι} {t : (i : ι) → Set (α i)} {a : (i : ι) → α i} :
(s.sigma fun (i : ι) => insert (a i) (t i)) = (fun (i : ι) => ⟨i, a i⟩) '' s ∪ s.sigma t
source
theorem Set.sigma_preimage_eq {ι : Type u_1} {ι' : Type u_2} {α : ι → Type u_3} {s : Set ι} {t : (i : ι) → Set (α i)} {β : ι → Type u_6} {f : ι' → ι} {g : (i : ι) → β i → α i} :
((f ⁻¹' s).sigma fun (i : ι') => g (f i) ⁻¹' t (f i)) = (fun (p : (i : ι') × β (f i)) => ⟨f p.fst, g (f p.fst) p.snd⟩) ⁻¹' s.sigma t
source
theorem Set.sigma_preimage_left {ι : Type u_1} {ι' : Type u_2} {α : ι → Type u_3} {s : Set ι} {t : (i : ι) → Set (α i)} {f : ι' → ι} :
((f ⁻¹' s).sigma fun (i : ι') => t (f i)) = (fun (p : (i : ι') × α (f i)) => ⟨f p.fst, p.snd⟩) ⁻¹' s.sigma t
source
theorem Set.sigma_preimage_right {ι : Type u_1} {α : ι → Type u_3} {s : Set ι} {t : (i : ι) → Set (α i)} {β : ι → Type u_6} {g : (i : ι) → β i → α i} :
(s.sigma fun (i : ι) => g i ⁻¹' t i) = (fun (p : (i : ι) × β i) => ⟨p.fst, g p.fst p.snd⟩) ⁻¹' s.sigma t
source
theorem Set.preimage_sigmaMap_sigma {ι : Type u_1} {ι' : Type u_2} {α : ι → Type u_3} {α' : ι' → Type u_7} (f : ι → ι') (g : (i : ι) → α i → α' (f i)) (s : Set ι') (t : (i : ι') → Set (α' i)) :
Sigma.map f g ⁻¹' s.sigma t = (f ⁻¹' s).sigma fun (i : ι) => g i ⁻¹' t (f i)
source
@[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 ⁻¹' s.sigma t = t i
source
@[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 ⁻¹' s.sigma t = ∅
source
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 ⁻¹' s.sigma t = if i ∈ s then t i else ∅
source
theorem Set.mk_preimage_sigma_fn_eq_if {ι : Type u_1} {α : ι → Type u_3} {s : Set ι} {t : (i : ι) → Set (α i)} {i : ι} {β : Type u_7} [DecidablePred fun (x : ι) => x ∈ s] (g : β → α i) :
(fun (b : β) => ⟨i, g b⟩) ⁻¹' s.sigma t = if i ∈ s then g ⁻¹' t i else ∅
source
theorem Set.sigma_univ_range_eq {ι : Type u_1} {α : ι → Type u_3} {β : ι → Type u_6} {f : (i : ι) → α i → β i} :
(univ.sigma fun (i : ι) => range (f i)) = range fun (x : (i : ι) × α i) => ⟨x.fst, f x.fst x.snd⟩
source
theorem Set.Nonempty.sigma {ι : Type u_1} {α : ι → Type u_3} {s : Set ι} {t : (i : ι) → Set (α i)} :
s.Nonempty → (∀ (i : ι), (t i).Nonempty) → (s.sigma t).Nonempty
source
theorem Set.Nonempty.sigma_fst {ι : Type u_1} {α : ι → Type u_3} {s : Set ι} {t : (i : ι) → Set (α i)} :
(s.sigma t).Nonempty → s.Nonempty
source
theorem Set.Nonempty.sigma_snd {ι : Type u_1} {α : ι → Type u_3} {s : Set ι} {t : (i : ι) → Set (α i)} :
(s.sigma t).Nonempty → ∃ i ∈ s, (t i).Nonempty
source
theorem Set.sigma_nonempty_iff {ι : Type u_1} {α : ι → Type u_3} {s : Set ι} {t : (i : ι) → Set (α i)} :
(s.sigma t).Nonempty ↔ ∃ i ∈ s, (t i).Nonempty
source
theorem Set.sigma_eq_empty_iff {ι : Type u_1} {α : ι → Type u_3} {s : Set ι} {t : (i : ι) → Set (α i)} :
s.sigma t = ∅ ↔ ∀ i ∈ s, t i = ∅
source
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 : ι) => ⟨i, a i⟩) '' s ⊆ s.sigma t
source
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 ⊆ s.sigma t
source
theorem Set.sigma_subset_preimage_fst {ι : Type u_1} {α : ι → Type u_3} (s : Set ι) (t : (i : ι) → Set (α i)) :
s.sigma t ⊆ Sigma.fst ⁻¹' s
source
theorem Set.fst_image_sigma_subset {ι : Type u_1} {α : ι → Type u_3} (s : Set ι) (t : (i : ι) → Set (α i)) :
Sigma.fst '' s.sigma t ⊆ s
source
theorem Set.image_sigma_eq_iUnion {ι : Type u_1} {α : ι → Type u_3} {s : Set ι} {t : (i : ι) → Set (α i)} {γ : Type u_7} (f : (i : ι) × α i → γ) :
f '' s.sigma t = ⋃ i ∈ s, f ∘ Sigma.mk i '' t i
source
theorem Set.fst_image_sigma {ι : Type u_1} {α : ι → Type u_3} {t : (i : ι) → Set (α i)} (s : Set ι) (ht : ∀ (i : ι), (t i).Nonempty) :
Sigma.fst '' s.sigma t = s
source
theorem Set.sigma_diff_sigma {ι : Type u_1} {α : ι → Type u_3} {s₁ s₂ : Set ι} {t₁ t₂ : (i : ι) → Set (α i)} :
s₁.sigma t₁ \ s₂.sigma t₂ = s₁.sigma (t₁ \ t₂) ∪ (s₁ \ s₂).sigma t₁
source
theorem Set.sigma_eq_biUnion {ι : Type u_1} {α : ι → Type u_3} {s : Set ι} {t : (i : ι) → Set (α i)} :
s.sigma t = ⋃ i ∈ s, Sigma.mk i '' t i
source
theorem Set.uncurry_preimage_sigma_pi {ι : Type u_1} {α : ι → Type u_3} {β : (i : ι) → α i → Type u_7} (s : Set ι) (t : (i : ι) → Set (α i)) (u : (p : (i : ι) × α i) → Set (β p.fst p.snd)) :
Sigma.uncurry ⁻¹' (s.sigma t).pi u = s.pi fun (i : ι) => (t i).pi fun (j : α i) => u ⟨i, j⟩