dedup_append — Mathlib

English

Dedup of concatenation equals left list unduplicated followed by dedup of right: dedup(l1 ++ l2) = l1 ∪ dedup(l2).

Русский

Dedup конкатенации равен объединению l1 и dedup(l2).

LaTeX

$$$\\mathrm{dedup}(l_1 \\;+\\; l_2) = l_1 \\cup \\mathrm{dedup}(l_2)$$$

Lean4

theorem dedup_append (l₁ l₂ : List α) : dedup (l₁ ++ l₂) = l₁ ∪ dedup l₂ :=
  by
  induction l₁ with
  | nil => rfl
  | cons a l₁ IH => ?_
  simp only [cons_union] at *
  rw [← IH, cons_append]
  by_cases h : a ∈ dedup (l₁ ++ l₂)
  · rw [dedup_cons_of_mem' h, insert_of_mem h]
  · rw [dedup_cons_of_notMem' h, insert_of_not_mem h]

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