mathlib3 documentation

data.finset.sigma

Finite sets in a sigma type #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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

Main declarations #

TODO #

finset.sigma_lift 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
@[protected]
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
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, norm_cast]
theorem finset.coe_sigma {ι : Type u_1} {α : ι → Type u_2} (s : finset ι) (t : Π (i : ι), finset (α i)) :
↑(s.sigma t) = ↑s.sigma (λ (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 : ι) (H : i ∈ s), (t i).nonempty
source
@[simp]
theorem finset.sigma_eq_empty {ι : Type u_1} {α : ι → Type u_2} {s : finset ι} {t : Π (i : ι), finset (α i)} :
s.sigma t = ∅ ↔ ∀ (i : ι), 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.pairwise_disjoint_map_sigma_mk {ι : Type u_1} {α : ι → Type u_2} {s : finset ι} {t : Π (i : ι), finset (α i)} :
↑s.pairwise_disjoint (λ (i : ι), finset.map (function.embedding.sigma_mk i) (t i))
source
@[simp]
theorem finset.disj_Union_map_sigma_mk {ι : Type u_1} {α : ι → Type u_2} {s : finset ι} {t : Π (i : ι), finset (α i)} :
s.disj_Union (λ (i : ι), finset.map (function.embedding.sigma_mk i) (t i)) finset.pairwise_disjoint_map_sigma_mk = s.sigma t
source
theorem finset.sigma_eq_bUnion {ι : Type u_1} {α : ι → Type u_2} [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⟩))
source
def finset.sigma_lift {ι : Type u_1} {α : ι → Type u_2} {β : ι → Type u_3} {γ : ι → Type u_4} [decidable_eq ι] (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
source
theorem finset.mem_sigma_lift {ι : Type u_1} {α : ι → Type u_2} {β : ι → Type u_3} {γ : ι → Type u_4} [decidable_eq ι] (f : Π ⦃i : ι⦄, α i → β i → finset (γ i)) (a : sigma α) (b : sigma β) (x : sigma γ) :
x ∈ finset.sigma_lift f a b ↔ ∃ (ha : a.fst = x.fst) (hb : b.fst = x.fst), x.snd ∈ f (eq.rec a.snd ha) (eq.rec b.snd hb)
source
theorem finset.mk_mem_sigma_lift {ι : Type u_1} {α : ι → Type u_2} {β : ι → Type u_3} {γ : ι → Type u_4} [decidable_eq ι] (f : Π ⦃i : ι⦄, α i → β i → finset (γ i)) (i : ι) (a : α i) (b : β i) (x : γ i) :
⟨i, x⟩ ∈ finset.sigma_lift f ⟨i, a⟩ ⟨i, b⟩ ↔ x ∈ f a b
source
theorem finset.not_mem_sigma_lift_of_ne_left {ι : Type u_1} {α : ι → Type u_2} {β : ι → Type u_3} {γ : ι → Type u_4} [decidable_eq ι] (f : Π ⦃i : ι⦄, α i → β i → finset (γ i)) (a : sigma α) (b : sigma β) (x : sigma γ) (h : a.fst ≠ x.fst) :
x ∉ finset.sigma_lift f a b
source
theorem finset.not_mem_sigma_lift_of_ne_right {ι : Type u_1} {α : ι → Type u_2} {β : ι → Type u_3} {γ : ι → Type u_4} [decidable_eq ι] (f : Π ⦃i : ι⦄, α i → β i → finset (γ i)) {a : sigma α} (b : sigma β) {x : sigma γ} (h : b.fst ≠ x.fst) :
x ∉ finset.sigma_lift f a b
source
theorem finset.sigma_lift_nonempty {ι : Type u_1} {α : ι → Type u_2} {β : ι → Type u_3} {γ : ι → Type u_4} [decidable_eq ι] {f : Π ⦃i : ι⦄, α i → β i → finset (γ i)} {a : Σ (i : ι), α i} {b : Σ (i : ι), β i} :
(finset.sigma_lift f a b).nonempty ↔ ∃ (h : a.fst = b.fst), (f (eq.rec a.snd h) b.snd).nonempty
source
theorem finset.sigma_lift_eq_empty {ι : Type u_1} {α : ι → Type u_2} {β : ι → Type u_3} {γ : ι → Type u_4} [decidable_eq ι] {f : Π ⦃i : ι⦄, α i → β i → finset (γ i)} {a : Σ (i : ι), α i} {b : Σ (i : ι), β i} :
finset.sigma_lift f a b = ∅ ↔ ∀ (h : a.fst = b.fst), f (eq.rec a.snd h) b.snd = ∅
source
theorem finset.sigma_lift_mono {ι : Type u_1} {α : ι → Type u_2} {β : ι → Type u_3} {γ : ι → Type u_4} [decidable_eq ι] {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) :
finset.sigma_lift f a b ⊆ finset.sigma_lift g a b
source
theorem finset.card_sigma_lift {ι : Type u_1} {α : ι → Type u_2} {β : ι → Type u_3} {γ : ι → Type u_4} [decidable_eq ι] (f : Π ⦃i : ι⦄, α i → β i → finset (γ i)) (a : Σ (i : ι), α i) (b : Σ (i : ι), β i) :
(finset.sigma_lift f a b).card = dite (a.fst = b.fst) (λ (h : a.fst = b.fst), (f (eq.rec a.snd h) b.snd).card) (λ (_x : ¬a.fst = b.fst), 0)