nodup_reverse

Mathlib.Data.List.Nodup

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

English

Nodup(l) if and only if Nodup(reverse(l)).

Русский

Безповторность списка эквивалентна безповторности его обратного.

LaTeX

$$$\\operatorname{Nodup}(\\mathrm{reverse}(l)) \\iff \\operatorname{Nodup}(l)$$$

Lean4

@[simp]
theorem nodup_reverse {l : List α} : Nodup (reverse l) ↔ Nodup l :=
  pairwise_reverse.trans <| by simp only [Nodup, Ne, eq_comm]

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

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

Разделы

Аффилиация

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