preimage_rev_Ioo

Mathlib.Order.Interval.Set.Fin

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

English

For i, j ∈ Fin(n), the preimage under rev of Ioo i j is Ioo j.rev i.rev; i.e., rev^{-1}(Ioo i j) = Ioo j.rev i.rev.

Русский

Для i, j ∈ Fin(n) прообраз разворота от Ioo i j равен Ioo j.rev i.rev.

LaTeX

$$$$ \\mathrm{rev}^{-1}(\\Ioo i j) = \\Ioo(j^{\\mathrm{rev}}, i^{\\mathrm{rev}}). $$$$

Lean4

@[simp]
theorem preimage_rev_Ioo (i j : Fin n) : rev ⁻¹' Ioo i j = Ioo j.rev i.rev := by ext;
  simp [lt_rev_iff, rev_lt_iff, and_comm]

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

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

Разделы

Аффилиация

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