Finite sets in a sigma type #
This file defines a few Finset
constructions on Σ i, α i
.
Main declarations #
Finset.sigma
: Given a finsets
inι
and finsetst 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.
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)) }
@[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.Nonempty (Finset.sigma s t) ↔ ∃ i, i ∈ s ∧ Finset.Nonempty (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.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
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)
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 → β i → Finset (γ 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
- 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 ∅
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
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)
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}
:
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
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