dedup_append_right — Mathlib

English

If xs is a subset of ys, dedup(xs ++ ys) = dedup(ys).

Русский

Если xs есть подмножество ys, то dedup(xs ++ ys) = dedup(ys).

LaTeX

$$$xs \\subseteq ys \\Rightarrow \\mathrm{dedup}(xs \\,+\\, ys) = \\mathrm{dedup}(ys)$$$

Lean4

/-- Note that the weaker `List.Subset.dedup_append_left` is proved later. -/
theorem dedup_append_right {xs ys : List α} (h : xs ⊆ ys) : dedup (xs ++ ys) = dedup ys := by
  rw [List.dedup_append, Subset.union_eq_right (List.Subset.trans h <| subset_dedup _)]

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