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)→ β i → Finset (γ i)→ Finset (γ i) to a map Σ i, α i → Σ i, β i → Finset (Σ i, γ i)→ Σ i, β i → Finset (Σ 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.

ink

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

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

ink

@[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

ink

@[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)

ink

@[simp]

theorem Finset.sigma_nonempty {ι : Type u_1} {α : ι → Type u_2} {s : Finset ι} {t : (i : ι) → Finset (α i)} : Finset.Nonempty (Finset.sigma s t) ↔ ∃ i, i ∈ s ∧ Finset.Nonempty (t i)

ink

@[simp]

theorem Finset.sigma_eq_empty {ι : Type u_1} {α : ι → Type u_2} {s : Finset ι} {t : (i : ι) → Finset (α i)} : Finset.sigma s t = ∅ ↔ ∀ (i : ι), i ∈ s → t i = ∅

ink

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₂

ink

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)

ink

@[simp]

theorem Finset.disjUnionᵢ_map_sigma_mk {ι : Type u_1} {α : ι → Type u_2} {s : Finset ι} {t : (i : ι) → Finset (α i)} : Finset.disjUnionᵢ s (fun i => Finset.map (Function.Embedding.sigmaMk i) (t i)) (_ : Set.PairwiseDisjoint ↑s fun i => Finset.map (Function.Embedding.sigmaMk i) (t i)) = Finset.sigma s t

ink

theorem Finset.sigma_eq_bunionᵢ {ι : Type u_2} {α : ι → Type u_1} [inst : DecidableEq ((i : ι) × α i)] (s : Finset ι) (t : (i : ι) → Finset (α i)) : Finset.sigma s t = Finset.bunionᵢ s fun i => Finset.map (Function.Embedding.sigmaMk i) (t i)

ink

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 }

ink

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 }

ink

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

• Finset.sigmaLift f a b = if h : a.fst = b.fst then Finset.map (Function.Embedding.sigmaMk b.fst) (f b.fst (h ▸ a.snd) b.snd) else ∅

ink

theorem Finset.mem_sigmaLift {ι : Type u_2} {α : ι → Type u_3} {β : ι → Type u_4} {γ : ι → Type u_1} [inst : DecidableEq ι] (f : ⦃i : ι⦄ → α i → β i → Finset (γ i)) (a : Sigma α) (b : Sigma β) (x : Sigma γ) : x ∈ Finset.sigmaLift f a b ↔ ∃ ha hb, x.snd ∈ f x.fst (ha ▸ a.snd) (hb ▸ b.snd)

ink

theorem Finset.mk_mem_sigmaLift {ι : Type u_2} {α : ι → Type u_3} {β : ι → Type u_4} {γ : ι → Type u_1} [inst : 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 i a b

ink

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

ink

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

ink

theorem Finset.sigmaLift_nonempty {ι : Type u_1} {α : ι → Type u_3} {β : ι → Type u_4} {γ : ι → Type u_2} [inst : DecidableEq ι] {f : ⦃i : ι⦄ → α i → β i → Finset (γ i)} {a : (i : ι) × α i} {b : (i : ι) × β i} : Finset.Nonempty (Finset.sigmaLift f a b) ↔ ∃ h, Finset.Nonempty (f b.fst (h ▸ a.snd) b.snd)

ink

theorem Finset.sigmaLift_eq_empty {ι : Type u_1} {α : ι → Type u_3} {β : ι → Type u_4} {γ : ι → Type u_2} [inst : DecidableEq ι] {f : ⦃i : ι⦄ → α i → β i → Finset (γ i)} {a : (i : ι) × α i} {b : (i : ι) × β i} : Finset.sigmaLift f a b = ∅ ↔ ∀ (h : a.fst = b.fst), f b.fst (h ▸ a.snd) b.snd = ∅

ink

theorem Finset.sigmaLift_mono {ι : Type u_2} {α : ι → Type u_3} {β : ι → Type u_4} {γ : ι → Type u_1} [inst : DecidableEq ι] {f : ⦃i : ι⦄ → α i → β i → Finset (γ i)} {g : ⦃i : ι⦄ → α i → β i → Finset (γ i)} (h : ∀ ⦃i : ι⦄ ⦃a : α i⦄ ⦃b : β i⦄, f i a b ⊆ g i a b) (a : (i : ι) × α i) (b : (i : ι) × β i) : Finset.sigmaLift f a b ⊆ Finset.sigmaLift g a b

ink

theorem Finset.card_sigmaLift {ι : Type u_1} {α : ι → Type u_3} {β : ι → Type u_4} {γ : ι → Type u_2} [inst : DecidableEq ι] (f : ⦃i : ι⦄ → α i → β i → Finset (γ 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 (h ▸ a.snd) b.snd) else 0