Documentation

Mathlib.Data.Finset.Sigma

Finite sets in a sigma type #

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

Main declarations #

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.

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∈ s and a ∈ t i∈ t i.

Equations
@[simp]
theorem Finset.mem_sigma {ι : Type u_1} {α : ιType u_2} {s : Finset ι} {t : (i : ι) → Finset (α i)} {a : (i : ι) × α i} :
a Finset.sigma s t a.fst s a.snd t a.fst
@[simp]
theorem Finset.coe_sigma {ι : Type u_1} {α : ιType u_2} (s : Finset ι) (t : (i : ι) → Finset (α i)) :
↑(Finset.sigma s t) = Set.Sigma s fun i => ↑(t i)
@[simp]
theorem Finset.sigma_nonempty {ι : Type u_1} {α : ιType u_2} {s : Finset ι} {t : (i : ι) → Finset (α i)} :
@[simp]
theorem Finset.sigma_eq_empty {ι : Type u_1} {α : ιType u_2} {s : Finset ι} {t : (i : ι) → Finset (α i)} :
Finset.sigma s t = ∀ (i : ι), i st i =
theorem Finset.sigma_mono {ι : Type u_1} {α : ιType u_2} {s₁ : Finset ι} {s₂ : Finset ι} {t₁ : (i : ι) → Finset (α i)} {t₂ : (i : ι) → Finset (α i)} (hs : s₁ s₂) (ht : ∀ (i : ι), t₁ i t₂ i) :
Finset.sigma s₁ t₁ Finset.sigma s₂ t₂
theorem Finset.pairwiseDisjoint_map_sigmaMk {ι : Type u_1} {α : ιType u_2} {s : Finset ι} {t : (i : ι) → Finset (α i)} :
@[simp]
theorem Finset.disjUnionᵢ_map_sigma_mk {ι : Type u_1} {α : ιType u_2} {s : Finset ι} {t : (i : ι) → Finset (α i)} :
theorem Finset.sigma_eq_bunionᵢ {ι : Type u_2} {α : ιType u_1} [inst : DecidableEq ((i : ι) × α i)] (s : Finset ι) (t : (i : ι) → Finset (α i)) :
theorem Finset.sup_sigma {ι : Type u_2} {α : ιType u_3} {β : Type u_1} (s : Finset ι) (t : (i : ι) → Finset (α i)) (f : (i : ι) × α iβ) [inst : SemilatticeSup β] [inst : OrderBot β] :
Finset.sup (Finset.sigma s t) f = Finset.sup s fun i => Finset.sup (t i) fun b => f { fst := i, snd := b }
theorem Finset.inf_sigma {ι : Type u_2} {α : ιType u_3} {β : Type u_1} (s : Finset ι) (t : (i : ι) → Finset (α i)) (f : (i : ι) × α iβ) [inst : SemilatticeInf β] [inst : OrderTop β] :
Finset.inf (Finset.sigma s t) f = Finset.inf s fun i => Finset.inf (t i) fun b => f { fst := i, snd := b }
def Finset.sigmaLift {ι : Type u_1} {α : ιType u_2} {β : ιType u_3} {γ : ιType u_4} [inst : DecidableEq ι] (f : i : ι⦄ → α iβ iFinset (γ i)) (a : Sigma α) (b : Sigma β) :

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

Equations
theorem Finset.mem_sigmaLift {ι : Type u_2} {α : ιType u_3} {β : ιType u_4} {γ : ιType u_1} [inst : DecidableEq ι] (f : i : ι⦄ → α iβ iFinset (γ i)) (a : Sigma α) (b : Sigma β) (x : Sigma γ) :
x Finset.sigmaLift f a b ha hb, x.snd f x.fst (haa.snd) (hbb.snd)
theorem Finset.mk_mem_sigmaLift {ι : Type u_2} {α : ιType u_3} {β : ιType u_4} {γ : ιType u_1} [inst : DecidableEq ι] (f : i : ι⦄ → α iβ iFinset (γ i)) (i : ι) (a : α i) (b : β i) (x : γ i) :
{ fst := i, snd := x } Finset.sigmaLift f { fst := i, snd := a } { fst := i, snd := b } x f i a b
theorem Finset.not_mem_sigmaLift_of_ne_left {ι : Type u_2} {α : ιType u_3} {β : ιType u_4} {γ : ιType u_1} [inst : DecidableEq ι] (f : i : ι⦄ → α iβ iFinset (γ i)) (a : Sigma α) (b : Sigma β) (x : Sigma γ) (h : a.fst x.fst) :
theorem Finset.not_mem_sigmaLift_of_ne_right {ι : Type u_2} {α : ιType u_3} {β : ιType u_4} {γ : ιType u_1} [inst : DecidableEq ι] (f : i : ι⦄ → α iβ iFinset (γ i)) {a : Sigma α} (b : Sigma β) {x : Sigma γ} (h : b.fst x.fst) :
theorem Finset.sigmaLift_nonempty {ι : Type u_1} {α : ιType u_3} {β : ιType u_4} {γ : ιType u_2} [inst : DecidableEq ι] {f : i : ι⦄ → α iβ iFinset (γ i)} {a : (i : ι) × α i} {b : (i : ι) × β i} :
Finset.Nonempty (Finset.sigmaLift f a b) h, Finset.Nonempty (f b.fst (ha.snd) b.snd)
theorem Finset.sigmaLift_eq_empty {ι : Type u_1} {α : ιType u_3} {β : ιType u_4} {γ : ιType u_2} [inst : DecidableEq ι] {f : i : ι⦄ → α iβ iFinset (γ i)} {a : (i : ι) × α i} {b : (i : ι) × β i} :
Finset.sigmaLift f a b = ∀ (h : a.fst = b.fst), f b.fst (ha.snd) b.snd =
theorem Finset.sigmaLift_mono {ι : Type u_2} {α : ιType u_3} {β : ιType u_4} {γ : ιType u_1} [inst : DecidableEq ι] {f : i : ι⦄ → α iβ iFinset (γ i)} {g : i : ι⦄ → α iβ iFinset (γ i)} (h : ∀ ⦃i : ι⦄ ⦃a : α i⦄ ⦃b : β i⦄, f i a b g i a b) (a : (i : ι) × α i) (b : (i : ι) × β i) :
theorem Finset.card_sigmaLift {ι : Type u_1} {α : ιType u_3} {β : ιType u_4} {γ : ιType u_2} [inst : DecidableEq ι] (f : i : ι⦄ → α iβ iFinset (γ i)) (a : (i : ι) × α i) (b : (i : ι) × β i) :
Finset.card (Finset.sigmaLift f a b) = if h : a.fst = b.fst then Finset.card (f b.fst (ha.snd) b.snd) else 0