The cartesian product of finsets #
pi #
The empty dependent product function, defined on the empty set. The assumption a ∈ ∅∈ ∅∅ is never
satisfied.
Equations
- Finset.Pi.empty β a h = Multiset.Pi.empty β a h
def
Finset.pi
{α : Type u_1}
{β : α → Type u}
[inst : DecidableEq α]
(s : Finset α)
(t : (a : α) → Finset (β 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
- Finset.pi s t = { val := Multiset.pi s.val fun a => (t a).val, nodup := (_ : Multiset.Nodup (Multiset.pi s.val fun a => (t a).val)) }
@[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
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
- Finset.Pi.cons s a b f a' h = Multiset.Pi.cons s.val a b f a' (_ : a' ∈ a ::ₘ s.val)
@[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)
:
Function.Injective (Finset.Pi.cons s a b)
@[simp]
theorem
Finset.pi_empty
{α : Type u_1}
{β : α → Type u}
[inst : DecidableEq α]
{t : (a : α) → Finset (β a)}
:
Finset.pi ∅ t = {Finset.Pi.empty β}
@[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)
:
Finset.pi (insert a s) t = Finset.bunionᵢ (t a) fun b => Finset.image (Finset.Pi.cons s a b) (Finset.pi s t)
theorem
Finset.pi_singletons
{α : Type u_2}
[inst : DecidableEq α]
{β : Type u_1}
(s : Finset α)
(f : α → β)
:
theorem
Finset.pi_const_singleton
{α : Type u_2}
[inst : DecidableEq α]
{β : Type u_1}
(s : Finset α)
(i : β)
: