English
Embed Fin n into Fin (n+1) by prepending the element 0 to the univ of Fin n.
Русский
Встраиваем Fin n в Fin (n+1), помещая в начало элементов 0 к множеству Fin n.
LaTeX
$$$$ \\operatorname{univ}_{\\mathrm{Fin}(n+1)} = \\operatorname{Finset.cons} 0 \\left(\\operatorname{univ}_{\\mathrm{Fin} n} .\\operatorname{map} \\left(\\langle \\mathrm{Fin.succ}, \\mathrm{Fin.succ_injective} \\_\\rangle\\right)\\right). $$$$
Lean4
/-- Embed `Fin n` into `Fin (n + 1)` by prepending zero to the `univ` -/
theorem univ_succ (n : ℕ) :
(univ : Finset (Fin (n + 1))) =
Finset.cons 0 (univ.map ⟨Fin.succ, Fin.succ_injective _⟩) (by simp [map_eq_image]) :=
by simp [map_eq_image]
