English
Embed Fin n into Fin (n+1) by inserting at a specified pivot p ∈ Fin (n+1) into the univ, i.e., the univ Fin (n+1) is cons p (univ.map (succAboveEmb p)).
Русский
Встраиваем Fin n в Fin (n+1) вокруг заданного опорного элемента p ∈ Fin (n+1): универcум Fin (n+1) равен cons p (univ.map (succAboveEmb p)).
LaTeX
$$$$ \\operatorname{univ}_{\\mathrm{Fin}(n+1)} = \\operatorname{Finset.cons} \\, p \\, (\\operatorname{univ}_{\\mathrm{Fin} n} .\\operatorname{map} \\operatorname{Fin.succAboveEmb} p). $$$$
Lean4
/-- Embed `Fin n` into `Fin (n + 1)` by inserting
around a specified pivot `p : Fin (n + 1)` into the `univ` -/
theorem univ_succAbove (n : ℕ) (p : Fin (n + 1)) :
(univ : Finset (Fin (n + 1))) = Finset.cons p (univ.map <| Fin.succAboveEmb p) (by simp) := by simp [map_eq_image]
