image_castSucc_Iic

Mathlib.Order.Interval.Set.Fin

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

English

The image of the interval Iic i under the castSucc map is the interval Iic i.castSucc.

Русский

Образ интервала Iic i при отображении castSucc равен Iic i.castSucc.

LaTeX

$$$ \operatorname{image}(\operatorname{Fin.castSucc})\bigl(\operatorname{Iic} i\bigr) = \operatorname{Iic} i.castSucc $$$

Lean4

@[simp]
theorem image_castSucc_Iic (i : Fin n) : castSucc '' Iic i = Iic i.castSucc :=
  image_castAdd_Iic ..

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

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

Разделы

Аффилиация

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