mathlib documentation

data.finset.sigma

Finite sets in a sigma type #

This file defines a finset construction on Σ i, α i.

Main declarations #

source
@[protected]
def finset.sigma {ι : Type u_1} {α : ι → Type u_3} (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
source
@[simp]
theorem finset.mem_sigma {ι : Type u_1} {α : ι → Type u_3} {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.sigma_nonempty {ι : Type u_1} {α : ι → Type u_3} {s : finset ι} {t : Π (i : ι), finset (α i)} :
(s.sigma t).nonempty ↔ ∃ (i : ι) (H : i ∈ s), (t i).nonempty
source
@[simp]
theorem finset.sigma_eq_empty {ι : Type u_1} {α : ι → Type u_3} {s : finset ι} {t : Π (i : ι), finset (α i)} :
s.sigma t = ∅ ↔ ∀ (i : ι), i ∈ s → t i = ∅
source
theorem finset.sigma_mono {ι : Type u_1} {α : ι → Type u_3} {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.sigma_eq_bUnion {ι : Type u_1} {α : ι → Type u_3} [decidable_eq (Σ (i : ι), α i)] (s : finset ι) (t : Π (i : ι), finset (α i)) :
s.sigma t = s.bUnion (λ (i : ι), finset.map (function.embedding.sigma_mk 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) → β) [semilattice_sup β] [order_bot β] :
(s.sigma t).sup f = s.sup (λ (i : ι), (t i).sup (λ (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) → β) [semilattice_inf β] [order_top β] :
(s.sigma t).inf f = s.inf (λ (i : ι), (t i).inf (λ (b : α i), f ⟨i, b⟩))