mathlib3 documentation

data.finset.prod

Finsets in product types #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 #

source
@[protected]
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
source
@[simp]
theorem finset.product_val {α : Type u_1} {β : Type u_2} {s : finset α} {t : finset β} :
(s ×ˢ t).val = s.val ×ˢ t.val
source
@[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
source
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
source
@[simp, norm_cast]
theorem finset.coe_product {α : Type u_1} {β : Type u_2} (s : finset α) (t : finset β) :
↑(s ×ˢ t) = ↑s ×ˢ ↑t
source
theorem finset.subset_product_image_fst {α : Type u_1} {β : Type u_2} {s : finset α} {t : finset β} [decidable_eq α] :
finset.image prod.fst (s ×ˢ t) ⊆ s
source
theorem finset.subset_product_image_snd {α : Type u_1} {β : Type u_2} {s : finset α} {t : finset β} [decidable_eq β] :
finset.image prod.snd (s ×ˢ t) ⊆ t
source
theorem finset.product_image_fst {α : Type u_1} {β : Type u_2} {s : finset α} {t : finset β} [decidable_eq α] (ht : t.nonempty) :
finset.image prod.fst (s ×ˢ t) = s
source
theorem finset.product_image_snd {α : Type u_1} {β : Type u_2} {s : finset α} {t : finset β} [decidable_eq β] (ht : s.nonempty) :
finset.image prod.snd (s ×ˢ t) = t
source
theorem finset.subset_product {α : Type u_1} {β : Type u_2} [decidable_eq α] [decidable_eq β] {s : finset (α × β)} :
s ⊆ finset.image prod.fst s ×ˢ finset.image prod.snd s
source
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'
source
theorem finset.product_subset_product_left {α : Type u_1} {β : Type u_2} {s s' : finset α} {t : finset β} (hs : s ⊆ s') :
s ×ˢ t ⊆ s' ×ˢ t
source
theorem finset.product_subset_product_right {α : Type u_1} {β : Type u_2} {s : finset α} {t t' : finset β} (ht : t ⊆ t') :
s ×ˢ t ⊆ s ×ˢ t'
source
theorem finset.map_swap_product {α : Type u_1} {β : Type u_2} (s : finset α) (t : finset β) :
finset.map {to_fun := prod.swap α, inj' := _} (t ×ˢ s) = s ×ˢ t
source
@[simp]
theorem finset.image_swap_product {α : Type u_1} {β : Type u_2} [decidable_eq α] [decidable_eq β] (s : finset α) (t : finset β) :
finset.image prod.swap (t ×ˢ s) = s ×ˢ t
source
theorem finset.product_eq_bUnion {α : Type u_1} {β : Type u_2} [decidable_eq α] [decidable_eq β] (s : finset α) (t : finset β) :
s ×ˢ t = s.bUnion (λ (a : α), finset.image (λ (b : β), (a, b)) t)
source
theorem finset.product_eq_bUnion_right {α : Type u_1} {β : Type u_2} [decidable_eq α] [decidable_eq β] (s : finset α) (t : finset β) :
s ×ˢ t = t.bUnion (λ (b : β), finset.image (λ (a : α), (a, b)) s)
source
@[simp]
theorem finset.product_bUnion {α : Type u_1} {β : Type u_2} {γ : Type u_3} [decidable_eq γ] (s : finset α) (t : finset β) (f : α × β → finset γ) :
(s ×ˢ t).bUnion f = s.bUnion (λ (a : α), t.bUnion (λ (b : β), f (a, b)))

See also finset.sup_product_left.

source
@[simp]
theorem finset.card_product {α : Type u_1} {β : Type u_2} (s : finset α) (t : finset β) :
(s ×ˢ t).card = s.card * t.card
source
theorem finset.filter_product {α : Type u_1} {β : Type u_2} {s : finset α} {t : finset β} (p : α → Prop) (q : β → Prop) [decidable_pred p] [decidable_pred q] :
finset.filter (λ (x : α × β), p x.fst ∧ q x.snd) (s ×ˢ t) = finset.filter p s ×ˢ finset.filter q t
source
theorem finset.filter_product_left {α : Type u_1} {β : Type u_2} {s : finset α} {t : finset β} (p : α → Prop) [decidable_pred p] :
finset.filter (λ (x : α × β), p x.fst) (s ×ˢ t) = finset.filter p s ×ˢ t
source
theorem finset.filter_product_right {α : Type u_1} {β : Type u_2} {s : finset α} {t : finset β} (q : β → Prop) [decidable_pred q] :
finset.filter (λ (x : α × β), q x.snd) (s ×ˢ t) = s ×ˢ finset.filter q t
source
theorem finset.filter_product_card {α : Type u_1} {β : Type u_2} (s : finset α) (t : finset β) (p : α → Prop) (q : β → Prop) [decidable_pred p] [decidable_pred q] :
(finset.filter (λ (x : α × β), p x.fst ↔ q x.snd) (s ×ˢ t)).card = (finset.filter p s).card * (finset.filter q t).card + (finset.filter (not ∘ p) s).card * (finset.filter (not ∘ q) t).card
source
theorem finset.empty_product {α : Type u_1} {β : Type u_2} (t : finset β) :
∅ ×ˢ t = ∅
source
theorem finset.product_empty {α : Type u_1} {β : Type u_2} (s : finset α) :
s ×ˢ ∅ = ∅
source
theorem finset.nonempty.product {α : Type u_1} {β : Type u_2} {s : finset α} {t : finset β} (hs : s.nonempty) (ht : t.nonempty) :
(s ×ˢ t).nonempty
source
theorem finset.nonempty.fst {α : Type u_1} {β : Type u_2} {s : finset α} {t : finset β} (h : (s ×ˢ t).nonempty) :
s.nonempty
source
theorem finset.nonempty.snd {α : Type u_1} {β : Type u_2} {s : finset α} {t : finset β} (h : (s ×ˢ t).nonempty) :
t.nonempty
source
@[simp]
theorem finset.nonempty_product {α : Type u_1} {β : Type u_2} {s : finset α} {t : finset β} :
(s ×ˢ t).nonempty ↔ s.nonempty ∧ t.nonempty
source
@[simp]
theorem finset.product_eq_empty {α : Type u_1} {β : Type u_2} {s : finset α} {t : finset β} :
s ×ˢ t = ∅ ↔ s = ∅ ∨ t = ∅
source
@[simp]
theorem finset.singleton_product {α : Type u_1} {β : Type u_2} {t : finset β} {a : α} :
{a} ×ˢ t = finset.map {to_fun := prod.mk a, inj' := _} t
source
@[simp]
theorem finset.product_singleton {α : Type u_1} {β : Type u_2} {s : finset α} {b : β} :
s ×ˢ {b} = finset.map {to_fun := λ (i : α), (i, b), inj' := _} s
source
theorem finset.singleton_product_singleton {α : Type u_1} {β : Type u_2} {a : α} {b : β} :
{a} ×ˢ {b} = {(a, b)}
source
@[simp]
theorem finset.union_product {α : Type u_1} {β : Type u_2} {s s' : finset α} {t : finset β} [decidable_eq α] [decidable_eq β] :
(s ∪ s') ×ˢ t = s ×ˢ t ∪ s' ×ˢ t
source
@[simp]
theorem finset.product_union {α : Type u_1} {β : Type u_2} {s : finset α} {t t' : finset β} [decidable_eq α] [decidable_eq β] :
s ×ˢ (t ∪ t') = s ×ˢ t ∪ s ×ˢ t'
source
theorem finset.inter_product {α : Type u_1} {β : Type u_2} {s s' : finset α} {t : finset β} [decidable_eq α] [decidable_eq β] :
(s ∩ s') ×ˢ t = s ×ˢ t ∩ s' ×ˢ t
source
theorem finset.product_inter {α : Type u_1} {β : Type u_2} {s : finset α} {t t' : finset β} [decidable_eq α] [decidable_eq β] :
s ×ˢ (t ∩ t') = s ×ˢ t ∩ s ×ˢ t'
source
theorem finset.product_inter_product {α : Type u_1} {β : Type u_2} {s s' : finset α} {t t' : finset β} [decidable_eq α] [decidable_eq β] :
s ×ˢ t ∩ s' ×ˢ t' = (s ∩ s') ×ˢ (t ∩ t')
source
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'
source
@[simp]
theorem finset.disj_union_product {α : Type u_1} {β : Type u_2} {s s' : finset α} {t : finset β} (hs : disjoint s s') :
s.disj_union s' hs ×ˢ t = (s ×ˢ t).disj_union (s' ×ˢ t) _
source
@[simp]
theorem finset.product_disj_union {α : Type u_1} {β : Type u_2} {s : finset α} {t t' : finset β} (ht : disjoint t t') :
s ×ˢ t.disj_union t' ht = (s ×ˢ t).disj_union (s ×ˢ t') _
source
def finset.diag {α : Type u_1} [decidable_eq α] (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
source
def finset.off_diag {α : Type u_1} [decidable_eq α] (s : finset α) :
finset (α × α)

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

Equations
source
@[simp]
theorem finset.mem_diag {α : Type u_1} [decidable_eq α] {s : finset α} {x : α × α} :
x ∈ s.diag ↔ x.fst ∈ s ∧ x.fst = x.snd
source
@[simp]
theorem finset.mem_off_diag {α : Type u_1} [decidable_eq α] {s : finset α} {x : α × α} :
x ∈ s.off_diag ↔ x.fst ∈ s ∧ x.snd ∈ s ∧ x.fst ≠ x.snd
source
@[simp, norm_cast]
theorem finset.coe_off_diag {α : Type u_1} [decidable_eq α] (s : finset α) :
↑(s.off_diag) = ↑s.off_diag
source
@[simp]
theorem finset.diag_card {α : Type u_1} [decidable_eq α] (s : finset α) :
s.diag.card = s.card
source
@[simp]
theorem finset.off_diag_card {α : Type u_1} [decidable_eq α] (s : finset α) :
s.off_diag.card = s.card * s.card - s.card
source
theorem finset.diag_mono {α : Type u_1} [decidable_eq α] :
monotone finset.diag
source
theorem finset.off_diag_mono {α : Type u_1} [decidable_eq α] :
monotone finset.off_diag
source
@[simp]
theorem finset.diag_empty {α : Type u_1} [decidable_eq α] :
∅.diag = ∅
source
@[simp]
theorem finset.off_diag_empty {α : Type u_1} [decidable_eq α] :
∅.off_diag = ∅
source
@[simp]
theorem finset.diag_union_off_diag {α : Type u_1} [decidable_eq α] (s : finset α) :
s.diag ∪ s.off_diag = s ×ˢ s
source
@[simp]
theorem finset.disjoint_diag_off_diag {α : Type u_1} [decidable_eq α] (s : finset α) :
disjoint s.diag s.off_diag
source
theorem finset.product_sdiff_diag {α : Type u_1} [decidable_eq α] (s : finset α) :
s ×ˢ s \ s.diag = s.off_diag
source
theorem finset.product_sdiff_off_diag {α : Type u_1} [decidable_eq α] (s : finset α) :
s ×ˢ s \ s.off_diag = s.diag
source
theorem finset.diag_inter {α : Type u_1} [decidable_eq α] (s t : finset α) :
(s ∩ t).diag = s.diag ∩ t.diag
source
theorem finset.off_diag_inter {α : Type u_1} [decidable_eq α] (s t : finset α) :
(s ∩ t).off_diag = s.off_diag ∩ t.off_diag
source
theorem finset.diag_union {α : Type u_1} [decidable_eq α] (s t : finset α) :
(s ∪ t).diag = s.diag ∪ t.diag
source
theorem finset.off_diag_union {α : Type u_1} [decidable_eq α] {s t : finset α} (h : disjoint s t) :
(s ∪ t).off_diag = s.off_diag ∪ t.off_diag ∪ s ×ˢ t ∪ t ×ˢ s
source
@[simp]
theorem finset.off_diag_singleton {α : Type u_1} [decidable_eq α] (a : α) :
{a}.off_diag = ∅
source
theorem finset.diag_singleton {α : Type u_1} [decidable_eq α] (a : α) :
{a}.diag = {(a, a)}
source
theorem finset.diag_insert {α : Type u_1} [decidable_eq α] {s : finset α} (a : α) :
(has_insert.insert a s).diag = has_insert.insert (a, a) s.diag
source
theorem finset.off_diag_insert {α : Type u_1} [decidable_eq α] {s : finset α} (a : α) (has : a ∉ s) :
(has_insert.insert a s).off_diag = s.off_diag ∪ {a} ×ˢ s ∪ s ×ˢ {a}