English
For i in Fin n, the set of elements greater than i.succ equals the image of Ioi i under the succ embedding.
Русский
Для i в Fin n множество элементов больше i.succ равно образу Ioi i под вложением succEmb.
LaTeX
$$$ \\mathrm{Ioi}(i.succ) = \\mathrm{Ioi}(i).\\mathrm{map}(\\mathrm{Fin.succEmb}(n)) $$$
Lean4
theorem Ioi_succ (i : Fin n) : Ioi i.succ = (Ioi i).map (Fin.succEmb _) := by simp