finsetImage_rev_uIcc

Mathlib.Order.Interval.Finset.Fin

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

English

Let i, j ∈ Fin n. Then (uIcc i j).image rev = uIcc(i.rev, j.rev).

Русский

Пусть i, j ∈ Fin n. Тогда (uIcc i j).image rev = uIcc(i.rev, j.rev).

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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