# The Cartesian product of multisets #

## Main definitions #

- `Multiset.pi`: Cartesian product of multisets indexed by a multiset.

source
def Multiset.Pi.empty {α : Type u_1} (δ : α → Sort u_3) (a : α) :
a ∈ 0 → δ a

Given `δ : α → Sort*`, `Pi.empty δ` is the trivial dependent function out of the empty multiset.

Equations

Instances For

source
def Multiset.Pi.cons {α : Type u_1} [DecidableEq α] {δ : α → Sort u_2} (m : Multiset α) (a : α) (b : δ a) (f : (a : α) → a ∈ m → δ a) (a' : α) :
a' ∈ a ::ₘ m → δ a'

Given `δ : α → Sort*`, 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

- Multiset.Pi.cons m a b f a' ha' = if h : a' = a then ⋯ ▸ b else f a' ⋯

Instances For

source
theorem Multiset.Pi.cons_same {α : Type u_1} [DecidableEq α] {δ : α → Sort u_2} {m : Multiset α} {a : α} {b : δ a} {f : (a : α) → a ∈ m → δ a} (h : a ∈ a ::ₘ m) :
cons m a b f a h = b
source
theorem Multiset.Pi.cons_ne {α : Type u_1} [DecidableEq α] {δ : α → Sort u_2} {m : Multiset α} {a a' : α} {b : δ a} {f : (a : α) → a ∈ m → δ a} (h' : a' ∈ a ::ₘ m) (h : a' ≠ a) :
cons m a b f a' h' = f a' ⋯
source
theorem Multiset.Pi.cons_swap {α : Type u_1} [DecidableEq α] {δ : α → Sort u_2} {a a' : α} {b : δ a} {b' : δ a'} {m : Multiset α} {f : (a : α) → a ∈ m → δ a} (h : a ≠ a') :
cons (a' ::ₘ m) a b (cons m a' b' f) ≍ cons (a ::ₘ m) a' b' (cons m a b f)
source
@[simp]
theorem Multiset.Pi.cons_eta {α : Type u_1} [DecidableEq α] {δ : α → Sort u_2} {m : Multiset α} {a : α} (f : (a' : α) → a' ∈ a ::ₘ m → δ a') :
(cons m a (f a ⋯) fun (a' : α) (ha' : a' ∈ m) => f a' ⋯) = f
source
theorem Multiset.Pi.cons_map {α : Type u_1} [DecidableEq α] {δ : α → Sort u_2} {m : Multiset α} {a : α} (b : δ a) (f : (a' : α) → a' ∈ m → δ a') {δ' : α → Sort u_3} (φ : ⦃a' : α⦄ → δ a' → δ' a') :
(cons m a (φ b) fun (a' : α) (ha' : a' ∈ m) => φ (f a' ha')) = fun (a' : α) (ha' : a' ∈ a ::ₘ m) => φ (cons m a b f a' ha')
source
theorem Multiset.Pi.forall_rel_cons_ext {α : Type u_1} [DecidableEq α] {δ : α → Sort u_2} {m : Multiset α} {a : α} {r : ⦃a : α⦄ → δ a → δ a → Prop} {b₁ b₂ : δ a} {f₁ f₂ : (a' : α) → a' ∈ m → δ a'} (hb : r b₁ b₂) (hf : ∀ (a : α) (ha : a ∈ m), r (f₁ a ha) (f₂ a ha)) (a✝ : α) (ha : a✝ ∈ a ::ₘ m) :
r (cons m a b₁ f₁ a✝ ha) (cons m a b₂ f₂ a✝ ha)
source
theorem Multiset.Pi.cons_injective {α : Type u_1} [DecidableEq α] {δ : α → Sort u_2} {a : α} {b : δ a} {s : Multiset α} (hs : a ∉ s) :
Function.Injective (cons s a b)
source
def Multiset.pi {α : Type u_1} [DecidableEq α] {β : α → 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

- m.pi t = m.recOn {Multiset.Pi.empty β} (fun (a : α) (m : Multiset α) (p : Multiset ((a : α) → a ∈ m → β a)) => (t a).bind fun (b : β a) => Multiset.map (Multiset.Pi.cons m a b) p) ⋯

Instances For

source
@[simp]
theorem Multiset.pi_zero {α : Type u_1} [DecidableEq α] {β : α → Type u_2} (t : (a : α) → Multiset (β a)) :
pi 0 t = {Pi.empty β}
source
@[simp]
theorem Multiset.pi_cons {α : Type u_1} [DecidableEq α] {β : α → Type u_2} (m : Multiset α) (t : (a : α) → Multiset (β a)) (a : α) :
(a ::ₘ m).pi t = (t a).bind fun (b : β a) => map (Pi.cons m a b) (m.pi t)
source
theorem Multiset.card_pi {α : Type u_1} [DecidableEq α] {β : α → Type u_2} (m : Multiset α) (t : (a : α) → Multiset (β a)) :
(m.pi t).card = (map (fun (a : α) => (t a).card) m).prod
source
theorem Multiset.Nodup.pi {α : Type u_1} [DecidableEq α] {β : α → Type u_2} {s : Multiset α} {t : (a : α) → Multiset (β a)} :
s.Nodup → (∀ a ∈ s, (t a).Nodup) → (s.pi t).Nodup
source
theorem Multiset.mem_pi {α : Type u_1} [DecidableEq α] {β : α → 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