Theorems · Theorem · combinatorics

Multiset.mem_pi

∀ {α : Type u_1} [inst : 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

Defined in

Mathlib.Data.Multiset.Pi

Cited by

2 results in Mathlib

Foundations

Depth 62 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

DecidableEq