mathlib documentation

data.finset.pi

The cartesian product of finsets

pi

def finset.pi.empty {α : Type u_1} (β : α → Type u_2) (a : α) :
a β a

The empty dependent product function, defined on the empty set. The assumption a ∈ ∅ is never satisfied.

Equations
def finset.pi {α : Type u_1} {δ : α → Type u_2} [decidable_eq α] (s : finset α) :
(Π (a : α), finset (δ a))finset (Π (a : α), a sδ a)

Given a finset s of α and for all a : α a finset t a of δ a, then one can define the finset s.pi t of all functions defined on elements of s taking values in t a for a ∈ s. Note that the elements of s.pi t are only partially defined, on s.

Equations
@[simp]
theorem finset.pi_val {α : Type u_1} {δ : α → Type u_2} [decidable_eq α] (s : finset α) (t : Π (a : α), finset (δ a)) :
(s.pi t).val = s.val.pi (λ (a : α), (t a).val)

@[simp]
theorem finset.mem_pi {α : Type u_1} {δ : α → Type u_2} [decidable_eq α] {s : finset α} {t : Π (a : α), finset (δ a)} {f : Π (a : α), a sδ a} :
f s.pi t ∀ (a : α) (h : a s), f a h t a

def finset.pi.cons {α : Type u_1} {δ : α → Type u_2} [decidable_eq α] (s : finset α) (a : α) (b : δ a) (f : Π (a : α), a sδ a) (a' : α) :
a' insert a sδ a'

Given a function f defined on a finset s, define a new function on the finset s ∪ {a}, equal to f on s and sending a to a given value b. This function is denoted s.pi.cons a b f. If a already belongs to s, the new function takes the value b at a anyway.

Equations
@[simp]
theorem finset.pi.cons_same {α : Type u_1} {δ : α → Type u_2} [decidable_eq α] (s : finset α) (a : α) (b : δ a) (f : Π (a : α), a sδ a) (h : a insert a s) :
finset.pi.cons s a b f a h = b

theorem finset.pi.cons_ne {α : Type u_1} {δ : α → Type u_2} [decidable_eq α] {s : finset α} {a a' : α} {b : δ a} {f : Π (a : α), a sδ a} {h : a' insert a s} (ha : a a') :
finset.pi.cons s a b f a' h = f a' _

theorem finset.pi_cons_injective {α : Type u_1} {δ : α → Type u_2} [decidable_eq α] {a : α} {b : δ a} {s : finset α} :

@[simp]
theorem finset.pi_empty {α : Type u_1} {δ : α → Type u_2} [decidable_eq α] {t : Π (a : α), finset (δ a)} :

@[simp]
theorem finset.pi_insert {α : Type u_1} {δ : α → Type u_2} [decidable_eq α] [Π (a : α), decidable_eq (δ a)] {s : finset α} {t : Π (a : α), finset (δ a)} {a : α} :
a s(insert a s).pi t = (t a).bind (λ (b : δ a), finset.image (finset.pi.cons s a b) (s.pi t))

theorem finset.pi_singletons {α : Type u_1} [decidable_eq α] {β : Type u_2} (s : finset α) (f : α → β) :
s.pi (λ (a : α), {f a}) = {λ (a : α) (_x : a s), f a}

theorem finset.pi_const_singleton {α : Type u_1} [decidable_eq α] {β : Type u_2} (s : finset α) (i : β) :
s.pi (λ (_x : α), {i}) = {λ (_x : α) (_x : _x s), i}

theorem finset.pi_subset {α : Type u_1} {δ : α → Type u_2} [decidable_eq α] {s : finset α} (t₁ t₂ : Π (a : α), finset (δ a)) :
(∀ (a : α), a st₁ a t₂ a)s.pi t₁ s.pi t₂

theorem finset.pi_disjoint_of_disjoint {α : Type u_1} [decidable_eq α] {δ : α → Type u_2} [Π (a : α), decidable_eq (δ a)] {s : finset α} [decidable_eq (Π (a : α), a sδ a)] (t₁ t₂ : Π (a : α), finset (δ a)) {a : α} :
a sdisjoint (t₁ a) (t₂ a)disjoint (s.pi t₁) (s.pi t₂)