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.

source

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.

Instances For

source

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

source

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

source

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

source

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

source

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₂

source

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)

source

@[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)) (_ : Set.PairwiseDisjoint ↑s fun i => Finset.map (Function.Embedding.sigmaMk i) (t i)) = Finset.sigma s t

source

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)

source

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 => f { fst := i, snd := b }

source

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 => f { fst := i, snd := b }

source

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).

Instances For

source

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 hb, x.snd ∈ f x.fst (ha ▸ a.snd) (hb ▸ b.snd)

source

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 i a b

source

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

source

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

source

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.Nonempty (Finset.sigmaLift f a b) ↔ ∃ h, Finset.Nonempty (f b.fst (h ▸ a.snd) b.snd)

source

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 b.fst (h ▸ a.snd) b.snd = ∅

source

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 i a b ⊆ g i a b) (a : (i : ι) × α i) (b : (i : ι) × β i) :

Finset.sigmaLift f a b ⊆ Finset.sigmaLift g a b

source

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.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