English
There is a bijection between Sym(Fin(n+2)) with k not containing 0 and Sym(Fin(n+1)) with k; it is obtained by decrementing all elements by 1 on the forward map and incrementing by 1 on the inverse.
Русский
Существует биекция между Sym(Fin(n+2)) с k не содержащим 0 и Sym(Fin(n+1)) с k; отображение достигается уменьшением всех элементов на 1 в прямом отображении и увеличением на 1 на обратном.
LaTeX
$$$\\{ s : \\mathrm{Sym}(\\mathrm{Fin}(n+2))\\ (k) \\mid \\uparrow 0 \\notin s \\} \\cong \\mathrm{Sym}(\\mathrm{Fin}(n+1))\\ k$$$
Lean4
/-- The multisets of size `k` over `Fin n+2` not containing `0`
are equivalent to those of size `k` over `Fin n+1`,
as demonstrated by respectively decrementing or incrementing every element of the multiset.
-/
protected def e2 {n k : ℕ} : { s : Sym (Fin n.succ.succ) k // ↑0 ∉ s } ≃ Sym (Fin n.succ) k
where
toFun s := map (Fin.predAbove 0) s.1
invFun s := ⟨map (Fin.succAbove 0) s, (mt mem_map.1) (not_exists.2 fun t => not_and.2 fun _ => Fin.succAbove_ne _ t)⟩
left_inv
s := by
ext1
simp only [map_map]
refine (Sym.map_congr fun v hv ↦ ?_).trans (map_id' _)
exact Fin.succAbove_predAbove (ne_of_mem_of_not_mem hv s.2)
right_inv s := by simp only [map_map, comp_apply, ← Fin.castSucc_zero, Fin.predAbove_succAbove, map_id']
