map_revPerm_Iic

Mathlib.Order.Interval.Finset.Fin

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

English

Let i ∈ Fin n. Then (Iic i).map revPerm.toEmbedding = Ici(i.rev).

Русский

Пусть i ∈ Fin n. Тогда (Iic i).map revPerm.toEmbedding = Ici(i.rev).

LaTeX

$$$ (Iic i).map revPerm.toEmbedding = Ici i.rev $$$

Lean4

@[simp]
theorem map_revPerm_Iic (i : Fin n) : (Iic i).map revPerm.toEmbedding = Ici i.rev := by simp [← coe_inj]

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

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

Разделы

Аффилиация

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