Finite sets in a sigma type #
This file defines a few Finset constructions on Σ i, α i.
Main declarations #
Finset.sigma: Given a finsetsinιand finsetst iin eachα i,s.sigma tis the finset of the dependent sumΣ i, α iFinset.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.
theorem
Finset.Aesop.sigma_nonempty_of_exists_nonempty
{ι : Type u_1}
{α : ι → Type u_2}
{s : Finset ι}
{t : (i : ι) → Finset (α i)}
:
(∃ i ∈ s, (t i).Nonempty) → (s.sigma t).Nonempty
Alias of the reverse direction of Finset.sigma_nonempty.
theorem
Finset.pairwiseDisjoint_map_sigmaMk
{ι : Type u_1}
{α : ι → Type u_2}
{s : Finset ι}
{t : (i : ι) → Finset (α i)}
:
(↑s).PairwiseDisjoint 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)}
:
s.disjiUnion (fun (i : ι) => Finset.map (Function.Embedding.sigmaMk i) (t i)) ⋯ = s.sigma t
theorem
Finset.sigma_eq_biUnion
{ι : Type u_1}
{α : ι → Type u_2}
[DecidableEq ((i : ι) × α i)]
(s : Finset ι)
(t : (i : ι) → Finset (α i))
:
s.sigma t = s.biUnion 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 β]
:
(s.sigma t).sup f = s.sup fun (i : ι) => (t i).sup fun (b : α i) => f ⟨i, 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 β]
:
(s.sigma t).inf f = s.inf fun (i : ι) => (t i).inf fun (b : α i) => f ⟨i, b⟩
theorem
biSup_finsetSigma
{ι : Type u_1}
{α : ι → Type u_2}
{β : Type u_3}
[CompleteLattice β]
(s : Finset ι)
(t : (i : ι) → Finset (α i))
(f : Sigma α → β)
:
⨆ ij ∈ s.sigma t, f ij = ⨆ i ∈ s, ⨆ j ∈ t i, f ⟨i, 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 ∈ s.sigma 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 ∈ s.sigma t, f ij = ⨅ i ∈ s, ⨅ j ∈ t i, f ⟨i, 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 ∈ s.sigma 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 β)
:
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 ∅
Instances For
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 γ)
:
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)
:
⟨i, x⟩ ∈ Finset.sigmaLift f ⟨i, a⟩ ⟨i, 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}
:
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