preimage_rev_Ioc

Mathlib.Order.Interval.Set.Fin

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

English

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

Русский

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

LaTeX

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

Lean4

@[simp]
theorem preimage_rev_Ioc (i j : Fin n) : rev ⁻¹' Ioc i j = Ico j.rev i.rev := by ext;
  simp [lt_rev_iff, rev_le_iff, and_comm]

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

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

Разделы

Аффилиация

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