map_succEmb_Iio

Mathlib.Order.Interval.Finset.Fin

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

English

Let i ∈ Fin n. Then the image of Iio(i) under succEmb n equals Ioo(0, i.succ).

Русский

Пусть i ∈ Fin n. Тогда образ Iio(i) под succEmb n равен Ioo(0, i.succ).

LaTeX

$$$ (Iio i).map (succEmb n) = Ioo 0 i.succ $$$

Lean4

@[simp]
theorem map_succEmb_Iio (i : Fin n) : (Iio i).map (succEmb n) = Ioo 0 i.succ := by simp [← coe_inj]

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

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

Разделы

Аффилиация

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