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.

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

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

@[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 = ∅ ↔ ∀ i ∈ s, 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)} : Set.PairwiseDisjoint ↑s fun (i : ι) => Finset.map (Function.Embedding.sigmaMk i) (t i)

@[simp]

theorem Finset.disjiUnion_map_sigma_mk {ι : Type u_1} {α : ι → Type u_2} {s : Finset ι} {t : (i : ι) → Finset (α i)} : Finset.disjiUnion s (fun (i : ι) => Finset.map (Function.Embedding.sigmaMk i) (t i)) ⋯ = Finset.sigma s t

theorem Finset.sigma_eq_biUnion {ι : Type u_1} {α : ι → Type u_2} [DecidableEq ((i : ι) × α i)] (s : Finset ι) (t : (i : ι) → Finset (α i)) : Finset.sigma s t = Finset.biUnion s fun (i : ι) => Finset.map (Function.Embedding.sigmaMk i) (t 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 : ι) → α i → Set β) : ⋃ 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 : ι) → α i → Set β) : ⋂ 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 → β 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 ∅

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 ∈ Finset.sigmaLift f a b ↔ ∃ (ha : a.fst = x.fst) (hb : b.fst = x.fst), x.snd ∈ f (ha ▸ a.snd) (hb ▸ b.snd)

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) : { 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 → β i → Finset (γ i)) (a : Sigma α) (b : Sigma β) (x : Sigma γ) (h : a.fst ≠ x.fst) : x ∉ Finset.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 → β i → Finset (γ i)) {a : Sigma α} (b : Sigma β) {x : Sigma γ} (h : b.fst ≠ x.fst) : x ∉ Finset.sigmaLift f a b

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} : (Finset.sigmaLift f a b).Nonempty ↔ ∃ (h : a.fst = b.fst), (f (h ▸ a.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 → β i → Finset (γ i)} {a : (i : ι) × α i} {b : (i : ι) × β i} : Finset.sigmaLift f a b = ∅ ↔ ∀ (h : a.fst = b.fst), f (h ▸ a.snd) b.snd = ∅

theorem Finset.sigmaLift_mono {ι : Type u_1} {α : ι → Type u_2} {β : ι → Type u_3} {γ : ι → Type u_4} [DecidableEq ι] {f : ⦃i : ι⦄ → α i → β i → Finset (γ i)} {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.sigmaLift f a b ⊆ Finset.sigmaLift g a b

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) : (Finset.sigmaLift f a b).card = if h : a.fst = b.fst then (f (h ▸ a.snd) b.snd).card else 0