The cartesian product of multisets #
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' : α)
(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.
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}
(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)
def
multiset.pi
{α : Type u_1}
[decidable_eq α]
{δ : α → Type u_2}
(m : multiset α)
(t : Π (a : α), multiset (δ a)) :
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 δ}
@[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 α}
(hs : 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)) :
⇑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)} :
@[simp]
theorem
multiset.pi.cons_ext
{α : Type u_1}
[decidable_eq α]
{δ : α → Type u_2}
{m : multiset α}
{a : α}
(f : Π (a' : α), a' ∈ a ::ₘ m → δ a') :
multiset.pi.cons m a (f a _) (λ (a' : α) (ha' : a' ∈ m), f a' _) = f