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 : DecidableEq α] (s : Finset α) (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 : DecidableEq α] (s : Finset α) (t : (a : α) → Finset (β a)) :
(Finset.pi s t).val = Multiset.pi s.val fun a => (t a).val
@[simp]
theorem Finset.mem_pi {α : Type u_1} {β : αType u} [inst : DecidableEq α] {s : Finset α} {t : (a : α) → Finset (β a)} {f : (a : α) → a sβ a} :
f Finset.pi s t ∀ (a : α) (h : a s), f a h t a
def Finset.Pi.cons {α : Type u_1} {δ : αSort v} [inst : DecidableEq α] (s : Finset α) (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 : DecidableEq α] (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} {δ : αSort v} [inst : DecidableEq α] {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' (_ : a' s)
theorem Finset.pi_cons_injective {α : Type u_1} {δ : αSort v} [inst : DecidableEq α] {a : α} {b : δ a} {s : Finset α} (hs : ¬a s) :
@[simp]
theorem Finset.pi_empty {α : Type u_1} {β : αType u} [inst : DecidableEq α] {t : (a : α) → Finset (β a)} :
@[simp]
theorem Finset.pi_insert {α : Type u_1} {β : αType u} [inst : DecidableEq α] [inst : (a : α) → DecidableEq (β a)] {s : Finset α} {t : (a : α) → Finset (β a)} {a : α} (ha : ¬a s) :
theorem Finset.pi_singletons {α : Type u_2} [inst : DecidableEq α] {β : Type u_1} (s : Finset α) (f : αβ) :
(Finset.pi s fun a => {f a}) = {fun a x => f a}
theorem Finset.pi_const_singleton {α : Type u_2} [inst : DecidableEq α] {β : Type u_1} (s : Finset α) (i : β) :
(Finset.pi s fun x => {i}) = {fun x x => i}
theorem Finset.pi_subset {α : Type u_1} {β : αType u} [inst : DecidableEq α] {s : Finset α} (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 : DecidableEq α] {δ : αType u_1} {s : Finset α} (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₂)