Iio_castSucc

Mathlib.Data.Fintype.Fin

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

English

For i in Fin n, the set of elements less than castSucc i equals the image of Iio i under castSuccEmb.

Русский

Для i в Fin n множество элементов меньше castSucc i равно образу Iio i под castSuccEmb.

LaTeX

$$$ \\mathrm{Iio}(i.castSucc) = (\\mathrm{Iio}(i)).\\mathrm{map}(\\mathrm{Fin.castSuccEmb}) $$$

Lean4

theorem Iio_castSucc (i : Fin n) : Iio (castSucc i) = (Iio i).map Fin.castSuccEmb := by simp

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

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

Разделы

Аффилиация

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