# 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
Instances For
def Finset.pi {α : Type u_1} {β : αType u} [] (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. Note that the elements of s.pi t are only partially defined, on s.

Equations
• s.pi t = { val := s.val.pi fun (a : α) => (t a).val, nodup := }
Instances For
@[simp]
theorem Finset.pi_val {α : Type u_1} {β : αType u} [] (s : ) (t : (a : α) → Finset (β a)) :
(s.pi t).val = s.val.pi fun (a : α) => (t a).val
@[simp]
theorem Finset.mem_pi {α : Type u_1} {β : αType u} [] {s : } {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} {δ : αSort v} [] (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}, 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
Instances For
@[simp]
theorem Finset.Pi.cons_same {α : Type u_1} {δ : αSort v} [] (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} [] {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'
theorem Finset.Pi.cons_injective {α : Type u_1} {δ : αSort v} [] {a : α} {b : δ a} {s : } (hs : as) :
@[simp]
theorem Finset.pi_empty {α : Type u_1} {β : αType u} [] {t : (a : α) → Finset (β a)} :
.pi t = {}
@[simp]
theorem Finset.pi_nonempty {α : Type u_1} {β : αType u} [] {s : } {t : (a : α) → Finset (β a)} :
(s.pi t).Nonempty as, (t a).Nonempty
@[simp]
theorem Finset.pi_insert {α : Type u_1} {β : αType u} [] [(a : α) → DecidableEq (β a)] {s : } {t : (a : α) → Finset (β a)} {a : α} (ha : as) :
(insert a s).pi t = (t a).biUnion fun (b : β a) => Finset.image () (s.pi t)
theorem Finset.pi_singletons {α : Type u_1} [] {β : Type u_2} (s : ) (f : αβ) :
(s.pi fun (a : α) => {f a}) = {fun (a : α) (x : a s) => f a}
theorem Finset.pi_const_singleton {α : Type u_1} [] {β : Type u_2} (s : ) (i : β) :
(s.pi fun (x : α) => {i}) = {fun (x : α) (x : x s) => i}
theorem Finset.pi_subset {α : Type u_1} {β : αType u} [] {s : } (t₁ : (a : α) → Finset (β a)) (t₂ : (a : α) → Finset (β a)) (h : as, t₁ a t₂ a) :
s.pi t₁ s.pi t₂
theorem Finset.pi_disjoint_of_disjoint {α : Type u_1} [] {δ : αType u_2} {s : } (t₁ : (a : α) → Finset (δ a)) (t₂ : (a : α) → Finset (δ a)) {a : α} (ha : a s) (h : Disjoint (t₁ a) (t₂ a)) :
Disjoint (s.pi t₁) (s.pi t₂)