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
: Turnss : Finset α
,t : Finset β
into their product inFinset (α × β)
.Finset.diag
: Fors : Finset α
,s.diag
is theFinset (α × α)
of pairs(a, a)
witha ∈ s
.Finset.offDiag
: Fors : Finset α
,s.offDiag
is theFinset (α × α)
of pairs(a, b)
witha, b ∈ s
anda ≠ b
.
prod #
Equations
- Finset.instSProd = { sprod := Finset.product }
theorem
Finset.subset_product
{α : Type u_1}
{β : Type u_2}
[DecidableEq α]
[DecidableEq β]
{s : Finset (α × β)}
:
theorem
Finset.filter_product_card
{α : Type u_1}
{β : Type u_2}
(s : Finset α)
(t : Finset β)
(p : α → Prop)
(q : β → Prop)
[DecidablePred p]
[DecidablePred q]
:
@[simp]
theorem
Finset.union_product
{α : Type u_1}
{β : Type u_2}
{s s' : Finset α}
{t : Finset β}
[DecidableEq α]
[DecidableEq β]
:
@[simp]
theorem
Finset.product_union
{α : Type u_1}
{β : Type u_2}
{s : Finset α}
{t t' : Finset β}
[DecidableEq α]
[DecidableEq β]
:
theorem
Finset.inter_product
{α : Type u_1}
{β : Type u_2}
{s s' : Finset α}
{t : Finset β}
[DecidableEq α]
[DecidableEq β]
:
theorem
Finset.product_inter
{α : Type u_1}
{β : Type u_2}
{s : Finset α}
{t t' : Finset β}
[DecidableEq α]
[DecidableEq β]
:
theorem
Finset.product_inter_product
{α : Type u_1}
{β : Type u_2}
{s s' : Finset α}
{t t' : Finset β}
[DecidableEq α]
[DecidableEq β]
:
@[simp]
@[simp]
@[simp]
@[simp]
@[simp]
theorem
Finset.disjoint_diag_offDiag
{α : Type u_1}
[DecidableEq α]
(s : Finset α)
:
Disjoint s.diag s.offDiag
@[simp]
theorem
Finset.offDiag_filter_lt_eq_filter_le
{ι : Type u_4}
[PartialOrder ι]
[DecidableEq ι]
[DecidableRel LE.le]
[DecidableRel LT.lt]
(s : Finset ι)
: