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 #

source

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

Finset.product s t = { val := s.val ×ˢ t.val, nodup := (_ : Multiset.Nodup (s.val ×ˢ t.val)) }

Instances For

source

instance Finset.instSProd {α : Type u_1} {β : Type u_2} :

SProd (Finset α) (Finset β) (Finset (α × β))

Equations

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

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]

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 β} [DecidableEq α] :

Finset.image Prod.fst (s ×ˢ t) ⊆ s

source

theorem Finset.subset_product_image_snd {α : Type u_1} {β : Type u_2} {s : Finset α} {t : Finset β} [DecidableEq β] :

Finset.image Prod.snd (s ×ˢ t) ⊆ t

source

theorem Finset.product_image_fst {α : Type u_1} {β : Type u_2} {s : Finset α} {t : Finset β} [DecidableEq α] (ht : Finset.Nonempty t) :

Finset.image Prod.fst (s ×ˢ t) = s

source

theorem Finset.product_image_snd {α : Type u_1} {β : Type u_2} {s : Finset α} {t : Finset β} [DecidableEq β] (ht : Finset.Nonempty s) :

Finset.image Prod.snd (s ×ˢ t) = t

source

theorem Finset.subset_product {α : Type u_1} {β : Type u_2} [DecidableEq α] [DecidableEq β] {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 : Finset α} {s' : Finset α} {t : Finset β} {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 : Finset α} {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 : Finset β} {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 { toFun := Prod.swap, inj' := (_ : Function.Injective Prod.swap) } (t ×ˢ s) = s ×ˢ t

source

@[simp]

theorem Finset.image_swap_product {α : Type u_1} {β : Type u_2} [DecidableEq (α × β)] (s : Finset α) (t : Finset β) :

Finset.image Prod.swap (t ×ˢ s) = s ×ˢ t

source

theorem Finset.product_eq_biUnion {α : Type u_1} {β : Type u_2} [DecidableEq (α × β)] (s : Finset α) (t : Finset β) :

s ×ˢ t = Finset.biUnion s fun a => Finset.image (fun b => (a, b)) t

source

theorem Finset.product_eq_biUnion_right {α : Type u_1} {β : Type u_2} [DecidableEq (α × β)] (s : Finset α) (t : Finset β) :

s ×ˢ t = Finset.biUnion t fun b => Finset.image (fun a => (a, b)) s

source

@[simp]

theorem Finset.product_biUnion {α : Type u_1} {β : Type u_2} {γ : Type u_3} [DecidableEq γ] (s : Finset α) (t : Finset β) (f : α × β → Finset γ) :

Finset.biUnion (s ×ˢ t) f = Finset.biUnion s fun a => Finset.biUnion t fun 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 β) :

Finset.card (s ×ˢ t) = Finset.card s * Finset.card t

source

theorem Finset.nontrivial_prod_iff {α : Type u_1} {β : Type u_2} {s : Finset α} {t : Finset β} :

Nontrivial { x // x ∈ s ×ˢ t } ↔ Finset.Nonempty s ∧ Finset.Nonempty t ∧ (Nontrivial { x // x ∈ s } ∨ Nontrivial { x // x ∈ t })

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

source

theorem Finset.filter_product {α : Type u_1} {β : Type u_2} {s : Finset α} {t : Finset β} (p : α → Prop) (q : β → Prop) [DecidablePred p] [DecidablePred q] :

Finset.filter (fun 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) [DecidablePred p] :

Finset.filter (fun 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) [DecidablePred q] :

Finset.filter (fun 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) [DecidablePred p] [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)

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 : Finset.Nonempty s) (ht : Finset.Nonempty t) :

Finset.Nonempty (s ×ˢ t)

source

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

Finset.Nonempty s

source

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

Finset.Nonempty t

source

@[simp]

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

Finset.Nonempty (s ×ˢ t) ↔ Finset.Nonempty s ∧ Finset.Nonempty t

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 { toFun := Prod.mk a, inj' := (_ : Function.Injective (Prod.mk a)) } t

source

@[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

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 : Finset α} {s' : Finset α} {t : Finset β} [DecidableEq α] [DecidableEq β] :

(s ∪ s') ×ˢ t = s ×ˢ t ∪ s' ×ˢ t

source

@[simp]

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

s ×ˢ (t ∪ t') = s ×ˢ t ∪ s ×ˢ t'

source

theorem Finset.inter_product {α : Type u_1} {β : Type u_2} {s : Finset α} {s' : Finset α} {t : Finset β} [DecidableEq α] [DecidableEq β] :

(s ∩ s') ×ˢ t = s ×ˢ t ∩ s' ×ˢ t

source

theorem Finset.product_inter {α : Type u_1} {β : Type u_2} {s : Finset α} {t : Finset β} {t' : Finset β} [DecidableEq α] [DecidableEq β] :

s ×ˢ (t ∩ t') = s ×ˢ t ∩ s ×ˢ t'

source

theorem Finset.product_inter_product {α : Type u_1} {β : Type u_2} {s : Finset α} {s' : Finset α} {t : Finset β} {t' : Finset β} [DecidableEq α] [DecidableEq β] :

s ×ˢ t ∩ s' ×ˢ t' = (s ∩ s') ×ˢ (t ∩ t')

source

theorem Finset.disjoint_product {α : Type u_1} {β : Type u_2} {s : Finset α} {s' : Finset α} {t : Finset β} {t' : Finset β} :

Disjoint (s ×ˢ t) (s' ×ˢ t') ↔ Disjoint s s' ∨ Disjoint t t'

source

@[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))

source

@[simp]

theorem Finset.product_disjUnion {α : Type u_1} {β : Type u_2} {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'))

source

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

Equations

Finset.diag s = Finset.filter (fun a => a.fst = a.snd) (s ×ˢ s)

Instances For

source

def Finset.offDiag {α : Type u_1} [DecidableEq α] (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

Finset.offDiag s = Finset.filter (fun a => a.fst ≠ a.snd) (s ×ˢ s)

Instances For

source

@[simp]

theorem Finset.mem_diag {α : Type u_1} [DecidableEq α] {s : Finset α} {x : α × α} :

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

source

@[simp]

theorem Finset.mem_offDiag {α : Type u_1} [DecidableEq α] {s : Finset α} {x : α × α} :

x ∈ Finset.offDiag s ↔ x.fst ∈ s ∧ x.snd ∈ s ∧ x.fst ≠ x.snd

source

@[simp]

theorem Finset.coe_offDiag {α : Type u_1} [DecidableEq α] (s : Finset α) :

↑(Finset.offDiag s) = Set.offDiag ↑s

source

@[simp]

theorem Finset.diag_card {α : Type u_1} [DecidableEq α] (s : Finset α) :

Finset.card (Finset.diag s) = Finset.card s

source

@[simp]

theorem Finset.offDiag_card {α : Type u_1} [DecidableEq α] (s : Finset α) :

Finset.card (Finset.offDiag s) = Finset.card s * Finset.card s - Finset.card s

source

theorem Finset.diag_mono {α : Type u_1} [DecidableEq α] :

Monotone Finset.diag

source

theorem Finset.offDiag_mono {α : Type u_1} [DecidableEq α] :

Monotone Finset.offDiag

source

@[simp]

theorem Finset.diag_empty {α : Type u_1} [DecidableEq α] :

Finset.diag ∅ = ∅

source

@[simp]

theorem Finset.offDiag_empty {α : Type u_1} [DecidableEq α] :

Finset.offDiag ∅ = ∅

source

@[simp]

theorem Finset.diag_union_offDiag {α : Type u_1} [DecidableEq α] (s : Finset α) :

Finset.diag s ∪ Finset.offDiag s = s ×ˢ s

source

@[simp]

theorem Finset.disjoint_diag_offDiag {α : Type u_1} [DecidableEq α] (s : Finset α) :

Disjoint (Finset.diag s) (Finset.offDiag s)

source

theorem Finset.product_sdiff_diag {α : Type u_1} [DecidableEq α] (s : Finset α) :

s ×ˢ s \ Finset.diag s = Finset.offDiag s

source

theorem Finset.product_sdiff_offDiag {α : Type u_1} [DecidableEq α] (s : Finset α) :

s ×ˢ s \ Finset.offDiag s = Finset.diag s

source

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

Finset.diag (s ∩ t) = Finset.diag s ∩ Finset.diag t

source

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

Finset.offDiag (s ∩ t) = Finset.offDiag s ∩ Finset.offDiag t

source

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

Finset.diag (s ∪ t) = Finset.diag s ∪ Finset.diag t

source

theorem Finset.offDiag_union {α : Type u_1} [DecidableEq α] {s : Finset α} {t : Finset α} (h : Disjoint s t) :

Finset.offDiag (s ∪ t) = Finset.offDiag s ∪ Finset.offDiag t ∪ s ×ˢ t ∪ t ×ˢ s

source

@[simp]

theorem Finset.offDiag_singleton {α : Type u_1} [DecidableEq α] (a : α) :

Finset.offDiag {a} = ∅

source

theorem Finset.diag_singleton {α : Type u_1} [DecidableEq α] (a : α) :

Finset.diag {a} = {(a, a)}

source

theorem Finset.diag_insert {α : Type u_1} [DecidableEq α] {s : Finset α} (a : α) :

Finset.diag (insert a s) = insert (a, a) (Finset.diag s)

source

theorem Finset.offDiag_insert {α : Type u_1} [DecidableEq α] {s : Finset α} (a : α) (has : ¬a ∈ s) :

Finset.offDiag (insert a s) = Finset.offDiag s ∪ {a} ×ˢ s ∪ s ×ˢ {a}