English
Let n be a natural number. The image of the universal Finset of Fin n under the embedding Fin.castSucc consists of all elements of Fin (n+1) except the largest element Fin.last n.
Русский
Пусть n — натуральное число. Образ множества Fin n под отображением Fin.castSucc равен всем элементам Fin (n+1), кроме наибольшего элемента Fin.last n.
LaTeX
$$$$ \\operatorname{image}(\\operatorname{Fin.castSucc}, \\operatorname{univ}(\\mathrm{Fin} \\, n)) = \\mathrm{univ}(\\mathrm{Fin}(n+1)) \\setminus \\{\\operatorname{Fin.last}\\\\, n\\}.$$$$
Lean4
@[simp]
theorem image_castSucc (n : ℕ) : (univ : Finset (Fin n)).image Fin.castSucc = {Fin.last n}ᶜ := by
rw [← Fin.succAbove_last, Fin.image_succAbove_univ]
/- The following three lemmas use `Finset.cons` instead of `insert` and `Finset.map` instead of
`Finset.image` to reduce proof obligations downstream. -/
