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.off_diag: For s : finset α, s.off_diag is the finset (α × α) of pairs (a, b) with a, b ∈ s and a ≠ b.

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

s.product t = {val := s.val.product t.val, nodup := _}

source

@[simp]

theorem finset.product_val {α : Type u_1} {β : Type u_2} {s : finset α} {t : finset β} :

(s.product t).val = s.val.product t.val

source

@[simp]

theorem finset.mem_product {α : Type u_1} {β : Type u_2} {s : finset α} {t : finset β} {p : α × β} :

p ∈ s.product 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.product t

source

@[simp, norm_cast]

theorem finset.coe_product {α : Type u_1} {β : Type u_2} (s : finset α) (t : finset β) :

↑(s.product t) = ↑s ×ˢ ↑t

source

theorem finset.subset_product {α : Type u_1} {β : Type u_2} [decidable_eq α] [decidable_eq β] {s : finset (α × β)} :

s ⊆ (finset.image prod.fst s).product (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.product t ⊆ s'.product t'

source

theorem finset.product_subset_product_left {α : Type u_1} {β : Type u_2} {s s' : finset α} {t : finset β} (hs : s ⊆ s') :

s.product t ⊆ s'.product t

source

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

s.product t ⊆ s.product t'

source

theorem finset.product_eq_bUnion {α : Type u_1} {β : Type u_2} [decidable_eq α] [decidable_eq β] (s : finset α) (t : finset β) :

s.product 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.product 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.product 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.product 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.product t) = (finset.filter p s).product (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.product 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 β) :

∅.product t = ∅

source

theorem finset.product_empty {α : Type u_1} {β : Type u_2} (s : finset α) :

s.product ∅ = ∅

source

theorem finset.nonempty.product {α : Type u_1} {β : Type u_2} {s : finset α} {t : finset β} (hs : s.nonempty) (ht : t.nonempty) :

(s.product t).nonempty

source

theorem finset.nonempty.fst {α : Type u_1} {β : Type u_2} {s : finset α} {t : finset β} (h : (s.product t).nonempty) :

s.nonempty

source

theorem finset.nonempty.snd {α : Type u_1} {β : Type u_2} {s : finset α} {t : finset β} (h : (s.product t).nonempty) :

t.nonempty

source

@[simp]

theorem finset.nonempty_product {α : Type u_1} {β : Type u_2} {s : finset α} {t : finset β} :

(s.product t).nonempty ↔ s.nonempty ∧ t.nonempty

source

@[simp]

theorem finset.product_eq_empty {α : Type u_1} {β : Type u_2} {s : finset α} {t : finset β} :

s.product t = ∅ ↔ s = ∅ ∨ t = ∅

source

@[simp]

theorem finset.singleton_product {α : Type u_1} {β : Type u_2} {t : finset β} {a : α} :

{a}.product 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.product {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}.product {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').product t = s.product t ∪ s'.product t

source

@[simp]

theorem finset.product_union {α : Type u_1} {β : Type u_2} {s : finset α} {t t' : finset β} [decidable_eq α] [decidable_eq β] :

s.product (t ∪ t') = s.product t ∪ s.product t'

source

def finset.diag {α : Type u_1} (s : finset α) [decidable_eq α] :

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.filter (λ (a : α × α), a.fst = a.snd) (s.product s)

source

def finset.off_diag {α : Type u_1} (s : finset α) [decidable_eq α] :

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

s.off_diag = finset.filter (λ (a : α × α), a.fst ≠ a.snd) (s.product s)

source

@[simp]

theorem finset.mem_diag {α : Type u_1} (s : finset α) [decidable_eq α] (x : α × α) :

x ∈ s.diag ↔ x.fst ∈ s ∧ x.fst = x.snd

source

@[simp]

theorem finset.mem_off_diag {α : Type u_1} (s : finset α) [decidable_eq α] (x : α × α) :

x ∈ s.off_diag ↔ x.fst ∈ s ∧ x.snd ∈ s ∧ x.fst ≠ x.snd

source

@[simp]

theorem finset.diag_card {α : Type u_1} (s : finset α) [decidable_eq α] :

s.diag.card = s.card

source

@[simp]

theorem finset.off_diag_card {α : Type u_1} (s : finset α) [decidable_eq α] :

s.off_diag.card = (s.card) * s.card - s.card

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} (s : finset α) [decidable_eq α] :

s.diag ∪ s.off_diag = s.product s

source

@[simp]

theorem finset.disjoint_diag_off_diag {α : Type u_1} (s : finset α) [decidable_eq α] :

disjoint s.diag s.off_diag