# Finite sets in a sigma type #

This file defines a few `Finset` constructions on `Σ i, α i`.

## Main declarations #

- `Finset.sigma`: Given a finset `s` in `ι` and finsets `t i` in each `α i`, `s.sigma t` is the finset of the dependent sum `Σ i, α i`
- `Finset.sigmaLift`: Lifts maps `α i → β i → Finset (γ i)` to a map `Σ i, α i → Σ i, β i → Finset (Σ i, γ i)`.

## TODO #

`Finset.sigmaLift` can be generalized to any alternative functor. But to make the generalization worth it, we must first refactor the functor library so that the `alternative` instance for `Finset` is computable and universe-polymorphic.

source
def Finset.sigma {ι : Type u_1} {α : ι → Type u_2} (s : Finset ι) (t : (i : ι) → Finset (α i)) :
Finset ((i : ι) × α i)

`s.sigma t` is the finset of dependent pairs `⟨i, a⟩` such that `i ∈ s` and `a ∈ t i`.

Equations

- s.sigma t = { val := s.val.sigma fun (i : ι) => (t i).val, nodup := ⋯ }

Instances For

source
@[simp]
theorem Finset.mem_sigma {ι : Type u_1} {α : ι → Type u_2} {s : Finset ι} {t : (i : ι) → Finset (α i)} {a : (i : ι) × α i} :
a ∈ s.sigma t ↔ a.fst ∈ s ∧ a.snd ∈ t a.fst
source
@[simp]
theorem Finset.coe_sigma {ι : Type u_1} {α : ι → Type u_2} (s : Finset ι) (t : (i : ι) → Finset (α i)) :
↑(s.sigma t) = (↑s).sigma fun (i : ι) => ↑(t i)
source
@[simp]
theorem Finset.sigma_nonempty {ι : Type u_1} {α : ι → Type u_2} {s : Finset ι} {t : (i : ι) → Finset (α i)} :
(s.sigma t).Nonempty ↔ ∃ i ∈ s, (t i).Nonempty
source
theorem Finset.Aesop.sigma_nonempty_of_exists_nonempty {ι : Type u_1} {α : ι → Type u_2} {s : Finset ι} {t : (i : ι) → Finset (α i)} :
(∃ i ∈ s, (t i).Nonempty) → (s.sigma t).Nonempty

Alias of the reverse direction of `Finset.sigma_nonempty`.

source
@[simp]
theorem Finset.sigma_eq_empty {ι : Type u_1} {α : ι → Type u_2} {s : Finset ι} {t : (i : ι) → Finset (α i)} :
s.sigma t = ∅ ↔ ∀ i ∈ s, t i = ∅
source
theorem Finset.sigma_mono {ι : Type u_1} {α : ι → Type u_2} {s₁ s₂ : Finset ι} {t₁ t₂ : (i : ι) → Finset (α i)} (hs : s₁ ⊆ s₂) (ht : ∀ (i : ι), t₁ i ⊆ t₂ i) :
s₁.sigma t₁ ⊆ s₂.sigma t₂
source
theorem Finset.pairwiseDisjoint_map_sigmaMk {ι : Type u_1} {α : ι → Type u_2} {s : Finset ι} {t : (i : ι) → Finset (α i)} :
(↑s).PairwiseDisjoint fun (i : ι) => map (Function.Embedding.sigmaMk i) (t i)
source
@[simp]
theorem Finset.disjiUnion_map_sigma_mk {ι : Type u_1} {α : ι → Type u_2} {s : Finset ι} {t : (i : ι) → Finset (α i)} :
s.disjiUnion (fun (i : ι) => map (Function.Embedding.sigmaMk i) (t i)) ⋯ = s.sigma t
source
theorem Finset.sigma_eq_biUnion {ι : Type u_1} {α : ι → Type u_2} [DecidableEq ((i : ι) × α i)] (s : Finset ι) (t : (i : ι) → Finset (α i)) :
s.sigma t = s.biUnion fun (i : ι) => map (Function.Embedding.sigmaMk i) (t i)
source
theorem Finset.sup_sigma {ι : Type u_1} {α : ι → Type u_2} {β : Type u_3} (s : Finset ι) (t : (i : ι) → Finset (α i)) (f : (i : ι) × α i → β) [SemilatticeSup β] [OrderBot β] :
(s.sigma t).sup f = s.sup fun (i : ι) => (t i).sup fun (b : α i) => f ⟨i, b⟩
source
theorem Finset.inf_sigma {ι : Type u_1} {α : ι → Type u_2} {β : Type u_3} (s : Finset ι) (t : (i : ι) → Finset (α i)) (f : (i : ι) × α i → β) [SemilatticeInf β] [OrderTop β] :
(s.sigma t).inf f = s.inf fun (i : ι) => (t i).inf fun (b : α i) => f ⟨i, b⟩
source
theorem biSup_finsetSigma {ι : Type u_1} {α : ι → Type u_2} {β : Type u_3} [CompleteLattice β] (s : Finset ι) (t : (i : ι) → Finset (α i)) (f : Sigma α → β) :
⨆ ij ∈ s.sigma t, f ij = ⨆ i ∈ s, ⨆ j ∈ t i, f ⟨i, j⟩
source
theorem biSup_finsetSigma' {ι : Type u_1} {α : ι → Type u_2} {β : Type u_3} [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
source
theorem biInf_finsetSigma {ι : Type u_1} {α : ι → Type u_2} {β : Type u_3} [CompleteLattice β] (s : Finset ι) (t : (i : ι) → Finset (α i)) (f : Sigma α → β) :
⨅ ij ∈ s.sigma t, f ij = ⨅ i ∈ s, ⨅ j ∈ t i, f ⟨i, j⟩
source
theorem biInf_finsetSigma' {ι : Type u_1} {α : ι → Type u_2} {β : Type u_3} [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
source
theorem Set.biUnion_finsetSigma {ι : Type u_1} {α : ι → Type u_2} {β : Type u_3} (s : Finset ι) (t : (i : ι) → Finset (α i)) (f : Sigma α → Set β) :
⋃ ij ∈ s.sigma t, f ij = ⋃ i ∈ s, ⋃ j ∈ t i, f ⟨i, j⟩
source
theorem Set.biUnion_finsetSigma' {ι : Type u_1} {α : ι → Type u_2} {β : Type u_3} (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
source
theorem Set.biInter_finsetSigma {ι : Type u_1} {α : ι → Type u_2} {β : Type u_3} (s : Finset ι) (t : (i : ι) → Finset (α i)) (f : Sigma α → Set β) :
⋂ ij ∈ s.sigma t, f ij = ⋂ i ∈ s, ⋂ j ∈ t i, f ⟨i, j⟩
source
theorem Set.biInter_finsetSigma' {ι : Type u_1} {α : ι → Type u_2} {β : Type u_3} (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
source
def Finset.sigmaLift {ι : Type u_1} {α : ι → Type u_2} {β : ι → Type u_3} {γ : ι → Type u_4} [DecidableEq ι] (f : ⦃i : ι⦄ → α i → β i → Finset (γ i)) (a : Sigma α) (b : Sigma β) :
Finset (Sigma γ)

Lifts maps `α i → β i → Finset (γ i)` to a map `Σ i, α i → Σ i, β i → Finset (Σ i, γ i)`.

Equations

- Finset.sigmaLift f a b = if h : a.fst = b.fst then Finset.map (Function.Embedding.sigmaMk b.fst) (f (h ▸ a.snd) b.snd) else ∅

Instances For

source
theorem Finset.mem_sigmaLift {ι : Type u_1} {α : ι → Type u_2} {β : ι → Type u_3} {γ : ι → Type u_4} [DecidableEq ι] (f : ⦃i : ι⦄ → α i → β i → Finset (γ i)) (a : Sigma α) (b : Sigma β) (x : Sigma γ) :
x ∈ sigmaLift f a b ↔ ∃ (ha : a.fst = x.fst) (hb : b.fst = x.fst), x.snd ∈ f (ha ▸ a.snd) (hb ▸ b.snd)
source
theorem Finset.mk_mem_sigmaLift {ι : Type u_1} {α : ι → Type u_2} {β : ι → Type u_3} {γ : ι → Type u_4} [DecidableEq ι] (f : ⦃i : ι⦄ → α i → β i → Finset (γ i)) (i : ι) (a : α i) (b : β i) (x : γ i) :
⟨i, x⟩ ∈ sigmaLift f ⟨i, a⟩ ⟨i, b⟩ ↔ x ∈ f a b
source
theorem Finset.notMem_sigmaLift_of_ne_left {ι : Type u_1} {α : ι → Type u_2} {β : ι → Type u_3} {γ : ι → Type u_4} [DecidableEq ι] (f : ⦃i : ι⦄ → α i → β i → Finset (γ i)) (a : Sigma α) (b : Sigma β) (x : Sigma γ) (h : a.fst ≠ x.fst) :
x ∉ sigmaLift f a b
source
@[deprecated Finset.notMem_sigmaLift_of_ne_left (since := "2025-05-23")]
theorem Finset.not_mem_sigmaLift_of_ne_left {ι : Type u_1} {α : ι → Type u_2} {β : ι → Type u_3} {γ : ι → Type u_4} [DecidableEq ι] (f : ⦃i : ι⦄ → α i → β i → Finset (γ i)) (a : Sigma α) (b : Sigma β) (x : Sigma γ) (h : a.fst ≠ x.fst) :
x ∉ sigmaLift f a b

Alias of `Finset.notMem_sigmaLift_of_ne_left`.

source
theorem Finset.notMem_sigmaLift_of_ne_right {ι : Type u_1} {α : ι → Type u_2} {β : ι → Type u_3} {γ : ι → Type u_4} [DecidableEq ι] (f : ⦃i : ι⦄ → α i → β i → Finset (γ i)) {a : Sigma α} (b : Sigma β) {x : Sigma γ} (h : b.fst ≠ x.fst) :
x ∉ sigmaLift f a b
source
@[deprecated Finset.notMem_sigmaLift_of_ne_right (since := "2025-05-23")]
theorem Finset.not_mem_sigmaLift_of_ne_right {ι : Type u_1} {α : ι → Type u_2} {β : ι → Type u_3} {γ : ι → Type u_4} [DecidableEq ι] (f : ⦃i : ι⦄ → α i → β i → Finset (γ i)) {a : Sigma α} (b : Sigma β) {x : Sigma γ} (h : b.fst ≠ x.fst) :
x ∉ sigmaLift f a b

Alias of `Finset.notMem_sigmaLift_of_ne_right`.

source
theorem Finset.sigmaLift_nonempty {ι : Type u_1} {α : ι → Type u_2} {β : ι → Type u_3} {γ : ι → Type u_4} [DecidableEq ι] {f : ⦃i : ι⦄ → α i → β i → Finset (γ i)} {a : (i : ι) × α i} {b : (i : ι) × β i} :
(sigmaLift f a b).Nonempty ↔ ∃ (h : a.fst = b.fst), (f (h ▸ a.snd) b.snd).Nonempty
source
theorem Finset.sigmaLift_eq_empty {ι : Type u_1} {α : ι → Type u_2} {β : ι → Type u_3} {γ : ι → Type u_4} [DecidableEq ι] {f : ⦃i : ι⦄ → α i → β i → Finset (γ i)} {a : (i : ι) × α i} {b : (i : ι) × β i} :
sigmaLift f a b = ∅ ↔ ∀ (h : a.fst = b.fst), f (h ▸ a.snd) b.snd = ∅
source
theorem Finset.sigmaLift_mono {ι : Type u_1} {α : ι → Type u_2} {β : ι → Type u_3} {γ : ι → Type u_4} [DecidableEq ι] {f g : ⦃i : ι⦄ → α i → β i → Finset (γ i)} (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
source
theorem Finset.card_sigmaLift {ι : Type u_1} {α : ι → Type u_2} {β : ι → Type u_3} {γ : ι → Type u_4} [DecidableEq ι] (f : ⦃i : ι⦄ → α i → β i → Finset (γ i)) (a : (i : ι) × α i) (b : (i : ι) × β i) :
(sigmaLift f a b).card = if h : a.fst = b.fst then (f (h ▸ a.snd) b.snd).card else 0