nodup_middle — Mathlib

English

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

Русский

Безповторность l1 ++ a :: l2 эквивалентна безповторности a :: (l1 ++ l2).

LaTeX

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

Lean4

theorem nodup_middle {a : α} {l₁ l₂ : List α} : Nodup (l₁ ++ a :: l₂) ↔ Nodup (a :: (l₁ ++ l₂)) := by
  simp only [nodup_append', not_or, and_left_comm, and_assoc, nodup_cons, mem_append, disjoint_cons_right]

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