English
There is a natural bijection between the set of k+1-multisets over Fin(n+1) that contain 0 and the set of k-multisets over Fin(n+1).
Русский
Существует естественная биекция между множествами мультисет размером k+1 над Fin(n+1), содержащими 0, и мультисетами размера k над Fin(n+1).
LaTeX
$$$\{ s : \mathrm{Sym}(\mathrm{Fin}(n+1))\ (k+1) \mid \uparrow 0 \in s \} \cong \mathrm{Sym}(\mathrm{Fin}(n+1))\ k$$$
Lean4
/-- Over `Fin (n + 1)`, the multisets of size `k + 1` containing `0` are equivalent to those of size
`k`, as demonstrated by respectively erasing or appending `0`. -/
protected def e1 {n k : ℕ} : { s : Sym (Fin (n + 1)) (k + 1) // ↑0 ∈ s } ≃ Sym (Fin n.succ) k
where
toFun s := s.1.erase 0 s.2
invFun s := ⟨cons 0 s, mem_cons_self 0 s⟩
left_inv s := by simp
right_inv s := by simp
