English
Embed Fin n into Fin (n+1) by appending the last element Fin.last n to the univ, i.e., the universal Finset Fin (n+1) is obtained by adding Fin.last n to the image of univ under Fin.castSuccEmb.
Русский
Встраиваем Fin n в Fin (n+1) добавляя к унив Fin (n+1) элемент Fin.last n; универcум Fin (n+1) получается дополняя образ univ под Fin.castSuccEmb последним элементом.
LaTeX
$$$$ \\operatorname{univ}_{\\mathrm{Fin}(n+1)} = \\operatorname{Finset.cons}(\\operatorname{Fin.last} \\, n, \\operatorname{univ}_{\\mathrm{Fin} n} .\\operatorname{map} \\operatorname{Fin.castSuccEmb}). $$$$
Lean4
/-- Embed `Fin n` into `Fin (n + 1)` by appending a new `Fin.last n` to the `univ` -/
theorem univ_castSuccEmb (n : ℕ) :
(univ : Finset (Fin (n + 1))) = Finset.cons (Fin.last n) (univ.map Fin.castSuccEmb) (by simp [map_eq_image]) := by
simp [map_eq_image]
