Theorems · Theorem · combinatorics

List.Pairwise.destutter_eq_dedup

∀ {α : Type u_1} [inst : DecidableEq α] {r : α → α → Prop} [Std.Antisymm r] {l : List α},
  List.Pairwise r l → List.destutter (fun x1 x2 => x1 ≠ x2) l = l.dedup

If the elements of a list l are related pairwise by an antisymmetric relation r, then destuttering l by disequality produces the same result as deduplicating l. This is most useful when r is a strict or weak ordering.

Defined in

Mathlib.Data.List.Destutter

Cited by

0 results in Mathlib

Foundations

Depth 22 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

DecidableEqStd.Antisymm