Mathlib.Data.Finset.Sigma

Finset.sigma definition

: Finset (Σ i, α i)

Full source

/-- `s.sigma t` is the finset of dependent pairs `⟨i, a⟩` such that `i ∈ s` and `a ∈ t i`. -/
protected def sigma : Finset (Σ i, α i) :=
  ⟨_, s.nodup.sigma fun i => (t i).nodup⟩

Dependent sum of finite sets

Informal description

Given a finite set $s$ over an index type $\iota$ and a family of finite sets $t(i)$ over types $\alpha_i$ for each $i \in \iota$, the dependent sum $s.\text{sigma}\, t$ is the finite set of dependent pairs $\langle i, a \rangle$ where $i$ ranges over $s$ and $a$ ranges over $t(i)$.

Finset.mem_sigma theorem

{a : Σ i, α i} : a ∈ s.sigma t ↔ a.1 ∈ s ∧ a.2 ∈ t a.1

Full source

@[simp]
theorem mem_sigma {a : Σ i, α i} : a ∈ s.sigma ta ∈ s.sigma t ↔ a.1 ∈ s ∧ a.2 ∈ t a.1 :=
  Multiset.mem_sigma

Membership Criterion for Finite Dependent Sum Set: $a \in s.\text{sigma}\, t \leftrightarrow a.1 \in s \land a.2 \in t(a.1)$

Informal description

For any dependent pair $a = (i, x)$ in the sigma type $\Sigma i, \alpha i$, $a$ is an element of the finite dependent sum set $s.\text{sigma}\, t$ if and only if the first component $i$ is an element of the finite set $s$ and the second component $x$ is an element of the finite set $t(i)$.

Finset.coe_sigma theorem

 (s : Finset ι) (t : ∀ i, Finset (α i)) : (s.sigma t : Set (Σ i, α i)) = (s : Set ι).sigma fun i ↦ (t i : Set (α i))

Full source

@[simp, norm_cast]
theorem coe_sigma (s : Finset ι) (t : ∀ i, Finset (α i)) :
    (s.sigma t : Set (Σ i, α i)) = (s : Set ι).sigma fun i ↦ (t i : Set (α i)) :=
  Set.ext fun _ => mem_sigma

Equality of Finite Dependent Sum and Its Underlying Set

Informal description

For any finite set $s$ over an index type $\iota$ and any family of finite sets $t(i)$ over types $\alpha_i$ for $i \in \iota$, the underlying set of the dependent sum $s.\text{sigma}\, t$ is equal to the indexed sum of the underlying sets of $s$ and $t(i)$. That is, $$(s.\text{sigma}\, t : \text{Set} (\Sigma i, \alpha i)) = (s : \text{Set} \iota).\text{sigma} \left( \lambda i, (t i : \text{Set} (\alpha i)) \right).$$

Finset.sigma_nonempty theorem

: (s.sigma t).Nonempty ↔ ∃ i ∈ s, (t i).Nonempty

Full source

@[simp]
theorem sigma_nonempty : (s.sigma t).Nonempty ↔ ∃ i ∈ s, (t i).Nonempty := by simp [Finset.Nonempty]

Nonemptiness Criterion for Finite Dependent Sum Set: $s.\text{sigma}\, t \neq \emptyset \leftrightarrow \exists i \in s, t(i) \neq \emptyset$

Informal description

The dependent sum finite set $s.\text{sigma}\, t$ is nonempty if and only if there exists an index $i \in s$ such that the finite set $t(i)$ is nonempty.

Finset.sigma_eq_empty theorem

: s.sigma t = ∅ ↔ ∀ i ∈ s, t i = ∅

Full source

@[simp]
theorem sigma_eq_empty : s.sigma t = ∅ ↔ ∀ i ∈ s, t i = ∅ := by
  simp only [← not_nonempty_iff_eq_empty, sigma_nonempty, not_exists, not_and]

Empty Dependent Sum Criterion: $s.\mathrm{sigma}\, t = \emptyset \leftrightarrow \forall i \in s, t(i) = \emptyset$

Informal description

The dependent sum finite set $s.\mathrm{sigma}\, t$ is empty if and only if for every index $i$ in $s$, the finite set $t(i)$ is empty.

Finset.sigma_mono theorem

(hs : s₁ ⊆ s₂) (ht : ∀ i, t₁ i ⊆ t₂ i) : s₁.sigma t₁ ⊆ s₂.sigma t₂

Full source

@[mono]
theorem sigma_mono (hs : s₁ ⊆ s₂) (ht : ∀ i, t₁ i ⊆ t₂ i) : s₁.sigma t₁ ⊆ s₂.sigma t₂ :=
  fun ⟨i, _⟩ h =>
  let ⟨hi, ha⟩ := mem_sigma.1 h
  mem_sigma.2 ⟨hs hi, ht i ha⟩

Monotonicity of Finite Dependent Sum Construction: $s_1 \subseteq s_2 \land (\forall i, t_1(i) \subseteq t_2(i)) \implies s_1.\text{sigma}\, t_1 \subseteq s_2.\text{sigma}\, t_2$

Informal description

Let $s_1$ and $s_2$ be finite subsets of an index type $\iota$ with $s_1 \subseteq s_2$, and let $t_1(i)$ and $t_2(i)$ be finite subsets of $\alpha_i$ for each $i \in \iota$ such that $t_1(i) \subseteq t_2(i)$ for all $i$. Then the dependent sum $s_1.\text{sigma}\, t_1$ is a subset of the dependent sum $s_2.\text{sigma}\, t_2$.

Finset.pairwiseDisjoint_map_sigmaMk theorem

: (s : Set ι).PairwiseDisjoint fun i => (t i).map (Embedding.sigmaMk i)

Full source

theorem pairwiseDisjoint_map_sigmaMk :
    (s : Set ι).PairwiseDisjoint fun i => (t i).map (Embedding.sigmaMk i) := by
  intro i _ j _ hij
  rw [Function.onFun, disjoint_left]
  simp_rw [mem_map, Function.Embedding.sigmaMk_apply]
  rintro _ ⟨y, _, rfl⟩ ⟨z, _, hz'⟩
  exact hij (congr_arg Sigma.fst hz'.symm)

Pairwise Disjointness of Injective Images in Dependent Sum Construction

Informal description

For a set $s$ of indices of type $\iota$ and a family of finite sets $t(i)$ of type $\alpha_i$ for each $i \in \iota$, the images of $t(i)$ under the injective embeddings $\text{Embedding.sigmaMk}\, i : \alpha_i \hookrightarrow \Sigma i, \alpha_i$ are pairwise disjoint. That is, for any two distinct indices $i, j \in s$, the finite sets $\text{map}\, (\text{Embedding.sigmaMk}\, i)\, (t(i))$ and $\text{map}\, (\text{Embedding.sigmaMk}\, j)\, (t(j))$ are disjoint.

Finset.disjiUnion_map_sigma_mk theorem

: s.disjiUnion (fun i => (t i).map (Embedding.sigmaMk i)) pairwiseDisjoint_map_sigmaMk = s.sigma t

Full source

@[simp]
theorem disjiUnion_map_sigma_mk :
    s.disjiUnion (fun i => (t i).map (Embedding.sigmaMk i)) pairwiseDisjoint_map_sigmaMk =
      s.sigma t :=
  rfl

Disjoint Union of Injective Images Equals Dependent Sum of Finite Sets

Informal description

For a finite set $s$ of type $\iota$ and a family of finite sets $t(i)$ of type $\alpha_i$ for each $i \in \iota$, the disjoint union of the images of $t(i)$ under the injective embeddings $\text{Embedding.sigmaMk}\, i : \alpha_i \hookrightarrow \Sigma i, \alpha_i$ is equal to the dependent sum $s.\text{sigma}\, t$. More precisely, we have: $$ \text{disjiUnion}\, s\, (\lambda i, \text{map}\, (\text{Embedding.sigmaMk}\, i)\, (t(i)))\, \text{pairwiseDisjoint\_map\_sigmaMk} = s.\text{sigma}\, t $$ where the disjointness condition ensures that the union is indeed disjoint.

Finset.sigma_eq_biUnion theorem

 [DecidableEq (Σ i, α i)] (s : Finset ι) (t : ∀ i, Finset (α i)) :
  s.sigma t = s.biUnion fun i => (t i).map <| Embedding.sigmaMk i

Full source

theorem sigma_eq_biUnion [DecidableEq (Σ i, α i)] (s : Finset ι) (t : ∀ i, Finset (α i)) :
    s.sigma t = s.biUnion fun i => (t i).map <| Embedding.sigmaMk i := by
  ext ⟨x, y⟩
  simp [and_left_comm]

Dependent Sum as Union of Injective Images

Informal description

For a finite set $s$ of type $\iota$ and a family of finite sets $t(i)$ of type $\alpha_i$ for each $i \in \iota$, the dependent sum $s.\text{sigma}\, t$ is equal to the finite union over $s$ of the images of $t(i)$ under the injective embedding $\text{Embedding.sigmaMk}\, i : \alpha_i \hookrightarrow \Sigma i, \alpha_i$. More precisely, under the assumption that equality is decidable for elements of $\Sigma i, \alpha_i$, we have: $$ s.\text{sigma}\, t = \bigcup_{i \in s} \text{map}\, (\text{Embedding.sigmaMk}\, i)\, (t(i)) $$ where $\text{map}$ applies the embedding to each element of $t(i)$ and $\bigcup$ denotes the finite union.

Finset.sup_sigma theorem

[SemilatticeSup β] [OrderBot β] : (s.sigma t).sup f = s.sup fun i => (t i).sup fun b => f ⟨i, b⟩

Full source

theorem sup_sigma [SemilatticeSup β] [OrderBot β] :
    (s.sigma t).sup f = s.sup fun i => (t i).sup fun b => f ⟨i, b⟩ := by
  simp only [le_antisymm_iff, Finset.sup_le_iff, mem_sigma, and_imp, Sigma.forall]
  exact
    ⟨fun i a hi ha => (le_sup hi).trans' <| le_sup (f := fun a => f ⟨i, a⟩) ha, fun i hi a ha =>
      le_sup <| mem_sigma.2 ⟨hi, ha⟩⟩

Supremum over Finite Dependent Sum Equals Iterated Supremum

Informal description

Let $\beta$ be a join-semilattice with a bottom element $\bot$, $s$ a finite set over an index type $\iota$, and $t_i$ a family of finite sets over types $\alpha_i$ for each $i \in \iota$. For any function $f : \Sigma i, \alpha_i \to \beta$, the supremum of $f$ over the dependent sum $s.\text{sigma}\, t$ is equal to the supremum over $s$ of the suprema of $f$ over each $t_i$. That is, \[ \sup_{\langle i, j \rangle \in s.\text{sigma}\, t} f(i, j) = \sup_{i \in s} \sup_{j \in t_i} f(i, j). \]

Finset.inf_sigma theorem

[SemilatticeInf β] [OrderTop β] : (s.sigma t).inf f = s.inf fun i => (t i).inf fun b => f ⟨i, b⟩

Full source

theorem inf_sigma [SemilatticeInf β] [OrderTop β] :
    (s.sigma t).inf f = s.inf fun i => (t i).inf fun b => f ⟨i, b⟩ :=
  @sup_sigma _ _ βᵒᵈ _ _ _ _ _

Infimum over Finite Dependent Sum Equals Iterated Infimum

Informal description

Let $\beta$ be a meet-semilattice with a greatest element $\top$, $s$ a finite set over an index type $\iota$, and $t_i$ a family of finite sets over types $\alpha_i$ for each $i \in \iota$. For any function $f : \Sigma i, \alpha_i \to \beta$, the infimum of $f$ over the dependent sum $s.\text{sigma}\, t$ is equal to the infimum over $s$ of the infima of $f$ over each $t_i$. That is, \[ \inf_{\langle i, j \rangle \in s.\text{sigma}\, t} f(i, j) = \inf_{i \in s} \inf_{j \in t_i} f(i, j). \]

biSup_finsetSigma theorem

 [CompleteLattice β] (s : Finset ι) (t : ∀ i, Finset (α i)) (f : Sigma α → β) :
  ⨆ ij ∈ s.sigma t, f ij = ⨆ (i ∈ s) (j ∈ t i), f ⟨i, j⟩

Full source

theorem _root_.biSup_finsetSigma [CompleteLattice β] (s : Finset ι) (t : ∀ i, Finset (α i))
    (f : Sigma α → β) : ⨆ ij ∈ s.sigma t, f ij = ⨆ (i ∈ s) (j ∈ t i), f ⟨i, j⟩ := by
  simp_rw [← Finset.iSup_coe, Finset.coe_sigma, biSup_sigma]

Supremum over Finite Dependent Sum Equals Iterated Supremum

Informal description

Let $\beta$ be a complete lattice, $s$ a finite set over an index type $\iota$, and $t_i$ a family of finite sets over types $\alpha_i$ for each $i \in \iota$. For any function $f : \Sigma i, \alpha_i \to \beta$, the supremum of $f$ over the dependent sum $s.\text{sigma}\, t$ 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 s.\text{sigma}\, t} f(i, j) = \bigsqcup_{i \in s} \bigsqcup_{j \in t_i} f(i, j). \]

biSup_finsetSigma' theorem

 [CompleteLattice β] (s : Finset ι) (t : ∀ i, Finset (α 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_finsetSigma' [CompleteLattice β] (s : Finset ι) (t : ∀ i, Finset (α i))
    (f : ∀ i, α i → β) : ⨆ (i ∈ s) (j ∈ t i), f i j = ⨆ ij ∈ s.sigma t, f ij.fst ij.snd :=
  Eq.symm (biSup_finsetSigma _ _ _)

Iterated Supremum Equals Supremum over Finite Dependent Sum

Informal description

Let $\beta$ be a complete lattice, $s$ a finite set over an index type $\iota$, and $t_i$ a family of finite sets over types $\alpha_i$ for each $i \in \iota$. For any family of functions $f_i : \alpha_i \to \beta$, the iterated supremum of $f_i(j)$ over $i \in s$ and $j \in t_i$ is equal to the supremum of $f_{ij.\text{fst}}(ij.\text{snd})$ over the dependent sum $s.\text{sigma}\, t$. That is, \[ \bigsqcup_{i \in s} \bigsqcup_{j \in t_i} f_i(j) = \bigsqcup_{\langle i, j \rangle \in s.\text{sigma}\, t} f_i(j). \]

biInf_finsetSigma theorem

 [CompleteLattice β] (s : Finset ι) (t : ∀ i, Finset (α i)) (f : Sigma α → β) :
  ⨅ ij ∈ s.sigma t, f ij = ⨅ (i ∈ s) (j ∈ t i), f ⟨i, j⟩

Full source

theorem _root_.biInf_finsetSigma [CompleteLattice β] (s : Finset ι) (t : ∀ i, Finset (α i))
    (f : Sigma α → β) : ⨅ ij ∈ s.sigma t, f ij = ⨅ (i ∈ s) (j ∈ t i), f ⟨i, j⟩ :=
  biSup_finsetSigma (β := βᵒᵈ) _ _ _

Infimum over Finite Dependent Sum Equals Iterated Infimum

Informal description

Let $\beta$ be a complete lattice, $s$ a finite set over an index type $\iota$, and $t_i$ a family of finite sets over types $\alpha_i$ for each $i \in \iota$. For any function $f : \Sigma i, \alpha_i \to \beta$, the infimum of $f$ over the dependent sum $s.\text{sigma}\, t$ 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 s.\text{sigma}\, t} f(i, j) = \bigsqcap_{i \in s} \bigsqcap_{j \in t_i} f(i, j). \]

biInf_finsetSigma' theorem

 [CompleteLattice β] (s : Finset ι) (t : ∀ i, Finset (α 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_finsetSigma' [CompleteLattice β] (s : Finset ι) (t : ∀ i, Finset (α i))
    (f : ∀ i, α i → β) : ⨅ (i ∈ s) (j ∈ t i), f i j = ⨅ ij ∈ s.sigma t, f ij.fst ij.snd :=
  Eq.symm (biInf_finsetSigma _ _ _)

Iterated Infimum Equals Infimum over Finite Dependent Sum

Informal description

Let $\beta$ be a complete lattice, $s$ a finite set over an index type $\iota$, and $t_i$ a family of finite sets over types $\alpha_i$ for each $i \in \iota$. For any family of functions $f_i : \alpha_i \to \beta$, 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 the dependent sum $s.\text{sigma}\, t$. That is, \[ \bigsqcap_{i \in s} \bigsqcap_{j \in t_i} f_i(j) = \bigsqcap_{\langle i, j \rangle \in s.\text{sigma}\, t} f_i(j). \]

Set.biUnion_finsetSigma theorem

 (s : Finset ι) (t : ∀ i, Finset (α i)) (f : Sigma α → Set β) : ⋃ ij ∈ s.sigma t, f ij = ⋃ i ∈ s, ⋃ j ∈ t i, f ⟨i, j⟩

Full source

theorem _root_.Set.biUnion_finsetSigma (s : Finset ι) (t : ∀ i, Finset (α i))
    (f : Sigma α → Set β) : ⋃ ij ∈ s.sigma t, f ij = ⋃ i ∈ s, ⋃ j ∈ t i, f ⟨i, j⟩ :=
  biSup_finsetSigma _ _ _

Union over Finite Dependent Sum Equals Iterated Union

Informal description

Let $s$ be a finite set over an index type $\iota$, and for each $i \in \iota$, let $t_i$ be a finite set over a type $\alpha_i$. For any function $f : \Sigma i, \alpha_i \to \text{Set } \beta$, the union of $f$ over the dependent sum $s.\text{sigma}\, t$ is equal to the iterated union of $f$ over $i \in s$ and $j \in t_i$. That is, \[ \bigcup_{\langle i, j \rangle \in s.\text{sigma}\, t} f(i, j) = \bigcup_{i \in s} \bigcup_{j \in t_i} f(i, j). \]

Set.biUnion_finsetSigma' theorem

 (s : Finset ι) (t : ∀ i, Finset (α 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 _root_.Set.biUnion_finsetSigma' (s : Finset ι) (t : ∀ i, Finset (α i))
    (f : ∀ i, α i → Set β) : ⋃ i ∈ s, ⋃ j ∈ t i, f i j = ⋃ ij ∈ s.sigma t, f ij.fst ij.snd :=
  biSup_finsetSigma' _ _ _

Union over Finite Dependent Sum Equals Iterated Union

Informal description

Let $s$ be a finite set over an index type $\iota$, and for each $i \in \iota$, let $t_i$ be a finite set over a type $\alpha_i$. Given a family of functions $f_i : \alpha_i \to \text{Set } \beta$, the union of the sets $f_i(j)$ over all $i \in s$ and $j \in t_i$ is equal to the union of the sets $f_{ij.\text{fst}}(ij.\text{snd})$ over all dependent pairs $\langle i, j \rangle$ in the finite dependent sum $s.\text{sigma}\, t$. That is, \[ \bigcup_{i \in s} \bigcup_{j \in t_i} f_i(j) = \bigcup_{\langle i, j \rangle \in s.\text{sigma}\, t} f_i(j). \]

Set.biInter_finsetSigma theorem

 (s : Finset ι) (t : ∀ i, Finset (α i)) (f : Sigma α → Set β) : ⋂ ij ∈ s.sigma t, f ij = ⋂ i ∈ s, ⋂ j ∈ t i, f ⟨i, j⟩

Full source

theorem _root_.Set.biInter_finsetSigma (s : Finset ι) (t : ∀ i, Finset (α i))
    (f : Sigma α → Set β) : ⋂ ij ∈ s.sigma t, f ij = ⋂ i ∈ s, ⋂ j ∈ t i, f ⟨i, j⟩ :=
  biInf_finsetSigma _ _ _

Iterated Intersection over Finite Dependent Sum

Informal description

For any finite set $s$ over an index type $\iota$, any family of finite sets $t_i$ over types $\alpha_i$ for each $i \in \iota$, and any function $f : \Sigma i, \alpha_i \to \text{Set } \beta$, the intersection of $f$ over the dependent sum $s.\text{sigma}\, t$ is equal to the iterated intersection of $f$ over $i \in s$ and $j \in t_i$. That is, \[ \bigcap_{\langle i, j \rangle \in s.\text{sigma}\, t} f(i, j) = \bigcap_{i \in s} \bigcap_{j \in t_i} f(i, j). \]

Set.biInter_finsetSigma' theorem

 (s : Finset ι) (t : ∀ i, Finset (α i)) (f : ∀ i, α i → Set β) :
  ⋂ i ∈ s, ⋂ j ∈ t i, f i j = ⋂ ij ∈ s.sigma t, f ij.1 ij.2

Full source

theorem _root_.Set.biInter_finsetSigma' (s : Finset ι) (t : ∀ i, Finset (α i))
    (f : ∀ i, α i → Set β) : ⋂ i ∈ s, ⋂ j ∈ t i, f i j = ⋂ ij ∈ s.sigma t, f ij.1 ij.2 :=
  biInf_finsetSigma' _ _ _

Iterated Intersection Equals Intersection over Finite Dependent Sum

Informal description

For any finite set $s$ over an index type $\iota$, any family of finite sets $t_i$ over types $\alpha_i$ for each $i \in \iota$, and any family of functions $f_i : \alpha_i \to \text{Set } \beta$, the iterated intersection of $f_i(j)$ over $i \in s$ and $j \in t_i$ is equal to the intersection of $f_{ij.1}(ij.2)$ over all dependent pairs $\langle i, j \rangle$ in the finite dependent sum $s.\text{sigma}\, t$. That is, \[ \bigcap_{i \in s} \bigcap_{j \in t_i} f_i(j) = \bigcap_{\langle i, j \rangle \in s.\text{sigma}\, t} f_i(j). \]

Finset.sigmaLift definition

(f : ∀ ⦃i⦄, α i → β i → Finset (γ i)) (a : Sigma α) (b : Sigma β) : Finset (Sigma γ)

Full source

/-- Lifts maps `α i → β i → Finset (γ i)` to a map `Σ i, α i → Σ i, β i → Finset (Σ i, γ i)`. -/
def sigmaLift (f : ∀ ⦃i⦄, α i → β i → Finset (γ i)) (a : Sigma α) (b : Sigma β) :
    Finset (Sigma γ) :=
  dite (a.1 = b.1) (fun h => (f (h ▸ a.2) b.2).map <| Embedding.sigmaMk _) fun _ => ∅

Lifting of finite set-valued functions to dependent pairs

Informal description

Given a family of functions $ f_i : \alpha_i \to \beta_i \to \text{Finset}(\gamma_i) $ indexed by $ i \in \iota $, the function `sigmaLift` lifts these to a function $ \Sigma i, \alpha_i \to \Sigma i, \beta_i \to \text{Finset}(\Sigma i, \gamma_i) $. Specifically, for dependent pairs $ a = (i, a') \in \Sigma i, \alpha_i $ and $ b = (j, b') \in \Sigma i, \beta_i $, if $ i = j $, then `sigmaLift f a b` is the image of $ f_i a' b' $ under the embedding $ \gamma_i \hookrightarrow \Sigma i, \gamma_i $ at index $ i $; otherwise, it is the empty set.

Finset.mem_sigmaLift theorem

 (f : ∀ ⦃i⦄, α i → β i → Finset (γ i)) (a : Sigma α) (b : Sigma β) (x : Sigma γ) :
  x ∈ sigmaLift f a b ↔ ∃ (ha : a.1 = x.1) (hb : b.1 = x.1), x.2 ∈ f (ha ▸ a.2) (hb ▸ b.2)

Full source

theorem mem_sigmaLift (f : ∀ ⦃i⦄, α i → β i → Finset (γ i)) (a : Sigma α) (b : Sigma β)
    (x : Sigma γ) :
    x ∈ sigmaLift f a bx ∈ sigmaLift f a b ↔ ∃ (ha : a.1 = x.1) (hb : b.1 = x.1), x.2 ∈ f (ha ▸ a.2) (hb ▸ b.2) := by
  obtain ⟨⟨i, a⟩, j, b⟩ := a, b
  obtain rfl | h := Decidable.eq_or_ne i j
  · constructor
    · simp_rw [sigmaLift]
      simp only [dite_eq_ite, ite_true, mem_map, Embedding.sigmaMk_apply, forall_exists_index,
        and_imp]
      rintro x hx rfl
      exact ⟨rfl, rfl, hx⟩
    · rintro ⟨⟨⟩, ⟨⟩, hx⟩
      rw [sigmaLift, dif_pos rfl, mem_map]
      exact ⟨_, hx, by simp [Sigma.ext_iff]⟩
  · rw [sigmaLift, dif_neg h]
    refine iff_of_false (not_mem_empty _) ?_
    rintro ⟨⟨⟩, ⟨⟩, _⟩
    exact h rfl

Characterization of Membership in Lifted Sigma Finite Set

Informal description

Let $f$ be a family of functions $f_i : \alpha_i \to \beta_i \to \text{Finset}(\gamma_i)$ indexed by $i \in \iota$. For dependent pairs $a = (i, a') \in \Sigma i, \alpha_i$, $b = (j, b') \in \Sigma i, \beta_i$, and $x = (k, x') \in \Sigma i, \gamma_i$, we have: $$ x \in \text{sigmaLift}\,f\,a\,b \leftrightarrow \exists (ha : i = k) (hb : j = k), x' \in f_i (ha \triangleright a') (hb \triangleright b') $$ where $ha \triangleright a'$ denotes the transport of $a'$ along the equality $ha : i = k$, and similarly for $hb \triangleright b'$.

Finset.mk_mem_sigmaLift theorem

 (f : ∀ ⦃i⦄, α i → β i → Finset (γ i)) (i : ι) (a : α i) (b : β i) (x : γ i) :
  (⟨i, x⟩ : Sigma γ) ∈ sigmaLift f ⟨i, a⟩ ⟨i, b⟩ ↔ x ∈ f a b

Full source

theorem mk_mem_sigmaLift (f : ∀ ⦃i⦄, α i → β i → Finset (γ i)) (i : ι) (a : α i) (b : β i)
    (x : γ i) : (⟨i, x⟩ : Sigma γ) ∈ sigmaLift f ⟨i, a⟩ ⟨i, b⟩(⟨i, x⟩ : Sigma γ) ∈ sigmaLift f ⟨i, a⟩ ⟨i, b⟩ ↔ x ∈ f a b := by
  rw [sigmaLift, dif_pos rfl, mem_map]
  refine ⟨?_, fun hx => ⟨_, hx, rfl⟩⟩
  rintro ⟨x, hx, _, rfl⟩
  exact hx

Membership in Lifted Sigma-Type Finite Set at Fixed Index

Informal description

Let $f_i : \alpha_i \to \beta_i \to \text{Finset}(\gamma_i)$ be a family of set-valued functions indexed by $i \in \iota$. For any $i \in \iota$, $a \in \alpha_i$, $b \in \beta_i$, and $x \in \gamma_i$, the dependent pair $\langle i, x \rangle$ belongs to the lifted set $\text{sigmaLift}\, f\, \langle i, a \rangle\, \langle i, b \rangle$ if and only if $x$ belongs to $f_i\, a\, b$.

Finset.not_mem_sigmaLift_of_ne_left theorem

 (f : ∀ ⦃i⦄, α i → β i → Finset (γ i)) (a : Sigma α) (b : Sigma β) (x : Sigma γ) (h : a.1 ≠ x.1) : x ∉ sigmaLift f a b

Full source

theorem not_mem_sigmaLift_of_ne_left (f : ∀ ⦃i⦄, α i → β i → Finset (γ i)) (a : Sigma α)
    (b : Sigma β) (x : Sigma γ) (h : a.1 ≠ x.1) : x ∉ sigmaLift f a b := by
  rw [mem_sigmaLift]
  exact fun H => h H.fst

Non-membership in Lifted Sigma-Type Finite Set Due to Index Mismatch on Left

Informal description

Let $f_i : \alpha_i \to \beta_i \to \text{Finset}(\gamma_i)$ be a family of set-valued functions indexed by $i \in \iota$. For dependent pairs $a = (i, a') \in \Sigma i, \alpha_i$, $b = (j, b') \in \Sigma i, \beta_i$, and $x = (k, x') \in \Sigma i, \gamma_i$, if $i \neq k$, then $x$ does not belong to the lifted set $\text{sigmaLift}\,f\,a\,b$.

Finset.not_mem_sigmaLift_of_ne_right theorem

 (f : ∀ ⦃i⦄, α i → β i → Finset (γ i)) {a : Sigma α} (b : Sigma β) {x : Sigma γ} (h : b.1 ≠ x.1) : x ∉ sigmaLift f a b

Full source

theorem not_mem_sigmaLift_of_ne_right (f : ∀ ⦃i⦄, α i → β i → Finset (γ i)) {a : Sigma α}
    (b : Sigma β) {x : Sigma γ} (h : b.1 ≠ x.1) : x ∉ sigmaLift f a b := by
  rw [mem_sigmaLift]
  exact fun H => h H.snd.fst

Non-membership in Lifted Sigma-Type Finite Set Due to Index Mismatch on Right

Informal description

Let $f_i : \alpha_i \to \beta_i \to \text{Finset}(\gamma_i)$ be a family of set-valued functions indexed by $i \in \iota$. For dependent pairs $a = (i, a') \in \Sigma i, \alpha_i$, $b = (j, b') \in \Sigma i, \beta_i$, and $x = (k, x') \in \Sigma i, \gamma_i$, if $j \neq k$, then $x$ does not belong to the lifted set $\text{sigmaLift}\,f\,a\,b$.

Finset.sigmaLift_nonempty theorem

: (sigmaLift f a b).Nonempty ↔ ∃ h : a.1 = b.1, (f (h ▸ a.2) b.2).Nonempty

Full source

theorem sigmaLift_nonempty :
    (sigmaLift f a b).Nonempty ↔ ∃ h : a.1 = b.1, (f (h ▸ a.2) b.2).Nonempty := by
  simp_rw [nonempty_iff_ne_empty, sigmaLift]
  split_ifs with h <;> simp [h]

Nonemptiness Condition for Lifted Finite Set-Valued Function on Dependent Pairs

Informal description

For a family of functions $f_i : \alpha_i \to \beta_i \to \text{Finset}(\gamma_i)$ indexed by $i \in \iota$, and for dependent pairs $a = (i, a') \in \Sigma i, \alpha_i$ and $b = (j, b') \in \Sigma i, \beta_i$, the finite set $\text{sigmaLift}\,f\,a\,b$ is nonempty if and only if $i = j$ and the finite set $f_i\,a'\,b'$ is nonempty.

Finset.sigmaLift_eq_empty theorem

: sigmaLift f a b = ∅ ↔ ∀ h : a.1 = b.1, f (h ▸ a.2) b.2 = ∅

Full source

theorem sigmaLift_eq_empty : sigmaLiftsigmaLift f a b = ∅ ↔ ∀ h : a.1 = b.1, f (h ▸ a.2) b.2 = ∅ := by
  simp_rw [sigmaLift]
  split_ifs with h
  · simp [h, forall_prop_of_true h]
  · simp [h, forall_prop_of_false h]

Emptyness condition for lifted sigma sets: $\text{sigmaLift}\,f\,a\,b = \emptyset \leftrightarrow \forall h : i = j, f_i\,(h \triangleright a')\,b' = \emptyset$

Informal description

For a family of functions $f_i : \alpha_i \to \beta_i \to \text{Finset}(\gamma_i)$ and dependent pairs $a = (i, a') \in \Sigma i, \alpha_i$ and $b = (j, b') \in \Sigma i, \beta_i$, the lifted set $\text{sigmaLift}\,f\,a\,b$ is empty if and only if for every proof $h$ that $i = j$, the set $f_i\,(h \triangleright a')\,b'$ is empty.

Finset.sigmaLift_mono theorem

 (h : ∀ ⦃i⦄ ⦃a : α i⦄ ⦃b : β i⦄, f a b ⊆ g a b) (a : Σ i, α i) (b : Σ i, β i) : sigmaLift f a b ⊆ sigmaLift g a b

Full source

theorem sigmaLift_mono
    (h : ∀ ⦃i⦄ ⦃a : α i⦄ ⦃b : β i⦄, f a b ⊆ g a b) (a : Σ i, α i) (b : Σ i, β i) :
    sigmaLiftsigmaLift f a b ⊆ sigmaLift g a b := by
  rintro x hx
  rw [mem_sigmaLift] at hx ⊢
  obtain ⟨ha, hb, hx⟩ := hx
  exact ⟨ha, hb, h hx⟩

Monotonicity of Sigma Lift for Finite Sets

Informal description

Let $\{f_i : \alpha_i \to \beta_i \to \text{Finset}(\gamma_i)\}_{i \in \iota}$ and $\{g_i : \alpha_i \to \beta_i \to \text{Finset}(\gamma_i)\}_{i \in \iota}$ be families of set-valued functions such that for all $i \in \iota$, $a \in \alpha_i$, and $b \in \beta_i$, we have $f_i(a, b) \subseteq g_i(a, b)$. Then for any dependent pairs $a = (i, a') \in \Sigma i, \alpha_i$ and $b = (j, b') \in \Sigma i, \beta_i$, the lifted finite sets satisfy $\text{sigmaLift}\,f\,a\,b \subseteq \text{sigmaLift}\,g\,a\,b$.

Finset.card_sigmaLift theorem

: (sigmaLift f a b).card = dite (a.1 = b.1) (fun h => (f (h ▸ a.2) b.2).card) fun _ => 0

Full source

theorem card_sigmaLift :
    (sigmaLift f a b).card = dite (a.1 = b.1) (fun h => (f (h ▸ a.2) b.2).card) fun _ => 0 := by
  simp_rw [sigmaLift]
  split_ifs with h <;> simp [h]

Cardinality of Lifted Finite Set on Dependent Pairs

Informal description

For any dependent pairs $a = (i, a') \in \Sigma i, \alpha_i$ and $b = (j, b') \in \Sigma i, \beta_i$, the cardinality of the finite set `sigmaLift f a b` is equal to the cardinality of $f_i(a', b')$ if $i = j$, and zero otherwise. In other words: \[ |\text{sigmaLift}\,f\,a\,b| = \begin{cases} |f_i(a', b')| & \text{if } i = j, \\ 0 & \text{otherwise.} \end{cases} \]

Mathlib.Data.Finset.Sigma

Main declarations

TODO