map_revPerm_Ioc

Mathlib.Order.Interval.Finset.Fin

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

English

Let i, j ∈ Fin n. Then the image of uIcc(i, j) under revPerm.toEmbedding equals uIcc(i.rev, j.rev).

Русский

Пусть i, j ∈ Fin n. Тогда образ uIcc(i, j) под Equiv.toEmbedding Fin.revPerm равен uIcc(i.rev, j.rev).

LaTeX

$$$ (uIcc i j).map revPerm.toEmbedding = uIcc i.rev j.rev $$$

Lean4

@[simp]
theorem map_revPerm_Ioc (i j : Fin n) : (Ioc i j).map revPerm.toEmbedding = Ico j.rev i.rev := by simp [← coe_inj]

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

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

Разделы

Аффилиация

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