mathlib documentation

data.finset.pi

The cartesian product of finsets #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

pi #

def finset.pi.empty {α : Type u_1} (β : α Type 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_2} [decidable_eq α] (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. 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' : α) (h : a' has_insert.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 has_insert.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' has_insert.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 α} (hs : a s) :
@[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 : α} (ha : a s) :
(has_insert.insert a s).pi t = (t a).bUnion (λ (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)) (h : (a : α), a s t₁ a t₂ a) :
s.pi t₁ s.pi t₂
theorem finset.pi_disjoint_of_disjoint {α : Type u_1} [decidable_eq α] {δ : α Type u_2} {s : finset α} (t₁ t₂ : Π (a : α), finset (δ a)) {a : α} (ha : a s) (h : disjoint (t₁ a) (t₂ a)) :
disjoint (s.pi t₁) (s.pi t₂)