The cartesian product of multisets
def
multiset.pi.cons
{α : Type u_1}
[decidable_eq α]
{δ : α → Type u_2}
(m : multiset α)
(a : α)
(b : δ a)
(f : Π (a : α), a ∈ m → δ a)
(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.
Given δ : α → Type*, pi.empty δ is the trivial dependent function out of the empty multiset.
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)
pi m t constructs the Cartesian product over t indexed by m.
Equations
- m.pi t = m.rec_on {multiset.pi.empty δ} (λ (a : α) (m : multiset α) (p : multiset (Π (a : α), a ∈ m → δ a)), (t a).bind (λ (b : δ a), multiset.map (multiset.pi.cons m a b) p)) _
@[simp]
theorem
multiset.pi_zero
{α : Type u_1}
[decidable_eq α]
{δ : α → Type u_2}
(t : Π (a : α), multiset (δ a)) :
0.pi t = multiset.pi.empty δ :: 0
@[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 α} :
a ∉ s → function.injective (multiset.pi.cons s a b)
theorem
multiset.card_pi
{α : Type u_1}
[decidable_eq α]
{δ : α → Type u_2}
(m : multiset α)
(t : Π (a : α), multiset (δ a)) :
theorem
multiset.nodup_pi
{α : Type u_1}
[decidable_eq α]
{δ : α → Type u_2}
{s : multiset α}
{t : Π (a : α), multiset (δ a)} :