isRotated_reverse_comm_iff

Mathlib.Data.List.Rotate

URI: https://scilib.ai/kg/mathlib#List.isRotated_reverse_comm_iff

English

Reversing both lists preserves rotation relation in the sense that l.reverse is rotated to l'.

Русский

Разворот обеих списков сохраняет вращение: l.reverse вращается к l'.reverse.

LaTeX

$$$ l.reverse \sim_{\mathrm{rot}} l' \iff l \sim_{\mathrm{rot}} l'.reverse $$$

Lean4

theorem isRotated_reverse_comm_iff : l.reverse ~r l' ↔ l ~r l'.reverse := by
  constructor <;>
    · intro h
      simpa using h.reverse

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

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

Разделы

Аффилиация

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