Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-08-10 00:22 f838fe85

View on Github →

feat(order/initial_seg): is_empty (r ≺i r) (#15803)

Estimated changes

modified theorem principal_seg.irrefl