Ioi_succ

Mathlib.Data.Fintype.Fin

URI: https://scilib.ai/kg/mathlib#Fin.Ioi_succ

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

Похожие утверждения

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru