The cartesian product of finsets
pi
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.
The empty dependent product function, defined on the emptyset. The assumption a ∈ ∅ is never
satisfied.
Equations
- finset.pi.empty β a h = multiset.pi.empty β a h
def
finset.pi.cons
{α : Type u_1}
{δ : α → Type u_2}
[decidable_eq α]
(s : finset α)
(a : α)
(b : δ a)
(f : Π (a : α), a ∈ s → δ a)
(a' : α) :
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
- finset.pi.cons s a b f a' h = multiset.pi.cons s.val a b f a' _
@[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 α} :
a ∉ s → function.injective (finset.pi.cons s a b)
@[simp]
theorem
finset.pi_empty
{α : Type u_1}
{δ : α → Type u_2}
[decidable_eq α]
{t : Π (a : α), finset (δ a)} :
∅.pi t = {finset.pi.empty δ}
@[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 → (has_insert.insert a s).pi t = (t a).bind (λ (b : δ a), finset.image (finset.pi.cons s a b) (s.pi t))
theorem
finset.pi_subset
{α : Type u_1}
{δ : α → Type u_2}
[decidable_eq α]
{s : finset α}
(t₁ t₂ : Π (a : α), finset (δ a)) :
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 : α} :