dedup_append_left — Mathlib

English

For lists s,t with t ⊆ s, List.dedup(s ++ t) is a permutation of List.dedup(s).

Русский

Для списков s,t с t ⊆ s, List.dedup(s ++ t) эквивалентен по перестановке List.dedup(s).

LaTeX

$$$$List.dedup(s ++ t) \sim List.dedup(s)$$$$

Lean4

/-- Note that the stronger `List.Subset.dedup_append_right` is proved earlier. -/
theorem _root_.List.Subset.dedup_append_left {s t : List α} (h : t ⊆ s) : List.dedup (s ++ t) ~ List.dedup s := by
  rw [← coe_eq_coe, ← coe_dedup, ← coe_add, Subset.dedup_add_left h, coe_dedup]

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