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 : Finset α) (t : Finset β) : 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 := ⋯ }

@[implicit_reducible]

instance Finset.instSProd {α : Type u_1} {β : Type u_2} : SProd (Finset α) (Finset β) (Finset (α × β))

Equations

• Finset.instSProd = { sprod := Finset.product }

@[simp]

theorem Finset.product_eq_sprod {α : Type u_1} {β : Type u_2} {s : Finset α} {t : Finset β} : s.product t = s ×ˢ t

@[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.1 ∈ s ∧ p.2 ∈ 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 β} [DecidableEq α] : image Prod.fst (s ×ˢ t) ⊆ s

theorem Finset.subset_product_image_snd {α : Type u_1} {β : Type u_2} {s : Finset α} {t : Finset β} [DecidableEq β] : image Prod.snd (s ×ˢ t) ⊆ t

theorem Finset.product_image_fst {α : Type u_1} {β : Type u_2} {s : Finset α} {t : Finset β} [DecidableEq α] (ht : t.Nonempty) : image Prod.fst (s ×ˢ t) = s

theorem Finset.product_image_snd {α : Type u_1} {β : Type u_2} {s : Finset α} {t : Finset β} [DecidableEq β] (ht : s.Nonempty) : image Prod.snd (s ×ˢ t) = t

theorem Finset.subset_product {α : Type u_1} {β : Type u_2} [DecidableEq α] [DecidableEq β] {s : Finset (α × β)} : s ⊆ image Prod.fst s ×ˢ image Prod.snd s

theorem Finset.product_subset_product {α : Type u_1} {β : Type u_2} {s s' : Finset α} {t 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 s' : Finset α} {t : Finset β} (hs : s ⊆ s') : s ×ˢ t ⊆ s' ×ˢ t

theorem Finset.product_subset_product_right {α : Type u_1} {β : Type u_2} {s : Finset α} {t t' : Finset β} (ht : t ⊆ t') : s ×ˢ t ⊆ s ×ˢ t'

theorem Finset.prodMap_image_product {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} [DecidableEq β] [DecidableEq δ] (f : α → β) (g : γ → δ) (s : Finset α) (t : Finset γ) : image (Prod.map f g) (s ×ˢ t) = image f s ×ˢ image g t

theorem Finset.prodMap_map_product {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} (f : α ↪ β) (g : γ ↪ δ) (s : Finset α) (t : Finset γ) : map (f.prodMap g) (s ×ˢ t) = map f s ×ˢ map g t

theorem Finset.map_swap_product {α : Type u_1} {β : Type u_2} (s : Finset α) (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 : Finset α) (t : Finset β) : image Prod.swap (t ×ˢ s) = s ×ˢ t

theorem Finset.product_eq_biUnion {α : Type u_1} {β : Type u_2} [DecidableEq (α × β)] (s : Finset α) (t : Finset β) : s ×ˢ t = s.biUnion fun (a : α) => image (fun (b : β) => (a, b)) t

theorem Finset.product_eq_biUnion_right {α : Type u_1} {β : Type u_2} [DecidableEq (α × β)] (s : Finset α) (t : Finset β) : s ×ˢ t = t.biUnion fun (b : β) => image (fun (a : α) => (a, b)) s

@[simp]

theorem Finset.product_biUnion {α : Type u_1} {β : Type u_2} {γ : Type u_3} [DecidableEq γ] (s : Finset α) (t : Finset β) (f : α × β → Finset γ) : (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 : Finset α) (t : Finset β) : (s ×ˢ t).card = s.card * t.card

theorem Finset.nontrivial_prod_iff {α : Type u_1} {β : Type u_2} {s : Finset α} {t : Finset β} : (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 : Finset α} {t : Finset β} (p : α → Prop) (q : β → Prop) [DecidablePred p] [DecidablePred q] : {x ∈ s ×ˢ t | p x.1 ∧ q x.2} = filter p s ×ˢ filter q t

theorem Finset.filter_product_left {α : Type u_1} {β : Type u_2} {s : Finset α} {t : Finset β} (p : α → Prop) [DecidablePred p] : {x ∈ s ×ˢ t | p x.1} = filter p s ×ˢ t

theorem Finset.filter_product_right {α : Type u_1} {β : Type u_2} {s : Finset α} {t : Finset β} (q : β → Prop) [DecidablePred q] : {x ∈ s ×ˢ t | q x.2} = s ×ˢ filter q t

theorem Finset.filter_product_card {α : Type u_1} {β : Type u_2} (s : Finset α) (t : Finset β) (p : α → Prop) (q : β → Prop) [DecidablePred p] [DecidablePred q] : {x ∈ s ×ˢ t | p x.1 = q x.2}.card = (filter p s).card * (filter q t).card + {x ∈ s | ¬p x}.card * {x ∈ t | ¬q x}.card

@[simp]

theorem Finset.empty_product {α : Type u_1} {β : Type u_2} (t : Finset β) : ∅ ×ˢ t = ∅

@[simp]

theorem Finset.product_empty {α : Type u_1} {β : Type u_2} (s : Finset α) : s ×ˢ ∅ = ∅

theorem Finset.Nonempty.product {α : Type u_1} {β : Type u_2} {s : Finset α} {t : Finset β} (hs : s.Nonempty) (ht : t.Nonempty) : (s ×ˢ t).Nonempty

theorem Finset.Nonempty.fst {α : Type u_1} {β : Type u_2} {s : Finset α} {t : Finset β} (h : (s ×ˢ t).Nonempty) : s.Nonempty

theorem Finset.Nonempty.snd {α : Type u_1} {β : Type u_2} {s : Finset α} {t : Finset β} (h : (s ×ˢ t).Nonempty) : t.Nonempty

@[simp]

theorem Finset.nonempty_product {α : Type u_1} {β : Type u_2} {s : Finset α} {t : Finset β} : (s ×ˢ t).Nonempty ↔ s.Nonempty ∧ t.Nonempty

@[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 = map { toFun := Prod.mk a, inj' := ⋯ } t

@[simp]

theorem Finset.product_singleton {α : Type u_1} {β : Type u_2} {s : Finset α} {b : β} : s ×ˢ {b} = 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' : Finset α} {t : Finset β} [DecidableEq α] [DecidableEq β] : (s ∪ s') ×ˢ t = s ×ˢ t ∪ s' ×ˢ t

@[simp]

theorem Finset.product_union {α : Type u_1} {β : Type u_2} {s : Finset α} {t t' : Finset β} [DecidableEq α] [DecidableEq β] : s ×ˢ (t ∪ t') = s ×ˢ t ∪ s ×ˢ t'

theorem Finset.inter_product {α : Type u_1} {β : Type u_2} {s s' : Finset α} {t : Finset β} [DecidableEq α] [DecidableEq β] : (s ∩ s') ×ˢ t = s ×ˢ t ∩ s' ×ˢ t

theorem Finset.product_inter {α : Type u_1} {β : Type u_2} {s : Finset α} {t t' : Finset β} [DecidableEq α] [DecidableEq β] : s ×ˢ (t ∩ t') = s ×ˢ t ∩ s ×ˢ t'

theorem Finset.product_inter_product {α : Type u_1} {β : Type u_2} {s s' : Finset α} {t t' : Finset β} [DecidableEq α] [DecidableEq β] : s ×ˢ t ∩ s' ×ˢ t' = (s ∩ s') ×ˢ (t ∩ t')

theorem Finset.disjoint_product {α : Type u_1} {β : Type u_2} {s s' : Finset α} {t 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 s' : Finset α} {t : Finset β} (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 : Finset α} {t t' : Finset β} (ht : Disjoint t t') : s ×ˢ t.disjUnion t' ht = (s ×ˢ t).disjUnion (s ×ˢ t') ⋯

def Finset.diag {α : Type u_1} (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.

Equations

• s.diag = Finset.map { toFun := fun (a : α) => (a, a), inj' := ⋯ } s

def Finset.offDiag {α : Type u_1} (s : Finset α) : 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

• s.offDiag = { val := Quotient.map List.offDiag ⋯ s.val, nodup := ⋯ }

@[simp]

theorem Finset.mem_diag {α : Type u_1} {s : Finset α} {x : α × α} : x ∈ s.diag ↔ x.1 ∈ s ∧ x.1 = x.2

@[simp]

theorem Finset.mem_offDiag {α : Type u_1} {s : Finset α} {x : α × α} : x ∈ s.offDiag ↔ x.1 ∈ s ∧ x.2 ∈ s ∧ x.1 ≠ x.2

@[simp]

theorem Finset.diag_nonempty {α : Type u_1} {s : Finset α} : s.diag.Nonempty ↔ s.Nonempty

@[simp]

theorem Finset.diag_eq_empty {α : Type u_1} {s : Finset α} : s.diag = ∅ ↔ s = ∅

theorem Finset.diag_eq_filter {α : Type u_1} {s : Finset α} [DecidableEq α] : s.diag = {a ∈ s ×ˢ s | a.1 = a.2}

@[simp]

theorem Finset.image_diag {α : Type u_1} {β : Type u_2} [DecidableEq β] (f : α × α → β) (s : Finset α) : image f s.diag = image (fun (x : α) => f (x, x)) s

@[simp]

theorem Finset.coe_offDiag {α : Type u_1} (s : Finset α) : ↑s.offDiag = (↑s).offDiag

@[simp]

theorem Finset.diag_card {α : Type u_1} (s : Finset α) : s.diag.card = s.card

@[simp]

theorem Finset.offDiag_card {α : Type u_1} (s : Finset α) : s.offDiag.card = s.card * s.card - s.card

theorem Finset.diag_mono {α : Type u_1} : Monotone diag

theorem Finset.offDiag_mono {α : Type u_1} : Monotone 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 : Finset α) [DecidableEq α] : s.diag ∪ s.offDiag = s ×ˢ s

@[simp]

theorem Finset.disjoint_diag_offDiag {α : Type u_1} (s : Finset α) : Disjoint s.diag s.offDiag

theorem Finset.product_sdiff_diag {α : Type u_1} (s : Finset α) [DecidableEq α] : s ×ˢ s \ s.diag = s.offDiag

theorem Finset.product_sdiff_offDiag {α : Type u_1} (s : Finset α) [DecidableEq α] : s ×ˢ s \ s.offDiag = s.diag

theorem Finset.diag_inter {α : Type u_1} (s t : Finset α) [DecidableEq α] : (s ∩ t).diag = s.diag ∩ t.diag

theorem Finset.offDiag_inter {α : Type u_1} (s t : Finset α) [DecidableEq α] : (s ∩ t).offDiag = s.offDiag ∩ t.offDiag

theorem Finset.diag_union {α : Type u_1} (s t : Finset α) [DecidableEq α] : (s ∪ t).diag = s.diag ∪ t.diag

theorem Finset.offDiag_union {α : Type u_1} {s t : Finset α} [DecidableEq α] (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 : Finset α} [DecidableEq α] (a : α) : (insert a s).diag = insert (a, a) s.diag

theorem Finset.offDiag_insert {α : Type u_1} {s : Finset α} [DecidableEq α] {a : α} (has : a ∉ s) : (insert a s).offDiag = s.offDiag ∪ {a} ×ˢ s ∪ s ×ˢ {a}

theorem Finset.offDiag_filter_lt_eq_filter_le {ι : Type u_4} [PartialOrder ι] [DecidableLE ι] [DecidableLT ι] (s : Finset ι) : {i ∈ s.offDiag | i.1 < i.2} = {i ∈ s.offDiag | i.1 ≤ i.2}