finsetImage_natAdd_Ici

Mathlib.Order.Interval.Finset.Fin

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

English

For i ∈ Fin n, image of Ici i under natAdd m equals Ici (natAdd m i).

Русский

Для i ∈ Fin n образ Ici i под natAdd m равен Ici (natAdd m i).

LaTeX

$$$$(\\mathrm{Ici}\\ i).\\operatorname{image}(\\mathrm{natAdd}\\ m) = \\mathrm{Ici}(\\mathrm{natAdd}\\ m\,i)$$$$

Lean4

@[simp]
theorem finsetImage_natAdd_Ici (m) (i : Fin n) : (Ici i).image (natAdd m) = Ici (natAdd m i) := by simp [← coe_inj]

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

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

Разделы

Аффилиация

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