Def InitialSeg.codRestrict

Modification history

2025-01-15 15:41

Mathlib/Order/InitialSeg.lean

refactor: redefine `Subrel` in terms of `α → Prop` instead of `Set α` (#20475) …

Modified InitialSeg.codRestrict View on Github →

2022-12-14 23:20

Mathlib/Order/InitialSeg.lean

feat port: Order.InitialSeg (#1012) …

Added InitialSeg.codRestrict View on Github →