mathlib documentation

data.multiset.pi

The cartesian product of multisets

def multiset.pi.empty {α : Type u_1} (δ : α → Type u_2) (a : α) :
a 0δ a

Given δ : α → Type*, pi.empty δ is the trivial dependent function out of the empty multiset.

def multiset.pi.cons {α : Type u_1} [decidable_eq α] {δ : α → Type u_2} (m : multiset α) (a : α) (b : δ a) (f : Π (a : α), a mδ a) (a' : α) :
a' a ::ₘ mδ a'

Given δ : α → Type*, a multiset m and a term a, as well as a term b : δ a and a function f such that f a' : δ a' for all a' in m, pi.cons m a b f is a function g such that g a'' : δ a'' for all a'' in a ::ₘ m.

Equations
theorem multiset.pi.cons_same {α : Type u_1} [decidable_eq α] {δ : α → Type u_2} {m : multiset α} {a : α} {b : δ a} {f : Π (a : α), a mδ a} (h : a a ::ₘ m) :
multiset.pi.cons m a b f a h = b

theorem multiset.pi.cons_ne {α : Type u_1} [decidable_eq α] {δ : α → Type u_2} {m : multiset α} {a a' : α} {b : δ a} {f : Π (a : α), a mδ a} (h' : a' a ::ₘ m) (h : a' a) :
multiset.pi.cons m a b f a' h' = f a' _

theorem multiset.pi.cons_swap {α : Type u_1} [decidable_eq α] {δ : α → Type u_2} {a a' : α} {b : δ a} {b' : δ a'} {m : multiset α} {f : Π (a : α), a mδ a} :
a a'multiset.pi.cons (a' ::ₘ m) a b (multiset.pi.cons m a' b' f) == multiset.pi.cons (a ::ₘ m) a' b' (multiset.pi.cons m a b f)

def multiset.pi {α : Type u_1} [decidable_eq α] {δ : α → Type u_2} (m : multiset α) :
(Π (a : α), multiset (δ a))multiset (Π (a : α), a mδ a)

pi m t constructs the Cartesian product over t indexed by m.

Equations
@[simp]
theorem multiset.pi_zero {α : Type u_1} [decidable_eq α] {δ : α → Type u_2} (t : Π (a : α), multiset (δ a)) :

@[simp]
theorem multiset.pi_cons {α : Type u_1} [decidable_eq α] {δ : α → Type u_2} (m : multiset α) (t : Π (a : α), multiset (δ a)) (a : α) :
(a ::ₘ m).pi t = (t a).bind (λ (b : δ a), multiset.map (multiset.pi.cons m a b) (m.pi t))

theorem multiset.pi_cons_injective {α : Type u_1} [decidable_eq α] {δ : α → Type u_2} {a : α} {b : δ a} {s : multiset α} :

theorem multiset.card_pi {α : Type u_1} [decidable_eq α] {δ : α → Type u_2} (m : multiset α) (t : Π (a : α), multiset (δ a)) :
(m.pi t).card = (multiset.map (λ (a : α), (t a).card) m).prod

theorem multiset.nodup_pi {α : Type u_1} [decidable_eq α] {δ : α → Type u_2} {s : multiset α} {t : Π (a : α), multiset (δ a)} :
s.nodup(∀ (a : α), a s(t a).nodup)(s.pi t).nodup

theorem multiset.mem_pi {α : Type u_1} [decidable_eq α] {δ : α → Type u_2} (m : multiset α) (t : Π (a : α), multiset (δ a)) (f : Π (a : α), a mδ a) :
f m.pi t ∀ (a : α) (h : a m), f a h t a