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

Equations
Instances For
    @[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)} :
    (Finset.sigma s t).Nonempty ∃ i ∈ s, (t i).Nonempty
    @[simp]
    theorem Finset.sigma_eq_empty {ι : Type u_1} {α : ιType u_2} {s : Finset ι} {t : (i : ι) → Finset (α i)} :
    Finset.sigma s t = is, t 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.disjiUnion_map_sigma_mk {ι : Type u_1} {α : ιType u_2} {s : Finset ι} {t : (i : ι) → Finset (α i)} :
    theorem Finset.sigma_eq_biUnion {ι : Type u_1} {α : ιType u_2} [DecidableEq ((i : ι) × α i)] (s : Finset ι) (t : (i : ι) → Finset (α i)) :
    theorem Finset.sup_sigma {ι : Type u_1} {α : ιType u_2} {β : Type u_3} (s : Finset ι) (t : (i : ι) → Finset (α i)) (f : (i : ι) × α iβ) [SemilatticeSup β] [OrderBot β] :
    Finset.sup (Finset.sigma s t) f = Finset.sup s fun (i : ι) => Finset.sup (t i) fun (b : α i) => f { fst := i, snd := b }
    theorem Finset.inf_sigma {ι : Type u_1} {α : ιType u_2} {β : Type u_3} (s : Finset ι) (t : (i : ι) → Finset (α i)) (f : (i : ι) × α iβ) [SemilatticeInf β] [OrderTop β] :
    Finset.inf (Finset.sigma s t) f = Finset.inf s fun (i : ι) => Finset.inf (t i) fun (b : α i) => f { fst := i, snd := b }
    theorem biSup_finsetSigma {ι : Type u_1} {α : ιType u_2} {β : Type u_3} [CompleteLattice β] (s : Finset ι) (t : (i : ι) → Finset (α i)) (f : Sigma αβ) :
    ⨆ ij ∈ Finset.sigma s t, f ij = ⨆ i ∈ s, ⨆ j ∈ t i, f { fst := i, snd := j }
    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 ∈ Finset.sigma s t, f ij.fst ij.snd
    theorem biInf_finsetSigma {ι : Type u_1} {α : ιType u_2} {β : Type u_3} [CompleteLattice β] (s : Finset ι) (t : (i : ι) → Finset (α i)) (f : Sigma αβ) :
    ⨅ ij ∈ Finset.sigma s t, f ij = ⨅ i ∈ s, ⨅ j ∈ t i, f { fst := i, snd := j }
    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 ∈ Finset.sigma s t, f ij.fst ij.snd
    theorem Set.biUnion_finsetSigma {ι : Type u_1} {α : ιType u_2} {β : Type u_3} (s : Finset ι) (t : (i : ι) → Finset (α i)) (f : Sigma αSet β) :
    ⋃ ij ∈ Finset.sigma s t, f ij = ⋃ i ∈ s, ⋃ j ∈ t i, f { fst := i, snd := j }
    theorem Set.biUnion_finsetSigma' {ι : Type u_1} {α : ιType u_2} {β : Type u_3} (s : Finset ι) (t : (i : ι) → Finset (α i)) (f : (i : ι) → α iSet β) :
    ⋃ i ∈ s, ⋃ j ∈ t i, f i j = ⋃ ij ∈ Finset.sigma s t, f ij.fst ij.snd
    theorem Set.biInter_finsetSigma {ι : Type u_1} {α : ιType u_2} {β : Type u_3} (s : Finset ι) (t : (i : ι) → Finset (α i)) (f : Sigma αSet β) :
    ⋂ ij ∈ Finset.sigma s t, f ij = ⋂ i ∈ s, ⋂ j ∈ t i, f { fst := i, snd := j }
    theorem Set.biInter_finsetSigma' {ι : Type u_1} {α : ιType u_2} {β : Type u_3} (s : Finset ι) (t : (i : ι) → Finset (α i)) (f : (i : ι) → α iSet β) :
    ⋂ i ∈ s, ⋂ j ∈ t i, f i j = ⋂ ij ∈ Finset.sigma s t, f ij.fst ij.snd
    def Finset.sigmaLift {ι : Type u_1} {α : ιType u_2} {β : ιType u_3} {γ : ιType u_4} [DecidableEq ι] (f : i : ι⦄ → α iβ iFinset (γ i)) (a : Sigma α) (b : Sigma β) :

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

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