Theorems · Theorem · order theory

List.orderedInsert_erase

∀ {α : Type u_1} {r : α → α → Prop} [inst : DecidableRel r] [inst_1 : DecidableEq α] [Std.Antisymm r] (x : α)
  (xs : List α), x ∈ xs → List.Pairwise r xs → List.orderedInsert r x (xs.erase x) = xs

For an antisymmetric relation, erasing then inserting is the identity.

Defined in: Mathlib.Data.List.Sort
Cited by: 1 results in Mathlib
Foundations: Depth 18 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: DecidableRel DecidableEq Std.Antisymm

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites1

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

List.orderedInsertstatement and proof · cited by 23

Cited by1

Results whose statement or proof uses this declaration.

List.sublist_insertionSort'proof · cited by 1