doc-next-gen

Mathlib.Data.Set.Sigma

Module docstring

{"# Sets in sigma types

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

Set.range_sigmaMk theorem
(i : ι) : range (Sigma.mk i : α i → Sigma α) = Sigma.fst ⁻¹' { i }
Full source 
@[simp]
theorem range_sigmaMk (i : ι) : range (Sigma.mk i : α i → Sigma α) = Sigma.fstSigma.fst ⁻¹' {i} := by
  apply Subset.antisymm
  · rintro _ ⟨b, rfl⟩
    simp
  · rintro ⟨x, y⟩ (rfl | _)
    exact mem_range_self y
Range of Sigma Embedding Equals Preimage of Singleton Index
Informal description
For any index $i \in \iota$, the range of the embedding $\Sigma.mk_i : \alpha_i \to \Sigma_{k} \alpha_k$ is equal to the preimage of the singleton set $\{i\}$ under the first projection $\Sigma.fst : \Sigma_{k} \alpha_k \to \iota$. In other words, \[ \mathrm{range}(\Sigma.mk_i) = \{ x \in \Sigma_{k} \alpha_k \mid \Sigma.fst(x) = i \}. \]
Set.preimage_image_sigmaMk_of_ne theorem
(h : i ≠ j) (s : Set (α j)) : Sigma.mk i ⁻¹' (Sigma.mk j '' s) = ∅
Full source 
theorem preimage_image_sigmaMk_of_ne (h : i ≠ j) (s : Set (α j)) :
    Sigma.mkSigma.mk i ⁻¹' (Sigma.mk j '' s) = ∅ := by
  ext x
  simp [h.symm]
Empty Preimage of Sigma Embedding for Distinct Indices
Informal description
For any distinct indices $i \neq j$ and any set $s \subseteq \alpha_j$, the preimage of the image of $s$ under the map $\Sigma.mk_j$ (which embeds $\alpha_j$ into the sigma type $\Sigma_{k} \alpha_k$) under the map $\Sigma.mk_i$ is the empty set. In other words, $\Sigma.mk_i^{-1}(\Sigma.mk_j(s)) = \emptyset$.
Set.image_sigmaMk_preimage_sigmaMap_subset theorem
{β : ι' → Type*} (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)
Full source 
theorem image_sigmaMk_preimage_sigmaMap_subset {β : ι' → Type*} (f : ι → ι')
    (g : ∀ i, α i → β (f i)) (i : ι) (s : Set (β (f i))) :
    Sigma.mkSigma.mk i '' (g i ⁻¹' s)Sigma.mk i '' (g i ⁻¹' s) ⊆ Sigma.map f g ⁻¹' (Sigma.mk (f i) '' s) :=
  image_subset_iff.2 fun x hx ↦ ⟨g i x, hx, rfl⟩
Image-Preimage Inclusion under Sigma Mapping
Informal description
For any function $f \colon \iota \to \iota'$, a family of functions $g_i \colon \alpha_i \to \beta(f(i))$ for each $i \in \iota$, an index $i \in \iota$, and a subset $s \subseteq \beta(f(i))$, the image of the preimage $g_i^{-1}(s)$ under the embedding $\Sigma.mk_i$ is contained in the preimage of the image $\Sigma.mk_{f(i)}(s)$ under the map $\Sigma.map \, f \, g$. In symbols: \[ \Sigma.mk_i(g_i^{-1}(s)) \subseteq (\Sigma.map \, f \, g)^{-1}(\Sigma.mk_{f(i)}(s)). \]
Set.image_sigmaMk_preimage_sigmaMap theorem
{β : ι' → Type*} {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)
Full source 
theorem image_sigmaMk_preimage_sigmaMap {β : ι' → Type*} {f : ι → ι'} (hf : Function.Injective f)
    (g : ∀ i, α i → β (f i)) (i : ι) (s : Set (β (f i))) :
    Sigma.mkSigma.mk i '' (g i ⁻¹' s) = Sigma.mapSigma.map f g ⁻¹' (Sigma.mk (f i) '' s) := by
  refine (image_sigmaMk_preimage_sigmaMap_subset f g i s).antisymm ?_
  rintro ⟨j, x⟩ ⟨y, hys, hxy⟩
  simp only [hf.eq_iff, Sigma.map, Sigma.ext_iff] at hxy
  rcases hxy with ⟨rfl, hxy⟩; rw [heq_iff_eq] at hxy; subst y
  exact ⟨x, hys, rfl⟩
Equality of Image-Preimage under Sigma Mapping for Injective Index Function
Informal description
Let $f \colon \iota \to \iota'$ be an injective function, and for each $i \in \iota$, let $g_i \colon \alpha_i \to \beta(f(i))$ be a function. For any index $i \in \iota$ and any subset $s \subseteq \beta(f(i))$, the image of the preimage $g_i^{-1}(s)$ under the embedding $\Sigma.mk_i$ is equal to the preimage of the image $\Sigma.mk_{f(i)}(s)$ under the map $\Sigma.map \, f \, g$. In symbols: \[ \Sigma.mk_i(g_i^{-1}(s)) = (\Sigma.map \, f \, g)^{-1}(\Sigma.mk_{f(i)}(s)). \]
Set.sigma definition
(s : Set ι) (t : ∀ i, Set (α i)) : Set (Σ i, α i)
Full source 
/-- Indexed sum of sets. `s.sigma t` is the set of dependent pairs `⟨i, a⟩` such that `i ∈ s` and
`a ∈ t i`. -/
protected def sigma (s : Set ι) (t : ∀ i, Set (α i)) : Set (Σ i, α i) := {x | x.1 ∈ s ∧ x.2 ∈ t x.1}
Indexed sum of sets
Informal description
Given an index set $\iota$ and a family of types $\alpha_i$ for each $i \in \iota$, the indexed sum of sets $s \subseteq \iota$ and $t_i \subseteq \alpha_i$ for each $i \in s$ is the set $\Sigma i \in s, t_i$ consisting of all dependent pairs $\langle i, a \rangle$ where $i \in s$ and $a \in t_i$.
Set.mem_sigma_iff theorem
: x ∈ s.sigma t ↔ x.1 ∈ s ∧ x.2 ∈ t x.1
Full source 
@[simp] theorem mem_sigma_iff : x ∈ s.sigma tx ∈ s.sigma t ↔ x.1 ∈ s ∧ x.2 ∈ t x.1 := Iff.rfl
Membership Criterion for Indexed Sum of Sets: $x \in \Sigma i \in s, t_i \leftrightarrow x_1 \in s \land x_2 \in t_{x_1}$
Informal description
For any element $x$ in the sigma type $\Sigma i, \alpha i$, $x$ belongs to the indexed sum of sets $s.\mathrm{sigma}\, t$ if and only if the first component of $x$ is in $s$ and the second component of $x$ is in the set $t$ indexed by the first component. In other words, $x \in \Sigma i \in s, t_i$ if and only if $x_1 \in s$ and $x_2 \in t_{x_1}$.
Set.mk_sigma_iff theorem
: (⟨i, a⟩ : Σ i, α i) ∈ s.sigma t ↔ i ∈ s ∧ a ∈ t i
Full source 
theorem mk_sigma_iff : (⟨i, a⟩ : Σ i, α i) ∈ s.sigma t(⟨i, a⟩ : Σ i, α i) ∈ s.sigma t ↔ i ∈ s ∧ a ∈ t i := Iff.rfl
Membership Criterion for Indexed Sum of Sets via Dependent Pair: $\langle i, a \rangle \in \Sigma i \in s, t_i \leftrightarrow i \in s \land a \in t_i$
Informal description
For any dependent pair $\langle i, a \rangle$ in the sigma type $\Sigma i, \alpha i$, the pair belongs to the indexed sum of sets $s.\mathrm{sigma}\, t$ if and only if $i \in s$ and $a \in t_i$.
Set.mk_mem_sigma theorem
(hi : i ∈ s) (ha : a ∈ t i) : (⟨i, a⟩ : Σ i, α i) ∈ s.sigma t
Full source 
theorem mk_mem_sigma (hi : i ∈ s) (ha : a ∈ t i) : (⟨i, a⟩ : Σ i, α i) ∈ s.sigma t := ⟨hi, ha⟩
Membership in Indexed Sum of Sets via Dependent Pair Construction
Informal description
For any index $i$ in a set $s$ and any element $a$ in the set $t_i$ indexed by $i$, the dependent pair $\langle i, a \rangle$ belongs to the indexed sum of sets $\Sigma i \in s, t_i$.
Set.sigma_mono theorem
(hs : s₁ ⊆ s₂) (ht : ∀ i, t₁ i ⊆ t₂ i) : s₁.sigma t₁ ⊆ s₂.sigma t₂
Full source 
theorem sigma_mono (hs : s₁ ⊆ s₂) (ht : ∀ i, t₁ i ⊆ t₂ i) : s₁.sigma t₁ ⊆ s₂.sigma t₂ := fun _ hx ↦
  ⟨hs hx.1, ht _ hx.2⟩
Monotonicity of Indexed Sum of Sets: $\Sigma i \in s_1, t_1(i) \subseteq \Sigma i \in s_2, t_2(i)$ when $s_1 \subseteq s_2$ and $t_1(i) \subseteq t_2(i)$ for all $i$
Informal description
For any two sets $s_1 \subseteq s_2$ in the index type $\iota$ and any family of sets $t_1(i) \subseteq t_2(i)$ for each $i \in \iota$, the indexed sum $\Sigma i \in s_1, t_1(i)$ is a subset of the indexed sum $\Sigma i \in s_2, t_2(i)$.
Set.sigma_subset_iff theorem
: s.sigma t ⊆ u ↔ ∀ ⦃i⦄, i ∈ s → ∀ ⦃a⦄, a ∈ t i → (⟨i, a⟩ : Σ i, α i) ∈ u
Full source 
theorem sigma_subset_iff :
    s.sigma t ⊆ us.sigma t ⊆ u ↔ ∀ ⦃i⦄, i ∈ s → ∀ ⦃a⦄, a ∈ t i → (⟨i, a⟩ : Σ i, α i) ∈ u :=
  ⟨fun h _ hi _ ha ↦ h <| mk_mem_sigma hi ha, fun h _ ha ↦ h ha.1 ha.2⟩
Characterization of Subset Relation for Indexed Sum of Sets
Informal description
For any set $s$ over an index type $\iota$, any family of sets $t_i$ over types $\alpha_i$ for each $i \in \iota$, and any set $u$ over the dependent pair type $\Sigma i, \alpha_i$, the indexed sum of sets $\Sigma i \in s, t_i$ is a subset of $u$ if and only if for every index $i \in s$ and every element $a \in t_i$, the dependent pair $\langle i, a \rangle$ belongs to $u$.
Set.forall_sigma_iff theorem
{p : (Σ i, α i) → Prop} : (∀ x ∈ s.sigma t, p x) ↔ ∀ ⦃i⦄, i ∈ s → ∀ ⦃a⦄, a ∈ t i → p ⟨i, a⟩
Full source 
theorem forall_sigma_iff {p : (Σ i, α i) → Prop} :
    (∀ x ∈ s.sigma t, p x) ↔ ∀ ⦃i⦄, i ∈ s → ∀ ⦃a⦄, a ∈ t i → p ⟨i, a⟩ := sigma_subset_iff
Universal Quantifier over Indexed Sum of Sets $\iff$ Universal Quantifier over Components
Informal description
For any predicate $p$ on the dependent pair type $\Sigma i, \alpha_i$, the following are equivalent: 1. For every element $x$ in the indexed sum $\Sigma i \in s, t_i$, the predicate $p(x)$ holds. 2. For every index $i \in s$ and every element $a \in t_i$, the predicate $p(\langle i, a \rangle)$ holds.
Set.exists_sigma_iff theorem
{p : (Σ i, α i) → Prop} : (∃ x ∈ s.sigma t, p x) ↔ ∃ i ∈ s, ∃ a ∈ t i, p ⟨i, a⟩
Full source 
theorem exists_sigma_iff {p : (Σi, α i) → Prop} :
    (∃ x ∈ s.sigma t, p x) ↔ ∃ i ∈ s, ∃ a ∈ t i, p ⟨i, a⟩ :=
  ⟨fun ⟨⟨i, a⟩, ha, h⟩ ↦ ⟨i, ha.1, a, ha.2, h⟩, fun ⟨i, hi, a, ha, h⟩ ↦ ⟨⟨i, a⟩, ⟨hi, ha⟩, h⟩⟩
Existence in Indexed Sum of Sets iff Existence in Components
Informal description
For any predicate $p$ on the dependent pair type $\Sigma i, \alpha i$, there exists an element $x$ in the indexed sum of sets $s.\mathrm{sigma}\, t$ such that $p(x)$ holds if and only if there exists an index $i \in s$ and an element $a \in t(i)$ such that $p(\langle i, a \rangle)$ holds.
Set.sigma_empty theorem
: s.sigma (fun i ↦ (∅ : Set (α i))) = ∅
Full source 
@[simp] theorem sigma_empty : s.sigma (fun i ↦ (∅ : Set (α i))) = ∅ :=
  ext fun _ ↦ iff_of_eq (and_false _)
Indexed Sum of Empty Sets is Empty
Informal description
For any set $s$ over an index type $\iota$ and the family of empty sets $\emptyset \subseteq \alpha_i$ for each $i \in \iota$, the indexed sum of sets $\Sigma i \in s, \emptyset$ is equal to the empty set $\emptyset$.
Set.empty_sigma theorem
: (∅ : Set ι).sigma t = ∅
Full source 
@[simp] theorem empty_sigma : (∅ : Set ι).sigma t = ∅ := ext fun _ ↦ iff_of_eq (false_and _)
Empty Indexed Sum of Sets is Empty
Informal description
For any family of sets $t_i \subseteq \alpha_i$ indexed by $i \in \iota$, the indexed sum $\Sigma i \in \emptyset, t_i$ is equal to the empty set $\emptyset$.
Set.univ_sigma_univ theorem
: (@univ ι).sigma (fun _ ↦ @univ (α i)) = univ
Full source 
theorem univ_sigma_univ : (@univ ι).sigma (fun _ ↦ @univ (α i)) = univ :=
  ext fun _ ↦ iff_of_eq (true_and _)
Universal Sigma Set Identity: $\Sigma_{i \in \iota} \alpha_i = \Sigma i, \alpha_i$
Informal description
For any index type $\iota$ and family of types $\alpha_i$ for $i \in \iota$, the indexed sum of the universal set over $\iota$ with the universal sets over each $\alpha_i$ equals the universal set over the dependent sum type $\Sigma i, \alpha_i$. In other words: $$\Sigma_{i \in \iota} \alpha_i = \Sigma i, \alpha_i$$
Set.sigma_univ theorem
: s.sigma (fun _ ↦ univ : ∀ i, Set (α i)) = Sigma.fst ⁻¹' s
Full source 
@[simp]
theorem sigma_univ : s.sigma (fun _ ↦ univ : ∀ i, Set (α i)) = Sigma.fstSigma.fst ⁻¹' s :=
  ext fun _ ↦ iff_of_eq (and_true _)
Sigma Set Equals Preimage of First Projection
Informal description
For any set $s \subseteq \iota$ and any family of types $\alpha_i$ indexed by $i \in \iota$, the indexed sum $\Sigma_{i \in s} \alpha_i$ is equal to the preimage of $s$ under the first projection $\Sigma.fst : \Sigma i, \alpha_i \to \iota$. In other words: $$\Sigma_{i \in s} \alpha_i = \Sigma.fst^{-1}(s)$$
Set.univ_sigma_preimage_mk theorem
(s : Set (Σ i, α i)) : (univ : Set ι).sigma (fun i ↦ Sigma.mk i ⁻¹' s) = s
Full source 
@[simp] theorem univ_sigma_preimage_mk (s : Set (Σ i, α i)) :
    (univ : Set ι).sigma (fun i ↦ Sigma.mkSigma.mk i ⁻¹' s) = s :=
  ext <| by simp
Universal Sigma Set Decomposition via Preimages
Informal description
For any set $s$ of dependent pairs in $\Sigma i, \alpha_i$, the indexed sum of the universal set over $\iota$ with the preimages of $s$ under the pairing function $\Sigma.mk_i$ equals $s$ itself. In other words: \[ \Sigma_{i \in \iota} (\Sigma.mk_i)^{-1}(s) = s. \]
Set.singleton_sigma theorem
: ({ i } : Set ι).sigma t = Sigma.mk i '' t i
Full source 
@[simp]
theorem singleton_sigma : ({i} : Set ι).sigma t = Sigma.mkSigma.mk i '' t i :=
  ext fun x ↦ by
    constructor
    · obtain ⟨j, a⟩ := x
      rintro ⟨rfl : j = i, ha⟩
      exact mem_image_of_mem _ ha
    · rintro ⟨b, hb, rfl⟩
      exact ⟨rfl, hb⟩
Singleton Sigma Set as Image of Pairing Function
Informal description
For any index $i \in \iota$ and any family of sets $t_i \subseteq \alpha_i$, the indexed sum of the singleton set $\{i\}$ with the family $t$ is equal to the image of $t_i$ under the pairing function $\Sigma.mk_i : \alpha_i \to \Sigma j, \alpha_j$. In other words: \[ \Sigma_{j \in \{i\}} t_j = \{\langle i, a \rangle \mid a \in t_i\}. \]
Set.sigma_singleton theorem
{a : ∀ i, α i} : s.sigma (fun i ↦ ({a i} : Set (α i))) = (fun i ↦ Sigma.mk i <| a i) '' s
Full source 
@[simp]
theorem sigma_singleton {a : ∀ i, α i} :
    s.sigma (fun i ↦ ({a i} : Set (α i))) = (fun i ↦ Sigma.mk i <| a i) '' s := by
  ext ⟨x, y⟩
  simp [and_left_comm, eq_comm]
Indexed Sum of Singleton Sets Equals Image of Pairing Function
Informal description
Given a set $s \subseteq \iota$ and a family of elements $a_i \in \alpha_i$ for each $i \in \iota$, the indexed sum of the singleton sets $\{a_i\}$ over $s$ is equal to the image of $s$ under the function $i \mapsto \langle i, a_i \rangle$. In other words: \[ \Sigma_{i \in s} \{a_i\} = \{\langle i, a_i \rangle \mid i \in s\}. \]
Set.singleton_sigma_singleton theorem
{a : ∀ i, α i} : (({ i } : Set ι).sigma fun i ↦ ({a i} : Set (α i))) = {⟨i, a i⟩}
Full source 
theorem singleton_sigma_singleton {a : ∀ i, α i} :
    (({i} : Set ι).sigma fun i ↦ ({a i} : Set (α i))) = {⟨i, a i⟩} := by
  rw [sigma_singleton, image_singleton]
Indexed Sum of Singleton Sets is a Singleton Pair
Informal description
For any index $i \in \iota$ and any family of elements $a_j \in \alpha_j$ for $j \in \iota$, the indexed sum of the singleton sets $\{i\}$ and $\{a_i\}$ is the singleton set $\{\langle i, a_i \rangle\}$. In other words: \[ \Sigma_{j \in \{i\}} \{a_j\} = \{\langle i, a_i \rangle\}. \]
Set.union_sigma theorem
: (s₁ ∪ s₂).sigma t = s₁.sigma t ∪ s₂.sigma t
Full source 
@[simp]
theorem union_sigma : (s₁ ∪ s₂).sigma t = s₁.sigma t ∪ s₂.sigma t := ext fun _ ↦ or_and_right
Union Property of Indexed Sum of Sets: $\Sigma_{s_1 \cup s_2} t = \Sigma_{s_1} t \cup \Sigma_{s_2} t$
Informal description
For any two sets $s_1, s_2 \subseteq \iota$ and a family of sets $t_i \subseteq \alpha_i$ for each $i \in \iota$, the indexed sum of sets over the union $s_1 \cup s_2$ is equal to the union of the indexed sums over $s_1$ and $s_2$ separately. That is: \[ \Sigma_{i \in s_1 \cup s_2} t_i = \left(\Sigma_{i \in s_1} t_i\right) \cup \left(\Sigma_{i \in s_2} t_i\right). \]
Set.sigma_union theorem
: s.sigma (fun i ↦ t₁ i ∪ t₂ i) = s.sigma t₁ ∪ s.sigma t₂
Full source 
@[simp]
theorem sigma_union : s.sigma (fun i ↦ t₁ i ∪ t₂ i) = s.sigma t₁ ∪ s.sigma t₂ :=
  ext fun _ ↦ and_or_left
Distributivity of Indexed Sum over Union: $\Sigma_s (t₁ \cup t₂) = \Sigma_s t₁ \cup \Sigma_s t₂$
Informal description
For any set $s \subseteq \iota$ and any two families of sets $t₁_i, t₂_i \subseteq \alpha_i$ indexed by $i \in \iota$, the indexed sum of the union sets $t₁_i \cup t₂_i$ over $s$ is equal to the union of the indexed sums of $t₁_i$ and $t₂_i$ over $s$. That is, \[ \Sigma_{i \in s} (t₁_i \cup t₂_i) = (\Sigma_{i \in s} t₁_i) \cup (\Sigma_{i \in s} t₂_i). \]
Set.sigma_inter_sigma theorem
: s₁.sigma t₁ ∩ s₂.sigma t₂ = (s₁ ∩ s₂).sigma fun i ↦ t₁ i ∩ t₂ i
Full source 
theorem sigma_inter_sigma : s₁.sigma t₁ ∩ s₂.sigma t₂ = (s₁ ∩ s₂).sigma fun i ↦ t₁ i ∩ t₂ i := by
  ext ⟨x, y⟩
  simp [and_assoc, and_left_comm]
Intersection of Sigma Sets Equals Sigma of Intersections
Informal description
For any two index sets $s_1, s_2 \subseteq \iota$ and two families of sets $t_1, t_2$ where $t_1(i), t_2(i) \subseteq \alpha_i$ for each $i \in \iota$, the intersection of the indexed sums $\Sigma i \in s_1, t_1(i)$ and $\Sigma i \in s_2, t_2(i)$ is equal to the indexed sum over the intersection $s_1 \cap s_2$ of the intersections $t_1(i) \cap t_2(i)$. That is, \[ \left( \Sigma i \in s_1, t_1(i) \right) \cap \left( \Sigma i \in s_2, t_2(i) \right) = \Sigma i \in s_1 \cap s_2, \left( t_1(i) \cap t_2(i) \right). \]
biSup_sigma theorem
(s : Set ι) (t : ∀ i, Set (α i)) (f : Sigma α → β) : ⨆ ij ∈ s.sigma t, f ij = ⨆ (i ∈ s) (j ∈ t i), f ⟨i, j⟩
Full source 
theorem _root_.biSup_sigma (s : Set ι) (t : ∀ i, Set (α i)) (f : Sigma α → β) :
    ⨆ ij ∈ s.sigma t, f ij = ⨆ (i ∈ s) (j ∈ t i), f ⟨i, j⟩ :=
  eq_of_forall_ge_iff fun _ ↦ ⟨by simp_all, by simp_all⟩
Supremum over Sigma Set Equals Iterated Supremum
Informal description
For any set $s \subseteq \iota$ and family of sets $t_i \subseteq \alpha_i$ indexed by $i \in \iota$, and for any function $f : \Sigma i, \alpha_i \to \beta$, the supremum of $f$ over the indexed sum set $\Sigma i \in s, t_i$ is equal to the iterated supremum of $f$ over $i \in s$ and $j \in t_i$. That is, \[ \bigsqcup_{\langle i, j \rangle \in \Sigma i \in s, t_i} f(i, j) = \bigsqcup_{i \in s} \bigsqcup_{j \in t_i} f(i, j). \]
biSup_sigma' theorem
(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
Full source 
theorem _root_.biSup_sigma' (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 :=
  Eq.symm (biSup_sigma _ _ _)
Iterated Supremum Equals Supremum over Sigma Set for Indexed Functions
Informal description
For any set $s \subseteq \iota$ and family of sets $t_i \subseteq \alpha_i$ indexed by $i \in \iota$, and for any family of functions $f_i : \alpha_i \to \beta$ indexed by $i \in \iota$, the iterated supremum of $f_i(j)$ over $i \in s$ and $j \in t_i$ is equal to the supremum of $f_{ij.\mathrm{fst}}(ij.\mathrm{snd})$ over all pairs $\langle i, j \rangle$ in the indexed sum set $\Sigma i \in s, t_i$. That is, \[ \bigsqcup_{i \in s} \bigsqcup_{j \in t_i} f_i(j) = \bigsqcup_{\langle i, j \rangle \in \Sigma i \in s, t_i} f_i(j). \]
biInf_sigma theorem
(s : Set ι) (t : ∀ i, Set (α i)) (f : Sigma α → β) : ⨅ ij ∈ s.sigma t, f ij = ⨅ (i ∈ s) (j ∈ t i), f ⟨i, j⟩
Full source 
theorem _root_.biInf_sigma (s : Set ι) (t : ∀ i, Set (α i)) (f : Sigma α → β) :
    ⨅ ij ∈ s.sigma t, f ij = ⨅ (i ∈ s) (j ∈ t i), f ⟨i, j⟩ :=
  biSup_sigma (β := βᵒᵈ) _ _ _
Infimum over Sigma Set Equals Iterated Infimum
Informal description
For any set $s \subseteq \iota$ and family of sets $t_i \subseteq \alpha_i$ indexed by $i \in \iota$, and for any function $f : \Sigma i, \alpha_i \to \beta$, the infimum of $f$ over the indexed sum set $\Sigma i \in s, t_i$ is equal to the iterated infimum of $f$ over $i \in s$ and $j \in t_i$. That is, \[ \bigsqcap_{\langle i, j \rangle \in \Sigma i \in s, t_i} f(i, j) = \bigsqcap_{i \in s} \bigsqcap_{j \in t_i} f(i, j). \]
biInf_sigma' theorem
(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
Full source 
theorem _root_.biInf_sigma' (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 :=
  Eq.symm (biInf_sigma _ _ _)
Iterated Infimum Equals Infimum over Sigma Set for Indexed Functions
Informal description
For any set $s \subseteq \iota$ and family of sets $t_i \subseteq \alpha_i$ indexed by $i \in \iota$, and for any family of functions $f_i : \alpha_i \to \beta$ indexed by $i \in \iota$, the iterated infimum of $f_i(j)$ over $i \in s$ and $j \in t_i$ is equal to the infimum of $f_{i}(j)$ over all pairs $\langle i, j \rangle$ in the indexed sum set $\Sigma i \in s, t_i$. That is, \[ \bigsqcap_{i \in s} \bigsqcap_{j \in t_i} f_i(j) = \bigsqcap_{\langle i, j \rangle \in \Sigma i \in s, t_i} f_i(j). \]
Set.biUnion_sigma theorem
(s : Set ι) (t : ∀ i, Set (α i)) (f : Sigma α → Set β) : ⋃ ij ∈ s.sigma t, f ij = ⋃ i ∈ s, ⋃ j ∈ t i, f ⟨i, j⟩
Full source 
theorem biUnion_sigma (s : Set ι) (t : ∀ i, Set (α i)) (f : Sigma α → Set β) :
    ⋃ ij ∈ s.sigma t, f ij = ⋃ i ∈ s, ⋃ j ∈ t i, f ⟨i, j⟩ :=
  biSup_sigma _ _ _
Union over Sigma Set Equals Iterated Union
Informal description
For any set $s \subseteq \iota$ and family of sets $t_i \subseteq \alpha_i$ indexed by $i \in \iota$, and for any function $f : \Sigma i, \alpha_i \to \mathcal{P}(\beta)$, the union of $f(i,j)$ over all pairs $\langle i, j \rangle$ in the indexed sum set $\Sigma i \in s, t_i$ is equal to the iterated union of $f(i,j)$ over $i \in s$ and $j \in t_i$. That is, \[ \bigcup_{\langle i, j \rangle \in \Sigma i \in s, t_i} f(i,j) = \bigcup_{i \in s} \bigcup_{j \in t_i} f(i,j). \]
Set.biUnion_sigma' theorem
(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
Full source 
theorem biUnion_sigma' (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 :=
  biSup_sigma' _ _ _
Union over Sigma Set Equals Iterated Union for Indexed Functions
Informal description
For any set $s \subseteq \iota$ and family of sets $t_i \subseteq \alpha_i$ indexed by $i \in \iota$, and for any family of set-valued functions $f_i : \alpha_i \to \mathcal{P}(\beta)$ indexed by $i \in \iota$, the iterated union of $f_i(j)$ over $i \in s$ and $j \in t_i$ is equal to the union of $f_{i}(j)$ over all pairs $\langle i, j \rangle$ in the indexed sum set $\Sigma i \in s, t_i$. That is, \[ \bigcup_{i \in s} \bigcup_{j \in t_i} f_i(j) = \bigcup_{\langle i, j \rangle \in \Sigma i \in s, t_i} f_i(j). \]
Set.biInter_sigma theorem
(s : Set ι) (t : ∀ i, Set (α i)) (f : Sigma α → Set β) : ⋂ ij ∈ s.sigma t, f ij = ⋂ i ∈ s, ⋂ j ∈ t i, f ⟨i, j⟩
Full source 
theorem biInter_sigma (s : Set ι) (t : ∀ i, Set (α i)) (f : Sigma α → Set β) :
    ⋂ ij ∈ s.sigma t, f ij = ⋂ i ∈ s, ⋂ j ∈ t i, f ⟨i, j⟩ :=
  biInf_sigma _ _ _
Intersection over Sigma Set Equals Iterated Intersection
Informal description
For any set $s \subseteq \iota$ and family of sets $t_i \subseteq \alpha_i$ indexed by $i \in \iota$, and for any function $f : \Sigma i, \alpha_i \to \mathcal{P}(\beta)$, the intersection of $f(i,j)$ over all pairs $\langle i, j \rangle$ in the indexed sum set $\Sigma i \in s, t_i$ is equal to the iterated intersection of $f(i,j)$ over $i \in s$ and $j \in t_i$. That is, \[ \bigcap_{\langle i, j \rangle \in \Sigma i \in s, t_i} f(i,j) = \bigcap_{i \in s} \bigcap_{j \in t_i} f(i,j). \]
Set.biInter_sigma' theorem
(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
Full source 
theorem biInter_sigma' (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 :=
  biInf_sigma' _ _ _
Iterated Intersection Equals Intersection over Sigma Set for Indexed Functions
Informal description
For any set $s \subseteq \iota$ and family of sets $t_i \subseteq \alpha_i$ indexed by $i \in \iota$, and for any family of functions $f_i : \alpha_i \to \text{Set } \beta$ indexed by $i \in \iota$, the iterated intersection of $f_i(j)$ over $i \in s$ and $j \in t_i$ is equal to the intersection of $f_i(j)$ over all pairs $\langle i, j \rangle$ in the indexed sum set $\Sigma i \in s, t_i$. That is, \[ \bigcap_{i \in s} \bigcap_{j \in t_i} f_i(j) = \bigcap_{\langle i, j \rangle \in \Sigma i \in s, t_i} f_i(j). \]
Set.insert_sigma theorem
: (insert i s).sigma t = Sigma.mk i '' t i ∪ s.sigma t
Full source 
theorem insert_sigma : (insert i s).sigma t = Sigma.mkSigma.mk i '' t iSigma.mk i '' t i ∪ s.sigma t := by
  rw [insert_eq, union_sigma, singleton_sigma]
Insertion Property of Indexed Sum of Sets: $\Sigma_{\text{insert}(i, s)} t = \{\langle i, a \rangle \mid a \in t_i\} \cup \Sigma_s t$
Informal description
For any index $i \in \iota$, any set $s \subseteq \iota$, and any family of sets $t_j \subseteq \alpha_j$ for $j \in \iota$, the indexed sum of sets over the insertion $\{i\} \cup s$ is equal to the union of the image of $t_i$ under the pairing function $\langle i, \cdot \rangle$ and the indexed sum of sets over $s$. That is: \[ \Sigma_{j \in \{i\} \cup s} t_j = \{\langle i, a \rangle \mid a \in t_i\} \cup \left(\Sigma_{j \in s} t_j\right). \]
Set.sigma_insert theorem
{a : ∀ i, α i} : s.sigma (fun i ↦ insert (a i) (t i)) = (fun i ↦ ⟨i, a i⟩) '' s ∪ s.sigma t
Full source 
theorem sigma_insert {a : ∀ i, α i} :
    s.sigma (fun i ↦ insert (a i) (t i)) = (fun i ↦ ⟨i, a i⟩) '' s(fun i ↦ ⟨i, a i⟩) '' s ∪ s.sigma t := by
  simp_rw [insert_eq, sigma_union, sigma_singleton]
Indexed Sum of Inserted Sets Equals Union of Image and Original Sum
Informal description
For a set $s \subseteq \iota$ and a family of sets $t_i \subseteq \alpha_i$ indexed by $i \in \iota$, along with a family of elements $a_i \in \alpha_i$, the indexed sum of the sets $\{a_i\} \cup t_i$ over $s$ is equal to the union of the image of $s$ under the map $i \mapsto \langle i, a_i \rangle$ and the indexed sum of the sets $t_i$ over $s$. In symbols: \[ \Sigma_{i \in s} (\{a_i\} \cup t_i) = \{\langle i, a_i \rangle \mid i \in s\} \cup \left( \Sigma_{i \in s} t_i \right). \]
Set.sigma_preimage_eq theorem
{f : ι' → ι} {g : ∀ i, β i → α i} : (f ⁻¹' s).sigma (fun i ↦ g (f i) ⁻¹' t (f i)) = (fun p : Σ i, β (f i) ↦ Sigma.mk _ (g _ p.2)) ⁻¹' s.sigma t
Full source 
theorem sigma_preimage_eq {f : ι' → ι} {g : ∀ i, β i → α i} :
    (f ⁻¹' s).sigma (fun i ↦ g (f i) ⁻¹' t (f i)) =
      (fun p : Σ i, β (f i) ↦ Sigma.mk _ (g _ p.2)) ⁻¹' s.sigma t := rfl
Preimage of Sigma Set under Fiberwise Mapped Pair Construction
Informal description
For any function $f \colon \iota' \to \iota$ and family of functions $g_i \colon \beta_i \to \alpha_i$ indexed by $i \in \iota$, the preimage of the indexed sum of sets $s \subseteq \iota$ and $t_i \subseteq \alpha_i$ under the map $(p : \Sigma i, \beta_{f(i)}) \mapsto \langle f(p_1), g_{f(p_1)}(p_2) \rangle$ is equal to the indexed sum of the preimage $f^{-1}(s) \subseteq \iota'$ and the preimages $g_{f(i)}^{-1}(t_{f(i)}) \subseteq \beta_i$ for each $i \in f^{-1}(s)$. In symbols: $$(f^{-1}s).\Sigma \left(i \mapsto g_{f(i)}^{-1}(t_{f(i)})\right) = \left(p \mapsto \langle f(p_1), g_{f(p_1)}(p_2) \rangle\right)^{-1}(s.\Sigma t)$$
Set.sigma_preimage_left theorem
{f : ι' → ι} : ((f ⁻¹' s).sigma fun i ↦ t (f i)) = (fun p : Σ i, α (f i) ↦ Sigma.mk _ p.2) ⁻¹' s.sigma t
Full source 
theorem sigma_preimage_left {f : ι' → ι} :
    ((f ⁻¹' s).sigma fun i ↦ t (f i)) = (fun p : Σ i, α (f i) ↦ Sigma.mk _ p.2) ⁻¹' s.sigma t :=
  rfl
Preimage of Indexed Sum under Projection Equals Indexed Sum of Preimages
Informal description
For any function $f \colon \iota' \to \iota$, the indexed sum of the preimage $f^{-1}(s) \subseteq \iota'$ and the sets $t_{f(i)} \subseteq \alpha_{f(i)}$ for each $i \in f^{-1}(s)$ is equal to the preimage of the indexed sum $s.\Sigma t$ under the map $(p : \Sigma i, \alpha_{f(i)}) \mapsto \langle p_1, p_2 \rangle$. In symbols: $$(f^{-1}s).\Sigma \left(i \mapsto t_{f(i)}\right) = \left(p \mapsto \langle p_1, p_2 \rangle\right)^{-1}(s.\Sigma t)$$
Set.sigma_preimage_right theorem
{g : ∀ i, β i → α i} : (s.sigma fun i ↦ g i ⁻¹' t i) = (fun p : Σ i, β i ↦ Sigma.mk p.1 (g _ p.2)) ⁻¹' s.sigma t
Full source 
theorem sigma_preimage_right {g : ∀ i, β i → α i} :
    (s.sigma fun i ↦ g i ⁻¹' t i) = (fun p : Σ i, β i ↦ Sigma.mk p.1 (g _ p.2)) ⁻¹' s.sigma t :=
  rfl
Preimage of Indexed Sum under Fiberwise Mapped Pair Construction
Informal description
For any family of functions $g_i \colon \beta_i \to \alpha_i$ indexed by $i \in \iota$, the indexed sum of the sets $s \subseteq \iota$ and the preimages $g_i^{-1}(t_i) \subseteq \beta_i$ is equal to the preimage of the indexed sum $s.\Sigma t$ under the map $(p : \Sigma i, \beta_i) \mapsto \langle p_1, g_{p_1}(p_2) \rangle$. In symbols: $$s.\Sigma \left(i \mapsto g_i^{-1}(t_i)\right) = \left(p \mapsto \langle p_1, g_{p_1}(p_2) \rangle\right)^{-1}(s.\Sigma t)$$
Set.preimage_sigmaMap_sigma theorem
{α' : ι' → Type*} (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)
Full source 
theorem preimage_sigmaMap_sigma {α' : ι' → Type*} (f : ι → ι') (g : ∀ i, α i → α' (f i))
    (s : Set ι') (t : ∀ i, Set (α' i)) :
    Sigma.mapSigma.map f g ⁻¹' s.sigma t = (f ⁻¹' s).sigma fun i ↦ g i ⁻¹' t (f i) := rfl
Preimage of Indexed Sum under Sigma Map Equals Indexed Sum of Preimages
Informal description
Let $\iota$ and $\iota'$ be index types, $\alpha : \iota \to \text{Type}$ and $\alpha' : \iota' \to \text{Type}$ be type families, $f : \iota \to \iota'$ be a function, and $g : \forall i, \alpha i \to \alpha' (f i)$ be a family of functions. For any set $s \subseteq \iota'$ and any family of sets $t_i \subseteq \alpha' i$ indexed by $i \in \iota'$, the preimage of the indexed sum $\Sigma_{i \in s} t_i$ under the map $\Sigma.\text{map} f g$ is equal to the indexed sum $\Sigma_{i \in f^{-1}(s)} (g i)^{-1}(t_{f(i)})$. In symbols: $$(\Sigma.\text{map} f g)^{-1}\left(\Sigma_{i \in s} t_i\right) = \Sigma_{i \in f^{-1}(s)} (g i)^{-1}(t_{f(i)})$$
Set.mk_preimage_sigma theorem
(hi : i ∈ s) : Sigma.mk i ⁻¹' s.sigma t = t i
Full source 
@[simp]
theorem mk_preimage_sigma (hi : i ∈ s) : Sigma.mkSigma.mk i ⁻¹' s.sigma t = t i :=
  ext fun _ ↦ and_iff_right hi
Preimage of Indexed Sum under Sigma Map Equals Component Set
Informal description
For any index $i$ in a set $s \subseteq \iota$ and any family of sets $t_i \subseteq \alpha_i$ indexed by $i \in \iota$, the preimage of the indexed sum $\Sigma_{i \in s} t_i$ under the map $\Sigma.mk_i$ is equal to $t_i$. That is, $(\Sigma.mk_i)^{-1}(\Sigma_{i \in s} t_i) = t_i$.
Set.mk_preimage_sigma_eq_empty theorem
(hi : i ∉ s) : Sigma.mk i ⁻¹' s.sigma t = ∅
Full source 
@[simp]
theorem mk_preimage_sigma_eq_empty (hi : i ∉ s) : Sigma.mkSigma.mk i ⁻¹' s.sigma t = ∅ :=
  ext fun _ ↦ iff_of_false (hi ∘ And.left) id
Empty Preimage of Indexed Sum for Non-Member Index
Informal description
For any index $i$ not in a set $s \subseteq \iota$ and any family of sets $t_i \subseteq \alpha_i$ indexed by $i \in \iota$, the preimage of the indexed sum $\Sigma_{i \in s} t_i$ under the map $\Sigma.mk_i$ is the empty set. That is, $(\Sigma.mk_i)^{-1}(\Sigma_{i \in s} t_i) = \emptyset$.
Set.mk_preimage_sigma_eq_if theorem
[DecidablePred (· ∈ s)] : Sigma.mk i ⁻¹' s.sigma t = if i ∈ s then t i else ∅
Full source 
theorem mk_preimage_sigma_eq_if [DecidablePred (· ∈ s)] :
    Sigma.mkSigma.mk i ⁻¹' s.sigma t = if i ∈ s then t i else ∅ := by split_ifs <;> simp [*]
Conditional Preimage of Indexed Sum under Sigma Map
Informal description
Let $s \subseteq \iota$ be a set with a decidable membership predicate, and let $t_i \subseteq \alpha_i$ be a family of sets indexed by $i \in \iota$. The preimage of the indexed sum $\Sigma_{i \in s} t_i$ under the map $\Sigma.mk_i$ is equal to $t_i$ if $i \in s$, and the empty set otherwise. That is: \[ (\Sigma.mk_i)^{-1}(\Sigma_{i \in s} t_i) = \begin{cases} t_i & \text{if } i \in s, \\ \emptyset & \text{otherwise.} \end{cases} \]
Set.mk_preimage_sigma_fn_eq_if theorem
{β : Type*} [DecidablePred (· ∈ s)] (g : β → α i) : (fun b ↦ Sigma.mk i (g b)) ⁻¹' s.sigma t = if i ∈ s then g ⁻¹' t i else ∅
Full source 
theorem mk_preimage_sigma_fn_eq_if {β : Type*} [DecidablePred (· ∈ s)] (g : β → α i) :
    (fun b ↦ Sigma.mk i (g b)) ⁻¹' s.sigma t = if i ∈ s then g ⁻¹' t i else ∅ :=
  ext fun _ ↦ by split_ifs <;> simp [*]
Preimage of Indexed Sum under Sigma Map with Conditional Result
Informal description
Let $s \subseteq \iota$ be a set with a decidable membership predicate, and let $t_i \subseteq \alpha_i$ be a family of sets indexed by $i \in \iota$. For any function $g : \beta \to \alpha_i$, the preimage of the indexed sum $\Sigma_{i \in s} t_i$ under the map $b \mapsto \langle i, g(b) \rangle$ is equal to $g^{-1}(t_i)$ if $i \in s$, and the empty set otherwise. That is: \[ \left\{b \in \beta \mid \langle i, g(b) \rangle \in \Sigma_{i \in s} t_i\right\} = \begin{cases} g^{-1}(t_i) & \text{if } i \in s, \\ \emptyset & \text{otherwise.} \end{cases} \]
Set.sigma_univ_range_eq theorem
{f : ∀ i, α i → β i} : (univ : Set ι).sigma (fun i ↦ range (f i)) = range fun x : Σ i, α i ↦ ⟨x.1, f _ x.2⟩
Full source 
theorem sigma_univ_range_eq {f : ∀ i, α i → β i} :
    (univ : Set ι).sigma (fun i ↦ range (f i)) = range fun x : Σ i, α i ↦ ⟨x.1, f _ x.2⟩ :=
  ext <| by simp [range, Sigma.forall]
Equality of Universal Sigma Range and Range of Sigma Map
Informal description
For any family of functions $f_i : \alpha_i \to \beta_i$ indexed by $i \in \iota$, the indexed sum of the universal set $\iota$ with the range sets of each $f_i$ is equal to the range of the function that maps each dependent pair $\langle i, a \rangle$ in $\Sigma i, \alpha_i$ to $\langle i, f_i(a) \rangle$. In other words: \[ \Sigma_{i \in \iota} \text{range}(f_i) = \text{range}\left(\lambda \langle i, a \rangle, \langle i, f_i(a) \rangle\right) \]
Set.Nonempty.sigma theorem
: s.Nonempty → (∀ i, (t i).Nonempty) → (s.sigma t).Nonempty
Full source 
protected theorem Nonempty.sigma :
    s.Nonempty → (∀ i, (t i).Nonempty) → (s.sigma t).Nonempty := fun ⟨i, hi⟩ h ↦
  let ⟨a, ha⟩ := h i
  ⟨⟨i, a⟩, hi, ha⟩
Nonemptiness of Indexed Sum of Nonempty Sets
Informal description
Given a nonempty set $s \subseteq \iota$ and a family of sets $t_i \subseteq \alpha_i$ for each $i \in \iota$ such that each $t_i$ is nonempty, the indexed sum $\Sigma i \in s, t_i$ is nonempty.
Set.Nonempty.sigma_fst theorem
: (s.sigma t).Nonempty → s.Nonempty
Full source 
theorem Nonempty.sigma_fst : (s.sigma t).Nonempty → s.Nonempty := fun ⟨x, hx⟩ ↦ ⟨x.1, hx.1⟩
Nonemptiness of First Component in Indexed Sum of Sets
Informal description
If the indexed sum $\Sigma i \in s, t_i$ is nonempty, then the index set $s$ is nonempty.
Set.Nonempty.sigma_snd theorem
: (s.sigma t).Nonempty → ∃ i ∈ s, (t i).Nonempty
Full source 
theorem Nonempty.sigma_snd : (s.sigma t).Nonempty → ∃ i ∈ s, (t i).Nonempty :=
  fun ⟨x, hx⟩ ↦ ⟨x.1, hx.1, x.2, hx.2⟩
Nonemptiness of Second Component in Indexed Sum of Sets
Informal description
If the indexed sum $\Sigma i \in s, t_i$ is nonempty, then there exists an index $i \in s$ such that the set $t_i$ is nonempty.
Set.sigma_eq_empty_iff theorem
: s.sigma t = ∅ ↔ ∀ i ∈ s, t i = ∅
Full source 
theorem sigma_eq_empty_iff : s.sigma t = ∅ ↔ ∀ i ∈ s, t i = ∅ :=
  not_nonempty_iff_eq_empty.symm.trans <|
    sigma_nonempty_iff.not.trans <| by
      simp only [not_nonempty_iff_eq_empty, not_and, not_exists]
Empty Indexed Sum Criterion: $\Sigma i \in s, t_i = \emptyset \leftrightarrow \forall i \in s, t_i = \emptyset$
Informal description
The indexed sum $\Sigma i \in s, t_i$ is equal to the empty set if and only if for every index $i \in s$, the set $t_i$ is empty.
Set.image_sigmaMk_subset_sigma_left theorem
{a : ∀ i, α i} (ha : ∀ i, a i ∈ t i) : (fun i ↦ Sigma.mk i (a i)) '' s ⊆ s.sigma t
Full source 
theorem image_sigmaMk_subset_sigma_left {a : ∀ i, α i} (ha : ∀ i, a i ∈ t i) :
    (fun i ↦ Sigma.mk i (a i)) '' s(fun i ↦ Sigma.mk i (a i)) '' s ⊆ s.sigma t :=
  image_subset_iff.2 fun _ hi ↦ ⟨hi, ha _⟩
Image of Index Map is Subset of Indexed Sum
Informal description
For any family of elements $a_i \in \alpha_i$ such that $a_i \in t_i$ for all $i$, the image of the set $s$ under the map $i \mapsto \langle i, a_i \rangle$ is a subset of the indexed sum $\Sigma i \in s, t_i$.
Set.image_sigmaMk_subset_sigma_right theorem
(hi : i ∈ s) : Sigma.mk i '' t i ⊆ s.sigma t
Full source 
theorem image_sigmaMk_subset_sigma_right (hi : i ∈ s) : Sigma.mkSigma.mk i '' t iSigma.mk i '' t i ⊆ s.sigma t :=
  image_subset_iff.2 fun _ ↦ And.intro hi
Inclusion of Right Injection in Indexed Sum: $\langle i, \cdot \rangle(t_i) \subseteq \Sigma_{j \in s} t_j$
Informal description
For any index $i \in s$ and any subset $t_i \subseteq \alpha_i$, the image of $t_i$ under the map $a \mapsto \langle i, a \rangle$ is contained in the indexed sum $\Sigma_{j \in s} t_j$. In symbols: \[ \{ \langle i, a \rangle \mid a \in t_i \} \subseteq \Sigma_{j \in s} t_j. \]
Set.sigma_subset_preimage_fst theorem
(s : Set ι) (t : ∀ i, Set (α i)) : s.sigma t ⊆ Sigma.fst ⁻¹' s
Full source 
theorem sigma_subset_preimage_fst (s : Set ι) (t : ∀ i, Set (α i)) : s.sigma t ⊆ Sigma.fst ⁻¹' s :=
  fun _ ↦ And.left
Indexed Sum is Subset of First Projection Preimage
Informal description
For any set $s \subseteq \iota$ and any family of sets $t_i \subseteq \alpha_i$ indexed by $i \in \iota$, the indexed sum $\Sigma i \in s, t_i$ is a subset of the preimage of $s$ under the first projection $\Sigma i, \alpha_i \to \iota$. In other words, if $\langle i, a \rangle \in \Sigma i \in s, t_i$, then $i \in s$.
Set.fst_image_sigma_subset theorem
(s : Set ι) (t : ∀ i, Set (α i)) : Sigma.fst '' s.sigma t ⊆ s
Full source 
theorem fst_image_sigma_subset (s : Set ι) (t : ∀ i, Set (α i)) : Sigma.fstSigma.fst '' s.sigma tSigma.fst '' s.sigma t ⊆ s :=
  image_subset_iff.2 fun _ ↦ And.left
First Projection Image of Indexed Sum is Subset of Index Set
Informal description
For any set $s \subseteq \iota$ and any family of sets $t_i \subseteq \alpha_i$ indexed by $i \in \iota$, the image of the indexed sum $\Sigma i \in s, t_i$ under the first projection $\Sigma.fst$ is a subset of $s$. In other words, if $\langle i, a \rangle \in \Sigma i \in s, t_i$, then $i \in s$.
Set.fst_image_sigma theorem
(s : Set ι) (ht : ∀ i, (t i).Nonempty) : Sigma.fst '' s.sigma t = s
Full source 
theorem fst_image_sigma (s : Set ι) (ht : ∀ i, (t i).Nonempty) : Sigma.fstSigma.fst '' s.sigma t = s :=
  (fst_image_sigma_subset _ _).antisymm fun i hi ↦
    let ⟨a, ha⟩ := ht i
    ⟨⟨i, a⟩, ⟨hi, ha⟩, rfl⟩
First Projection Maps Indexed Sum Onto Index Set for Nonempty Fibers
Informal description
For any set $s \subseteq \iota$ and any family of nonempty sets $t_i \subseteq \alpha_i$ indexed by $i \in \iota$, the image of the indexed sum $\Sigma i \in s, t_i$ under the first projection $\Sigma.fst$ is equal to $s$. In other words, the projection map $\langle i, a \rangle \mapsto i$ maps the dependent product $\Sigma i \in s, t_i$ exactly onto $s$ when each $t_i$ is nonempty.
Set.sigma_diff_sigma theorem
: s₁.sigma t₁ \ s₂.sigma t₂ = s₁.sigma (t₁ \ t₂) ∪ (s₁ \ s₂).sigma t₁
Full source 
theorem sigma_diff_sigma : s₁.sigma t₁ \ s₂.sigma t₂ = s₁.sigma (t₁ \ t₂) ∪ (s₁ \ s₂).sigma t₁ :=
  ext fun x ↦ by
    by_cases h₁ : x.1 ∈ s₁ <;> by_cases h₂ : x.2 ∈ t₁ x.1 <;> simp [*, ← imp_iff_or_not]
Difference of Indexed Sums of Sets
Informal description
For any sets $s_1, s_2 \subseteq \iota$ and families of sets $t_1, t_2$ where $t_1(i), t_2(i) \subseteq \alpha_i$ for each $i \in \iota$, the difference of the indexed sums satisfies: $$ (\Sigma i \in s_1, t_1(i)) \setminus (\Sigma i \in s_2, t_2(i)) = (\Sigma i \in s_1, t_1(i) \setminus t_2(i)) \cup (\Sigma i \in s_1 \setminus s_2, t_1(i)) $$