English
There is a natural embedding of a multiset into α×ℕ sending each occurrence to the pair (element, occurrence index). The embedding is injective.
Русский
Существует естественное вложение мультимножества в α×ℕ, отправляющее каждое вхождение в пару (элемент, индекс вхождения). Вложение инъективно.
LaTeX
$$coeEmbedding (m : Multiset α) : m ↪ α × ℕ with toFun x := (x, x.2) and inj' defined by unique representation$$
Lean4
/-- The embedding from a multiset into `α × ℕ` where the second coordinate enumerates repeats.
If you are looking for the function `m → α`, that would be plain `(↑)`. -/
@[simps]
def coeEmbedding (m : Multiset α) : m ↪ α × ℕ where
toFun x := (x, x.2)
inj' := by
intro ⟨x, i, hi⟩ ⟨y, j, hj⟩
rintro ⟨⟩
rfl
