Theorem List.orderedInsert_erase

Modification history

2026-01-07 07:34

Mathlib/Data/List/Sort.lean

chore(Order/Defs/Unbundled): deprecate `IsAntisymm` in favor of core's `Std.Antisymm` (#33685)

Modified List.orderedInsert_erase View on Github →

2024-03-07 21:56

Mathlib/Data/List/Sort.lean

feat: results about `List.orderedInsert` (#11191) …

Added List.orderedInsert_erase View on Github →