# Documentation

Mathlib.Data.Multiset.Pi

# The cartesian product of multisets #

def Multiset.Pi.empty {α : Type u_1} (δ : αSort u_2) (a : α) :
a 0δ a

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

Equations
def Multiset.Pi.cons {α : Type u_1} [inst : ] {δ : αSort v} (m : ) (a : α) (b : δ a) (f : (a : α) → a mδ a) (a' : α) :
a' a ::ₘ mδ a'

Given δ : α → Type _→ 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} [inst : ] {δ : αSort v} {m : } {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} [inst : ] {δ : αSort v} {m : } {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' (_ : a' m)
theorem Multiset.Pi.cons_swap {α : Type u_1} [inst : ] {δ : αSort v} {a : α} {a' : α} {b : δ a} {b' : δ a'} {m : } {f : (a : α) → a mδ a} (h : a a') :
HEq (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} [inst : ] {β : αType u} (m : ) (t : (a : α) → Multiset (β a)) :
Multiset ((a : α) → a mβ a)

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

Equations
• One or more equations did not get rendered due to their size.
@[simp]
theorem Multiset.pi_zero {α : Type u_1} [inst : ] {β : αType u} (t : (a : α) → Multiset (β a)) :
=
@[simp]
theorem Multiset.pi_cons {α : Type u_1} [inst : ] {β : αType u} (m : ) (t : (a : α) → Multiset (β a)) (a : α) :
Multiset.pi (a ::ₘ m) t = Multiset.bind (t a) fun b => Multiset.map () ()
theorem Multiset.pi_cons_injective {α : Type u_1} [inst : ] {δ : αSort v} {a : α} {b : δ a} {s : } (hs : ¬a s) :
theorem Multiset.card_pi {α : Type u_1} [inst : ] {β : αType u} (m : ) (t : (a : α) → Multiset (β a)) :
Multiset.card () = Multiset.prod (Multiset.map (fun a => Multiset.card (t a)) m)
theorem Multiset.Nodup.pi {α : Type u_1} [inst : ] {β : αType u} {s : } {t : (a : α) → Multiset (β a)} :
(∀ (a : α), a sMultiset.Nodup (t a)) →
@[simp]
theorem Multiset.pi.cons_ext {α : Type u_1} [inst : ] {δ : αSort v} {m : } {a : α} (f : (a' : α) → a' a ::ₘ mδ a') :
(Multiset.Pi.cons m a (f a (_ : a a ::ₘ m)) fun a' ha' => f a' (_ : a' a ::ₘ m)) = f
theorem Multiset.mem_pi {α : Type u_1} [inst : ] {β : αType u} (m : ) (t : (a : α) → Multiset (β a)) (f : (a : α) → a mβ a) :
f ∀ (a : α) (h : a m), f a h t a