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

• Finset.product: Turns s : Finset α, t : Finset β into their product in Finset (α × β).
• Finset.diag: For s : Finset α, s.diag is the Finset (α × α) of pairs (a, a) with a ∈ s.
• Finset.offDiag: For s : Finset α, s.offDiag is the Finset (α × α) of pairs (a, b) with a, b ∈ s and a ≠ b.

### prod #

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

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

Equations
• s.product t = { val := s.val ×ˢ t.val, nodup := }
Instances For
instance Finset.instSProd {α : Type u_1} {β : Type u_2} :
SProd () () (Finset (α × β))
Equations
• Finset.instSProd = { sprod := Finset.product }
@[simp]
theorem Finset.product_val {α : Type u_1} {β : Type u_2} {s : } {t : } :
(s ×ˢ t).val = s.val ×ˢ t.val
@[simp]
theorem Finset.mem_product {α : Type u_1} {β : Type u_2} {s : } {t : } {p : α × β} :
p s ×ˢ t p.1 s p.2 t
theorem Finset.mk_mem_product {α : Type u_1} {β : Type u_2} {s : } {t : } {a : α} {b : β} (ha : a s) (hb : b t) :
(a, b) s ×ˢ t
@[simp]
theorem Finset.coe_product {α : Type u_1} {β : Type u_2} (s : ) (t : ) :
(s ×ˢ t) = s ×ˢ t
theorem Finset.subset_product_image_fst {α : Type u_1} {β : Type u_2} {s : } {t : } [] :
Finset.image Prod.fst (s ×ˢ t) s
theorem Finset.subset_product_image_snd {α : Type u_1} {β : Type u_2} {s : } {t : } [] :
Finset.image Prod.snd (s ×ˢ t) t
theorem Finset.product_image_fst {α : Type u_1} {β : Type u_2} {s : } {t : } [] (ht : t.Nonempty) :
Finset.image Prod.fst (s ×ˢ t) = s
theorem Finset.product_image_snd {α : Type u_1} {β : Type u_2} {s : } {t : } [] (ht : s.Nonempty) :
Finset.image Prod.snd (s ×ˢ t) = t
theorem Finset.subset_product {α : Type u_1} {β : Type u_2} [] [] {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 : } {s' : } {t : } {t' : } (hs : s s') (ht : t t') :
s ×ˢ t s' ×ˢ t'
theorem Finset.product_subset_product_left {α : Type u_1} {β : Type u_2} {s : } {s' : } {t : } (hs : s s') :
s ×ˢ t s' ×ˢ t
theorem Finset.product_subset_product_right {α : Type u_1} {β : Type u_2} {s : } {t : } {t' : } (ht : t t') :
s ×ˢ t s ×ˢ t'
theorem Finset.map_swap_product {α : Type u_1} {β : Type u_2} (s : ) (t : ) :
Finset.map { toFun := Prod.swap, inj' := } (t ×ˢ s) = s ×ˢ t
@[simp]
theorem Finset.image_swap_product {α : Type u_1} {β : Type u_2} [DecidableEq (α × β)] (s : ) (t : ) :
Finset.image Prod.swap (t ×ˢ s) = s ×ˢ t
theorem Finset.product_eq_biUnion {α : Type u_1} {β : Type u_2} [DecidableEq (α × β)] (s : ) (t : ) :
s ×ˢ t = s.biUnion fun (a : α) => Finset.image (fun (b : β) => (a, b)) t
theorem Finset.product_eq_biUnion_right {α : Type u_1} {β : Type u_2} [DecidableEq (α × β)] (s : ) (t : ) :
s ×ˢ t = t.biUnion fun (b : β) => Finset.image (fun (a : α) => (a, b)) s
@[simp]
theorem Finset.product_biUnion {α : Type u_1} {β : Type u_2} {γ : Type u_3} [] (s : ) (t : ) (f : α × β) :
(s ×ˢ t).biUnion f = s.biUnion fun (a : α) => t.biUnion fun (b : β) => f (a, b)

See also Finset.sup_product_left.

@[simp]
theorem Finset.card_product {α : Type u_1} {β : Type u_2} (s : ) (t : ) :
(s ×ˢ t).card = s.card * t.card
theorem Finset.nontrivial_prod_iff {α : Type u_1} {β : Type u_2} {s : } {t : } :
(s ×ˢ t).Nontrivial s.Nonempty t.Nonempty (s.Nontrivial t.Nontrivial)

The product of two Finsets is nontrivial iff both are nonempty at least one of them is nontrivial.

theorem Finset.filter_product {α : Type u_1} {β : Type u_2} {s : } {t : } (p : αProp) (q : βProp) [] [] :
Finset.filter (fun (x : α × β) => p x.1 q x.2) (s ×ˢ t) = ×ˢ
theorem Finset.filter_product_left {α : Type u_1} {β : Type u_2} {s : } {t : } (p : αProp) [] :
Finset.filter (fun (x : α × β) => p x.1) (s ×ˢ t) = ×ˢ t
theorem Finset.filter_product_right {α : Type u_1} {β : Type u_2} {s : } {t : } (q : βProp) [] :
Finset.filter (fun (x : α × β) => q x.2) (s ×ˢ t) = s ×ˢ
theorem Finset.filter_product_card {α : Type u_1} {β : Type u_2} (s : ) (t : ) (p : αProp) (q : βProp) [] [] :
(Finset.filter (fun (x : α × β) => p x.1 = q x.2) (s ×ˢ t)).card = ().card * ().card + (Finset.filter (fun (x : α) => ¬p x) s).card * (Finset.filter (fun (x : β) => ¬q x) t).card
@[simp]
theorem Finset.empty_product {α : Type u_1} {β : Type u_2} (t : ) :
@[simp]
theorem Finset.product_empty {α : Type u_1} {β : Type u_2} (s : ) :
theorem Finset.Nonempty.product {α : Type u_1} {β : Type u_2} {s : } {t : } (hs : s.Nonempty) (ht : t.Nonempty) :
(s ×ˢ t).Nonempty
theorem Finset.Nonempty.fst {α : Type u_1} {β : Type u_2} {s : } {t : } (h : (s ×ˢ t).Nonempty) :
s.Nonempty
theorem Finset.Nonempty.snd {α : Type u_1} {β : Type u_2} {s : } {t : } (h : (s ×ˢ t).Nonempty) :
t.Nonempty
@[simp]
theorem Finset.nonempty_product {α : Type u_1} {β : Type u_2} {s : } {t : } :
(s ×ˢ t).Nonempty s.Nonempty t.Nonempty
@[simp]
theorem Finset.product_eq_empty {α : Type u_1} {β : Type u_2} {s : } {t : } :
s ×ˢ t = s = t =
@[simp]
theorem Finset.singleton_product {α : Type u_1} {β : Type u_2} {t : } {a : α} :
{a} ×ˢ t = Finset.map { toFun := , inj' := } t
@[simp]
theorem Finset.product_singleton {α : Type u_1} {β : Type u_2} {s : } {b : β} :
s ×ˢ {b} = Finset.map { toFun := fun (i : α) => (i, b), inj' := } 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 : } {s' : } {t : } [] [] :
(s s') ×ˢ t = s ×ˢ t s' ×ˢ t
@[simp]
theorem Finset.product_union {α : Type u_1} {β : Type u_2} {s : } {t : } {t' : } [] [] :
s ×ˢ (t t') = s ×ˢ t s ×ˢ t'
theorem Finset.inter_product {α : Type u_1} {β : Type u_2} {s : } {s' : } {t : } [] [] :
(s s') ×ˢ t = s ×ˢ t s' ×ˢ t
theorem Finset.product_inter {α : Type u_1} {β : Type u_2} {s : } {t : } {t' : } [] [] :
s ×ˢ (t t') = s ×ˢ t s ×ˢ t'
theorem Finset.product_inter_product {α : Type u_1} {β : Type u_2} {s : } {s' : } {t : } {t' : } [] [] :
s ×ˢ t s' ×ˢ t' = (s s') ×ˢ (t t')
theorem Finset.disjoint_product {α : Type u_1} {β : Type u_2} {s : } {s' : } {t : } {t' : } :
Disjoint (s ×ˢ t) (s' ×ˢ t') Disjoint s s' Disjoint t t'
@[simp]
theorem Finset.disjUnion_product {α : Type u_1} {β : Type u_2} {s : } {s' : } {t : } (hs : Disjoint s s') :
s.disjUnion s' hs ×ˢ t = (s ×ˢ t).disjUnion (s' ×ˢ t)
@[simp]
theorem Finset.product_disjUnion {α : Type u_1} {β : Type u_2} {s : } {t : } {t' : } (ht : Disjoint t t') :
s ×ˢ t.disjUnion t' ht = (s ×ˢ t).disjUnion (s ×ˢ t')
def Finset.diag {α : Type u_1} [] (s : ) :
Finset (α × α)

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

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

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

Equations
Instances For
@[simp]
theorem Finset.mem_diag {α : Type u_1} [] {s : } {x : α × α} :
x s.diag x.1 s x.1 = x.2
@[simp]
theorem Finset.mem_offDiag {α : Type u_1} [] {s : } {x : α × α} :
x s.offDiag x.1 s x.2 s x.1 x.2
@[simp]
theorem Finset.coe_offDiag {α : Type u_1} [] (s : ) :
s.offDiag = (s).offDiag
@[simp]
theorem Finset.diag_card {α : Type u_1} [] (s : ) :
s.diag.card = s.card
@[simp]
theorem Finset.offDiag_card {α : Type u_1} [] (s : ) :
s.offDiag.card = s.card * s.card - s.card
theorem Finset.diag_mono {α : Type u_1} [] :
Monotone Finset.diag
theorem Finset.offDiag_mono {α : Type u_1} [] :
Monotone Finset.offDiag
@[simp]
theorem Finset.diag_empty {α : Type u_1} [] :
.diag =
@[simp]
theorem Finset.offDiag_empty {α : Type u_1} [] :
.offDiag =
@[simp]
theorem Finset.diag_union_offDiag {α : Type u_1} [] (s : ) :
s.diag s.offDiag = s ×ˢ s
@[simp]
theorem Finset.disjoint_diag_offDiag {α : Type u_1} [] (s : ) :
Disjoint s.diag s.offDiag
theorem Finset.product_sdiff_diag {α : Type u_1} [] (s : ) :
s ×ˢ s \ s.diag = s.offDiag
theorem Finset.product_sdiff_offDiag {α : Type u_1} [] (s : ) :
s ×ˢ s \ s.offDiag = s.diag
theorem Finset.diag_inter {α : Type u_1} [] (s : ) (t : ) :
(s t).diag = s.diag t.diag
theorem Finset.offDiag_inter {α : Type u_1} [] (s : ) (t : ) :
(s t).offDiag = s.offDiag t.offDiag
theorem Finset.diag_union {α : Type u_1} [] (s : ) (t : ) :
(s t).diag = s.diag t.diag
theorem Finset.offDiag_union {α : Type u_1} [] {s : } {t : } (h : Disjoint s t) :
(s t).offDiag = s.offDiag t.offDiag s ×ˢ t t ×ˢ s
@[simp]
theorem Finset.offDiag_singleton {α : Type u_1} [] (a : α) :
{a}.offDiag =
theorem Finset.diag_singleton {α : Type u_1} [] (a : α) :
{a}.diag = {(a, a)}
theorem Finset.diag_insert {α : Type u_1} [] {s : } (a : α) :
(insert a s).diag = insert (a, a) s.diag
theorem Finset.offDiag_insert {α : Type u_1} [] {s : } (a : α) (has : as) :
(insert a s).offDiag = s.offDiag {a} ×ˢ s s ×ˢ {a}