replicate_dedup — Mathlib

English

If k ≠ 0, then replicate(k, x).dedup = [x] for any x.

Русский

Если k ≠ 0, то replicate(k, x).dedup = [x] для любого x.

LaTeX

$$$\\forall x\\in \\alpha,\\ \\forall k \\, (k \\neq 0)\\Rightarrow \\mathrm{dedup}(\\mathrm{replicate}(k,x)) = [x]$$$

Lean4

theorem replicate_dedup {x : α} : ∀ {k}, k ≠ 0 → (replicate k x).dedup = [x]
  | 0, h => (h rfl).elim
  | 1, _ => rfl
  | n + 2, _ => by
    rw [replicate_succ, dedup_cons_of_mem (mem_replicate.2 ⟨n.succ_ne_zero, rfl⟩), replicate_dedup n.succ_ne_zero]

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