nodup_reverse_iff

Mathlib.Data.List.Cycle

URI: https://scilib.ai/kg/mathlib#Cycle.nodup_reverse_iff

English

Nodup is preserved by reversal: s.reverse.Nodup ↔ s.Nodup.

Русский

Без повторов сохраняется разворотом: s.reverse.Nodup ↔ s.Nodup.

LaTeX

$$$\operatorname{Nodup}(s.reverse) \iff \operatorname{Nodup}(s)$$$

Lean4

@[simp]
theorem nodup_reverse_iff {s : Cycle α} : s.reverse.Nodup ↔ s.Nodup :=
  Quot.inductionOn s fun _ => nodup_reverse

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

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

Разделы

Аффилиация

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