mathlib3 documentation

data.multiset.pi

The cartesian product of multisets #

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

def multiset.pi.empty {α : Type u_1} (δ : α Sort u_2) (a : α) (H : 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 α] {δ : α Sort u_3} (m : multiset α) (a : α) (b : δ a) (f : Π (a : α), a m δ a) (a' : α) (H : 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 α] {δ : α Sort u_3} {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 α] {δ : α Sort u_3} {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 α] {δ : α Sort u_3} {a a' : α} {b : δ a} {b' : δ a'} {m : multiset α} {f : Π (a : α), a m δ a} (h : 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)
@[simp]
theorem multiset.pi.cons_eta {α : Type u_1} [decidable_eq α] {δ : α Sort u_3} {m : multiset α} {a : α} (f : Π (a' : α), a' a ::ₘ m δ a') :
multiset.pi.cons m a (f a _) (λ (a' : α) (ha' : a' m), f a' _) = f
theorem multiset.pi.cons_injective {α : Type u_1} [decidable_eq α] {δ : α Sort u_3} {a : α} {b : δ a} {s : multiset α} (hs : a s) :
def multiset.pi {α : Type u_1} [decidable_eq α] {β : α Type u_2} (m : multiset α) (t : Π (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.card_pi {α : Type u_1} [decidable_eq α] {β : α Type u_2} (m : multiset α) (t : Π (a : α), multiset (β a)) :
multiset.card (m.pi t) = (multiset.map (λ (a : α), multiset.card (t a)) m).prod
@[protected]
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