The cartesian product of multisets #
Given δ : α → Type*
, Pi.empty δ
is the trivial dependent function out of the empty
multiset.
Equations
- Multiset.Pi.empty δ a✝ a = Multiset.Pi.empty.match_1 (fun (a : α) (a_1 : a ∈ 0) => δ a) a✝ a
Instances For
def
Multiset.Pi.cons
{α : Type u_1}
[DecidableEq α]
{δ : α → Sort v}
(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
.
Equations
- Multiset.Pi.cons m a b f a' ha' = if h : a' = a then ⋯ ▸ b else f a' ⋯
Instances For
theorem
Multiset.Pi.cons_same
{α : Type u_1}
[DecidableEq α]
{δ : α → Sort v}
{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}
[DecidableEq α]
{δ : α → Sort v}
{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}
[DecidableEq α]
{δ : α → Sort v}
{a : α}
{a' : α}
{b : δ a}
{b' : δ a'}
{m : Multiset α}
{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))
@[simp]
theorem
Multiset.pi.cons_eta
{α : Type u_1}
[DecidableEq α]
{δ : α → Sort v}
{m : Multiset α}
{a : α}
(f : (a' : α) → a' ∈ a ::ₘ m → δ a')
:
(Multiset.Pi.cons m a (f a ⋯) fun (a' : α) (ha' : a' ∈ m) => f a' ⋯) = f
theorem
Multiset.Pi.cons_injective
{α : Type u_1}
[DecidableEq α]
{δ : α → Sort v}
{a : α}
{b : δ a}
{s : Multiset α}
(hs : a ∉ s)
:
Function.Injective (Multiset.Pi.cons s a b)
def
Multiset.pi
{α : Type u_1}
[DecidableEq α]
{β : α → Type u}
(m : Multiset α)
(t : (a : α) → Multiset (β 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.
Instances For
@[simp]
theorem
Multiset.pi_zero
{α : Type u_1}
[DecidableEq α]
{β : α → Type u}
(t : (a : α) → Multiset (β a))
:
Multiset.pi 0 t = {Multiset.Pi.empty β}
@[simp]
theorem
Multiset.pi_cons
{α : Type u_1}
[DecidableEq α]
{β : α → Type u}
(m : Multiset α)
(t : (a : α) → Multiset (β a))
(a : α)
:
Multiset.pi (a ::ₘ m) t = Multiset.bind (t a) fun (b : β a) => Multiset.map (Multiset.Pi.cons m a b) (Multiset.pi m t)
theorem
Multiset.card_pi
{α : Type u_1}
[DecidableEq α]
{β : α → Type u}
(m : Multiset α)
(t : (a : α) → Multiset (β a))
:
Multiset.card (Multiset.pi m t) = Multiset.prod (Multiset.map (fun (a : α) => Multiset.card (t a)) m)
theorem
Multiset.Nodup.pi
{α : Type u_1}
[DecidableEq α]
{β : α → Type u}
{s : Multiset α}
{t : (a : α) → Multiset (β a)}
:
Multiset.Nodup s → (∀ a ∈ s, Multiset.Nodup (t a)) → Multiset.Nodup (Multiset.pi s t)
theorem
Multiset.mem_pi
{α : Type u_1}
[DecidableEq α]
{β : α → Type u}
(m : Multiset α)
(t : (a : α) → Multiset (β a))
(f : (a : α) → a ∈ m → β a)
:
f ∈ Multiset.pi m t ↔ ∀ (a : α) (h : a ∈ m), f a h ∈ t a