finsetImage_rev_Icc

Mathlib.Order.Interval.Finset.Fin

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

English

Let i, j ∈ Fin n. Then the image of the interval Icc(i, j) under the reversal map equals Icc(j.rev, i.rev).

Русский

Пусть i, j ∈ Fin n. Тогда образ Icc(i, j) под отображением разворота равен Icc(j.rev, i.rev).

LaTeX

$$$ (Icc i j).image rev = Icc j.rev i.rev $$$

Lean4

@[simp]
theorem finsetImage_rev_Icc (i j : Fin n) : (Icc i j).image rev = Icc j.rev i.rev := by simp [← coe_inj]

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

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

Разделы

Аффилиация

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