# Documentation

Mathlib.Data.Finset.Pi

# The cartesian product of finsets #

### pi #

def Finset.Pi.empty {α : Type u_1} (β : αSort u_2) (a : α) (h : 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} [inst : ] (s : ) (t : (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∈ 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} [inst : ] (s : ) (t : (a : α) → Finset (β a)) :
().val = Multiset.pi s.val fun a => (t a).val
@[simp]
theorem Finset.mem_pi {α : Type u_1} {β : αType u} [inst : ] {s : } {t : (a : α) → Finset (β a)} {f : (a : α) → a sβ a} :
f ∀ (a : α) (h : a s), f a h t a
def Finset.Pi.cons {α : Type u_1} {δ : αSort v} [inst : ] (s : ) (a : α) (b : δ a) (f : (a : α) → a sδ a) (a' : α) (h : a' insert a s) :
δ a'

Given a function f defined on a finset s, define a new function on the finset s ∪ {a}∪ {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} {δ : αSort v} [inst : ] (s : ) (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} {δ : αSort v} [inst : ] {s : } {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' (_ : a' s)
theorem Finset.pi_cons_injective {α : Type u_1} {δ : αSort v} [inst : ] {a : α} {b : δ a} {s : } (hs : ¬a s) :
@[simp]
theorem Finset.pi_empty {α : Type u_1} {β : αType u} [inst : ] {t : (a : α) → Finset (β a)} :
= {}
@[simp]
theorem Finset.pi_insert {α : Type u_1} {β : αType u} [inst : ] [inst : (a : α) → DecidableEq (β a)] {s : } {t : (a : α) → Finset (β a)} {a : α} (ha : ¬a s) :
Finset.pi (insert a s) t = Finset.bunionᵢ (t a) fun b => Finset.image () ()
theorem Finset.pi_singletons {α : Type u_2} [inst : ] {β : Type u_1} (s : ) (f : αβ) :
(Finset.pi s fun a => {f a}) = {fun a x => f a}
theorem Finset.pi_const_singleton {α : Type u_2} [inst : ] {β : Type u_1} (s : ) (i : β) :
(Finset.pi s fun x => {i}) = {fun x x => i}
theorem Finset.pi_subset {α : Type u_1} {β : αType u} [inst : ] {s : } (t₁ : (a : α) → Finset (β a)) (t₂ : (a : α) → Finset (β a)) (h : ∀ (a : α), a st₁ a t₂ a) :
Finset.pi s t₁ Finset.pi s t₂
theorem Finset.pi_disjoint_of_disjoint {α : Type u_2} [inst : ] {δ : αType u_1} {s : } (t₁ : (a : α) → Finset (δ a)) (t₂ : (a : α) → Finset (δ a)) {a : α} (ha : a s) (h : Disjoint (t₁ a) (t₂ a)) :
Disjoint (Finset.pi s t₁) (Finset.pi s t₂)