dedup — Mathlib

English

Dedup preserves permutation: if l1 ~ l2 then dedup(l1) ~ dedup(l2).

Русский

Dedup сохраняет перестановку: если l1 ~ l2, то dedup(l1) ~ dedup(l2).

LaTeX

$$$l_1 \\sim l_2 \\Rightarrow \\mathrm{dedup}(l_1) \\sim \\mathrm{dedup}(l_2)$$$

Lean4

theorem dedup {l₁ l₂ : List α} (p : l₁ ~ l₂) : dedup l₁ ~ dedup l₂ :=
  perm_iff_count.2 fun a =>
    if h : a ∈ l₁ then by simp [h, nodup_dedup, p.subset h] else by simp [h, count_eq_zero_of_not_mem, mt p.mem_iff.2]

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