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.sigma_lift: Lifts mapsα i → β i → finset (γ i)to a mapΣ i, α i → Σ i, β i → finset (Σ i, γ i).
TODO #
finset.sigma_lift 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.sigma_eq_bUnion
{ι : Type u_1}
{α : ι → Type u_2}
[decidable_eq (Σ (i : ι), α i)]
(s : finset ι)
(t : Π (i : ι), finset (α i)) :
s.sigma t = s.bUnion (λ (i : ι), finset.map (function.embedding.sigma_mk i) (t i))
def
finset.sigma_lift
{ι : Type u_1}
{α : ι → Type u_2}
{β : ι → Type u_3}
{γ : ι → Type u_4}
[decidable_eq ι]
(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).
theorem
finset.mem_sigma_lift
{ι : Type u_1}
{α : ι → Type u_2}
{β : ι → Type u_3}
{γ : ι → Type u_4}
[decidable_eq ι]
(f : Π ⦃i : ι⦄, α i → β i → finset (γ i))
(a : sigma α)
(b : sigma β)
(x : sigma γ) :
theorem
finset.mk_mem_sigma_lift
{ι : Type u_1}
{α : ι → Type u_2}
{β : ι → Type u_3}
{γ : ι → Type u_4}
[decidable_eq ι]
(f : Π ⦃i : ι⦄, α i → β i → finset (γ i))
(i : ι)
(a : α i)
(b : β i)
(x : γ i) :
theorem
finset.not_mem_sigma_lift_of_ne_left
{ι : Type u_1}
{α : ι → Type u_2}
{β : ι → Type u_3}
{γ : ι → Type u_4}
[decidable_eq ι]
(f : Π ⦃i : ι⦄, α i → β i → finset (γ i))
(a : sigma α)
(b : sigma β)
(x : sigma γ)
(h : a.fst ≠ x.fst) :
x ∉ finset.sigma_lift f a b
theorem
finset.not_mem_sigma_lift_of_ne_right
{ι : Type u_1}
{α : ι → Type u_2}
{β : ι → Type u_3}
{γ : ι → Type u_4}
[decidable_eq ι]
(f : Π ⦃i : ι⦄, α i → β i → finset (γ i))
{a : sigma α}
(b : sigma β)
{x : sigma γ}
(h : b.fst ≠ x.fst) :
x ∉ finset.sigma_lift f a b
theorem
finset.sigma_lift_nonempty
{ι : Type u_1}
{α : ι → Type u_2}
{β : ι → Type u_3}
{γ : ι → Type u_4}
[decidable_eq ι]
{f : Π ⦃i : ι⦄, α i → β i → finset (γ i)}
{a : Σ (i : ι), α i}
{b : Σ (i : ι), β i} :
theorem
finset.sigma_lift_eq_empty
{ι : Type u_1}
{α : ι → Type u_2}
{β : ι → Type u_3}
{γ : ι → Type u_4}
[decidable_eq ι]
{f : Π ⦃i : ι⦄, α i → β i → finset (γ i)}
{a : Σ (i : ι), α i}
{b : Σ (i : ι), β i} :
theorem
finset.sigma_lift_mono
{ι : Type u_1}
{α : ι → Type u_2}
{β : ι → Type u_3}
{γ : ι → Type u_4}
[decidable_eq ι]
{f 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.sigma_lift f a b ⊆ finset.sigma_lift g a b
theorem
finset.card_sigma_lift
{ι : Type u_1}
{α : ι → Type u_2}
{β : ι → Type u_3}
{γ : ι → Type u_4}
[decidable_eq ι]
(f : Π ⦃i : ι⦄, α i → β i → finset (γ i))
(a : Σ (i : ι), α i)
(b : Σ (i : ι), β i) :