Module docstring
{"# fintype instances for sigma types "}
Set.biUnion_finsetSigma_univ
theorem
(s : Finset ι) (f : Sigma κ → Set α) : ⋃ ij ∈ s.sigma fun _ ↦ Finset.univ, f ij = ⋃ i ∈ s, ⋃ j, f ⟨i, j⟩
Full source
lemma Set.biUnion_finsetSigma_univ (s : Finset ι) (f : Sigma κ → Set α) :
⋃ ij ∈ s.sigma fun _ ↦ Finset.univ, f ij = ⋃ i ∈ s, ⋃ j, f ⟨i, j⟩ := by aesopInformal description
For any finite set $s$ of indices of type $\iota$ and any function $f$ mapping pairs $(i, j)$ (where $i \in s$ and $j$ is of type $\kappa i$) to sets of type $\alpha$, the union of $f$ over all pairs $(i, j)$ in the product of $s$ with the universal finite set (for each $i$) is equal to the union over all $i \in s$ of the union of $f(i, j)$ over all $j$.
In symbols:
\[
\bigcup_{(i,j) \in s \times \text{univ}} f(i,j) = \bigcup_{i \in s} \bigcup_{j} f(i,j)
\]
Set.biUnion_finsetSigma_univ'
theorem
(s : Finset ι) (f : Π i, κ i → Set α) : ⋃ i ∈ s, ⋃ j, f i j = ⋃ ij ∈ s.sigma fun _ ↦ Finset.univ, f ij.1 ij.2
Full source
lemma Set.biUnion_finsetSigma_univ' (s : Finset ι) (f : Π i, κ i → Set α) :
⋃ i ∈ s, ⋃ j, f i j = ⋃ ij ∈ s.sigma fun _ ↦ Finset.univ, f ij.1 ij.2 := by aesopInformal description
For any finite set $s$ of indices of type $\iota$ and any family of sets $f_i(j) : \kappa i \to \text{Set } \alpha$ indexed by $i \in s$, the union over all $i \in s$ and all $j$ of $f_i(j)$ is equal to the union over all pairs $(i,j)$ in the product of $s$ with the universal finite set (for each $i$) of $f_i(j)$.
In symbols:
\[
\bigcup_{i \in s} \bigcup_{j} f_i(j) = \bigcup_{(i,j) \in s \times \text{univ}} f_i(j)
\]
Set.biInter_finsetSigma_univ
theorem
(s : Finset ι) (f : Sigma κ → Set α) : ⋂ ij ∈ s.sigma fun _ ↦ Finset.univ, f ij = ⋂ i ∈ s, ⋂ j, f ⟨i, j⟩
Full source
lemma Set.biInter_finsetSigma_univ (s : Finset ι) (f : Sigma κ → Set α) :
⋂ ij ∈ s.sigma fun _ ↦ Finset.univ, f ij = ⋂ i ∈ s, ⋂ j, f ⟨i, j⟩ := by aesopInformal description
For any finite set $s$ of indices of type $\iota$ and any function $f$ mapping pairs $(i, j)$ (where $i \in s$ and $j$ is of type $\kappa i$) to sets of type $\alpha$, the intersection of $f$ over all pairs $(i, j)$ in the product of $s$ with the universal finite set (for each $i$) is equal to the intersection over all $i \in s$ of the intersection of $f(i, j)$ over all $j$.
In symbols:
\[
\bigcap_{(i,j) \in s \times \text{univ}} f(i,j) = \bigcap_{i \in s} \bigcap_{j} f(i,j)
\]
Set.biInter_finsetSigma_univ'
theorem
(s : Finset ι) (f : Π i, κ i → Set α) : ⋂ i ∈ s, ⋂ j, f i j = ⋂ ij ∈ s.sigma fun _ ↦ Finset.univ, f ij.1 ij.2
Full source
lemma Set.biInter_finsetSigma_univ' (s : Finset ι) (f : Π i, κ i → Set α) :
⋂ i ∈ s, ⋂ j, f i j = ⋂ ij ∈ s.sigma fun _ ↦ Finset.univ, f ij.1 ij.2 := by aesopInformal description
For any finite set $s$ of indices of type $\iota$ and any family of sets $f_i(j) : \kappa i \to \text{Set } \alpha$ indexed by $i \in s$ and $j \in \kappa i$, the intersection over all $i \in s$ and all $j$ of $f_i(j)$ is equal to the intersection over all pairs $(i,j)$ in the product of $s$ with the universal finite set (for each $i$) of $f_i(j)$.
In symbols:
\[
\bigcap_{i \in s} \bigcap_{j} f_i(j) = \bigcap_{(i,j) \in s \times \text{univ}} f_i(j)
\]
Sigma.instFintype
instance
: Fintype (Σ i, κ i)
Full source
instance Sigma.instFintype : Fintype (Σ i, κ i) := ⟨univ.sigma fun _ ↦ univ, by simp⟩Informal description
For any finite type $ι$ and a family of finite types $κ_i$ indexed by $i \in ι$, the dependent sum type $\Sigma i, κ_i$ is also finite.
PSigma.instFintype
instance
: Fintype (Σ' i, κ i)
Full source
instance PSigma.instFintype : Fintype (Σ' i, κ i) := .ofEquiv _ (Equiv.psigmaEquivSigma _).symmInformal description
For any finite type $ι$ and a family of finite types $κ_i$ indexed by $i \in ι$, the dependent sum type $\Sigma' i, κ_i$ (a `PSigma` type) is also finite.
Finset.univ_sigma_univ
theorem
: univ.sigma (fun _ ↦ univ) = (univ : Finset (Σ i, κ i))
Informal description
For a finite type $ι$ and a family of finite types $κ_i$ indexed by $i \in ι$, the Cartesian product of the universal finite sets of $ι$ and each $κ_i$ equals the universal finite set of the dependent sum type $\Sigma i, κ_i$. In other words, $\text{univ}.\text{sigma} (\lambda \_, \text{univ}) = \text{univ} : \text{Finset} (\Sigma i, κ_i)$.