nodup_append_comm

Mathlib.Data.List.Nodup

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

English

Nodup(l1 ++ l2) is equivalent to Nodup(l2 ++ l1).

Русский

Без повторов в порядке l1 ++ l2 эквивалентно безповторности в порядке l2 ++ l1.

LaTeX

$$$ \\operatorname{Nodup}(l_1 ++ l_2) \\iff \\operatorname{Nodup}(l_2 ++ l_1) $$$

Lean4

theorem nodup_append_comm {l₁ l₂ : List α} : Nodup (l₁ ++ l₂) ↔ Nodup (l₂ ++ l₁) := by
  simp only [nodup_append', and_left_comm, disjoint_comm]

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

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

Разделы

Аффилиация

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