Documentation

Mathlib.Data.Finset.Prod

Finsets in product types #

This file defines finset constructions on the product type α × β× β. Beware not to confuse with the Finset.prod operation which computes the multiplicative product.

Main declarations #

prod #

def Finset.product {α : Type u_1} {β : Type u_2} (s : Finset α) (t : Finset β) :
Finset (α × β)

product s t is the set of pairs (a, b) such that a ∈ s∈ s and b ∈ t∈ t.

Equations

product s t is the set of pairs (a, b) such that a ∈ s∈ s and b ∈ t∈ t.

Equations
@[simp]
theorem Finset.product_val {α : Type u_1} {β : Type u_2} {s : Finset α} {t : Finset β} :
(s ×ᶠ t).val = s.val ×ˢ t.val
@[simp]
theorem Finset.mem_product {α : Type u_1} {β : Type u_2} {s : Finset α} {t : Finset β} {p : α × β} :
p s ×ᶠ t p.fst s p.snd t
theorem Finset.mk_mem_product {α : Type u_1} {β : Type u_2} {s : Finset α} {t : Finset β} {a : α} {b : β} (ha : a s) (hb : b t) :
(a, b) s ×ᶠ t
@[simp]
theorem Finset.coe_product {α : Type u_1} {β : Type u_2} (s : Finset α) (t : Finset β) :
↑(s ×ᶠ t) = s ×ˢ t
theorem Finset.subset_product_image_fst {α : Type u_1} {β : Type u_2} {s : Finset α} {t : Finset β} [inst : DecidableEq α] :
Finset.image Prod.fst (s ×ᶠ t) s
theorem Finset.subset_product_image_snd {α : Type u_2} {β : Type u_1} {s : Finset α} {t : Finset β} [inst : DecidableEq β] :
Finset.image Prod.snd (s ×ᶠ t) t
theorem Finset.product_image_fst {α : Type u_1} {β : Type u_2} {s : Finset α} {t : Finset β} [inst : DecidableEq α] (ht : Finset.Nonempty t) :
Finset.image Prod.fst (s ×ᶠ t) = s
theorem Finset.product_image_snd {α : Type u_2} {β : Type u_1} {s : Finset α} {t : Finset β} [inst : DecidableEq β] (ht : Finset.Nonempty s) :
Finset.image Prod.snd (s ×ᶠ t) = t
theorem Finset.subset_product {α : Type u_1} {β : Type u_2} [inst : DecidableEq α] [inst : DecidableEq β] {s : Finset (α × β)} :
s Finset.image Prod.fst s ×ᶠ Finset.image Prod.snd s
theorem Finset.product_subset_product {α : Type u_1} {β : Type u_2} {s : Finset α} {s' : Finset α} {t : Finset β} {t' : Finset β} (hs : s s') (ht : t t') :
s ×ᶠ t s' ×ᶠ t'
theorem Finset.product_subset_product_left {α : Type u_1} {β : Type u_2} {s : Finset α} {s' : Finset α} {t : Finset β} (hs : s s') :
s ×ᶠ t s' ×ᶠ t
theorem Finset.product_subset_product_right {α : Type u_2} {β : Type u_1} {s : Finset α} {t : Finset β} {t' : Finset β} (ht : t t') :
s ×ᶠ t s ×ᶠ t'
theorem Finset.map_swap_product {α : Type u_1} {β : Type u_2} (s : Finset α) (t : Finset β) :
Finset.map { toFun := Prod.swap, inj' := (_ : Function.Injective Prod.swap) } (t ×ᶠ s) = s ×ᶠ t
@[simp]
theorem Finset.image_swap_product {α : Type u_2} {β : Type u_1} [inst : DecidableEq (α × β)] (s : Finset α) (t : Finset β) :
Finset.image Prod.swap (t ×ᶠ s) = s ×ᶠ t
theorem Finset.product_eq_bunionᵢ {α : Type u_2} {β : Type u_1} [inst : DecidableEq (α × β)] (s : Finset α) (t : Finset β) :
s ×ᶠ t = Finset.bunionᵢ s fun a => Finset.image (fun b => (a, b)) t
theorem Finset.product_eq_bunionᵢ_right {α : Type u_2} {β : Type u_1} [inst : DecidableEq (α × β)] (s : Finset α) (t : Finset β) :
s ×ᶠ t = Finset.bunionᵢ t fun b => Finset.image (fun a => (a, b)) s
@[simp]
theorem Finset.product_bunionᵢ {α : Type u_2} {β : Type u_3} {γ : Type u_1} [inst : DecidableEq γ] (s : Finset α) (t : Finset β) (f : α × βFinset γ) :
Finset.bunionᵢ (s ×ᶠ t) f = Finset.bunionᵢ s fun a => Finset.bunionᵢ t fun b => f (a, b)

See also Finset.sup_product_left.

@[simp]
theorem Finset.card_product {α : Type u_1} {β : Type u_2} (s : Finset α) (t : Finset β) :
theorem Finset.filter_product {α : Type u_1} {β : Type u_2} {s : Finset α} {t : Finset β} (p : αProp) (q : βProp) [inst : DecidablePred p] [inst : DecidablePred q] :
Finset.filter (fun x => p x.fst q x.snd) (s ×ᶠ t) = Finset.filter p s ×ᶠ Finset.filter q t
theorem Finset.filter_product_left {α : Type u_1} {β : Type u_2} {s : Finset α} {t : Finset β} (p : αProp) [inst : DecidablePred p] :
Finset.filter (fun x => p x.fst) (s ×ᶠ t) = Finset.filter p s ×ᶠ t
theorem Finset.filter_product_right {α : Type u_2} {β : Type u_1} {s : Finset α} {t : Finset β} (q : βProp) [inst : DecidablePred q] :
Finset.filter (fun x => q x.snd) (s ×ᶠ t) = s ×ᶠ Finset.filter q t
theorem Finset.filter_product_card {α : Type u_1} {β : Type u_2} (s : Finset α) (t : Finset β) (p : αProp) (q : βProp) [inst : DecidablePred p] [inst : DecidablePred q] :
Finset.card (Finset.filter (fun x => p x.fst = q x.snd) (s ×ᶠ t)) = Finset.card (Finset.filter p s) * Finset.card (Finset.filter q t) + Finset.card (Finset.filter (fun x => ¬p x) s) * Finset.card (Finset.filter (fun x => ¬q x) t)
theorem Finset.empty_product {α : Type u_2} {β : Type u_1} (t : Finset β) :
theorem Finset.product_empty {α : Type u_1} {β : Type u_2} (s : Finset α) :
theorem Finset.Nonempty.product {α : Type u_1} {β : Type u_2} {s : Finset α} {t : Finset β} (hs : Finset.Nonempty s) (ht : Finset.Nonempty t) :
theorem Finset.Nonempty.fst {α : Type u_1} {β : Type u_2} {s : Finset α} {t : Finset β} (h : Finset.Nonempty (s ×ᶠ t)) :
theorem Finset.Nonempty.snd {α : Type u_1} {β : Type u_2} {s : Finset α} {t : Finset β} (h : Finset.Nonempty (s ×ᶠ t)) :
@[simp]
theorem Finset.nonempty_product {α : Type u_1} {β : Type u_2} {s : Finset α} {t : Finset β} :
@[simp]
theorem Finset.product_eq_empty {α : Type u_1} {β : Type u_2} {s : Finset α} {t : Finset β} :
s ×ᶠ t = s = t =
@[simp]
theorem Finset.singleton_product {α : Type u_1} {β : Type u_2} {t : Finset β} {a : α} :
{a} ×ᶠ t = Finset.map { toFun := Prod.mk a, inj' := (_ : Function.Injective (Prod.mk a)) } t
@[simp]
theorem Finset.product_singleton {α : Type u_1} {β : Type u_2} {s : Finset α} {b : β} :
s ×ᶠ {b} = Finset.map { toFun := fun i => (i, b), inj' := (_ : Function.Injective fun a => (a, b)) } s
theorem Finset.singleton_product_singleton {α : Type u_1} {β : Type u_2} {a : α} {b : β} :
{a} ×ᶠ {b} = {(a, b)}
@[simp]
theorem Finset.union_product {α : Type u_1} {β : Type u_2} {s : Finset α} {s' : Finset α} {t : Finset β} [inst : DecidableEq α] [inst : DecidableEq β] :
(s s') ×ᶠ t = s ×ᶠ t s' ×ᶠ t
@[simp]
theorem Finset.product_union {α : Type u_1} {β : Type u_2} {s : Finset α} {t : Finset β} {t' : Finset β} [inst : DecidableEq α] [inst : DecidableEq β] :
s ×ᶠ (t t') = s ×ᶠ t s ×ᶠ t'
theorem Finset.inter_product {α : Type u_1} {β : Type u_2} {s : Finset α} {s' : Finset α} {t : Finset β} [inst : DecidableEq α] [inst : DecidableEq β] :
(s s') ×ᶠ t = s ×ᶠ t s' ×ᶠ t
theorem Finset.product_inter {α : Type u_1} {β : Type u_2} {s : Finset α} {t : Finset β} {t' : Finset β} [inst : DecidableEq α] [inst : DecidableEq β] :
s ×ᶠ (t t') = s ×ᶠ t s ×ᶠ t'
theorem Finset.product_inter_product {α : Type u_1} {β : Type u_2} {s : Finset α} {s' : Finset α} {t : Finset β} {t' : Finset β} [inst : DecidableEq α] [inst : DecidableEq β] :
s ×ᶠ t s' ×ᶠ t' = (s s') ×ᶠ (t t')
theorem Finset.disjoint_product {α : Type u_2} {β : Type u_1} {s : Finset α} {s' : Finset α} {t : Finset β} {t' : Finset β} :
Disjoint (s ×ᶠ t) (s' ×ᶠ t') Disjoint s s' Disjoint t t'
@[simp]
theorem Finset.disjUnion_product {α : Type u_1} {β : Type u_2} {s : Finset α} {s' : Finset α} {t : Finset β} (hs : Disjoint s s') :
Finset.disjUnion s s' hs ×ᶠ t = Finset.disjUnion (s ×ᶠ t) (s' ×ᶠ t) (_ : Disjoint (s ×ᶠ t) (s' ×ᶠ t))
@[simp]
theorem Finset.product_disjUnion {α : Type u_2} {β : Type u_1} {s : Finset α} {t : Finset β} {t' : Finset β} (ht : Disjoint t t') :
s ×ᶠ Finset.disjUnion t t' ht = Finset.disjUnion (s ×ᶠ t) (s ×ᶠ t') (_ : Disjoint (s ×ᶠ t) (s ×ᶠ t'))
def Finset.diag {α : Type u_1} [inst : DecidableEq α] (s : Finset α) :
Finset (α × α)

Given a finite set s, the diagonal, s.diag is the set of pairs of the form (a, a) for a ∈ s∈ s.

Equations
def Finset.offDiag {α : Type u_1} [inst : DecidableEq α] (s : Finset α) :
Finset (α × α)

Given a finite set s, the off-diagonal, s.offDiag is the set of pairs (a, b) with a ≠ b≠ b for a, b ∈ s∈ s.

Equations
@[simp]
theorem Finset.mem_diag {α : Type u_1} [inst : DecidableEq α] {s : Finset α} {x : α × α} :
x Finset.diag s x.fst s x.fst = x.snd
@[simp]
theorem Finset.mem_offDiag {α : Type u_1} [inst : DecidableEq α] {s : Finset α} {x : α × α} :
x Finset.offDiag s x.fst s x.snd s x.fst x.snd
@[simp]
theorem Finset.coe_offDiag {α : Type u_1} [inst : DecidableEq α] (s : Finset α) :
@[simp]
theorem Finset.diag_card {α : Type u_1} [inst : DecidableEq α] (s : Finset α) :
theorem Finset.diag_mono {α : Type u_1} [inst : DecidableEq α] :
Monotone Finset.diag
theorem Finset.offDiag_mono {α : Type u_1} [inst : DecidableEq α] :
Monotone Finset.offDiag
@[simp]
theorem Finset.diag_empty {α : Type u_1} [inst : DecidableEq α] :
@[simp]
theorem Finset.offDiag_empty {α : Type u_1} [inst : DecidableEq α] :
@[simp]
theorem Finset.diag_union_offDiag {α : Type u_1} [inst : DecidableEq α] (s : Finset α) :
@[simp]
theorem Finset.disjoint_diag_offDiag {α : Type u_1} [inst : DecidableEq α] (s : Finset α) :
theorem Finset.diag_inter {α : Type u_1} [inst : DecidableEq α] (s : Finset α) (t : Finset α) :
theorem Finset.offDiag_inter {α : Type u_1} [inst : DecidableEq α] (s : Finset α) (t : Finset α) :
theorem Finset.diag_union {α : Type u_1} [inst : DecidableEq α] (s : Finset α) (t : Finset α) :
theorem Finset.offDiag_union {α : Type u_1} [inst : DecidableEq α] {s : Finset α} {t : Finset α} (h : Disjoint s t) :
@[simp]
theorem Finset.offDiag_singleton {α : Type u_1} [inst : DecidableEq α] (a : α) :
theorem Finset.diag_singleton {α : Type u_1} [inst : DecidableEq α] (a : α) :
Finset.diag {a} = {(a, a)}
theorem Finset.diag_insert {α : Type u_1} [inst : DecidableEq α] {s : Finset α} (a : α) :
theorem Finset.offDiag_insert {α : Type u_1} [inst : DecidableEq α] {s : Finset α} (a : α) (has : ¬a s) :