Def PrincipalSeg.ltEquiv

Modification history

2024-11-14 00:39

Mathlib/Order/InitialSeg.lean

chore(Order/InitialSeg): rename various defs (#17989) …

Deleted PrincipalSeg.ltEquiv View on Github →

2024-10-10 10:38

Mathlib/Order/InitialSeg.lean

chore(Order/InitialSeg): small cleanup (#17607) …

Modified PrincipalSeg.ltEquiv View on Github →

2022-12-14 23:20

Mathlib/Order/InitialSeg.lean

feat port: Order.InitialSeg (#1012) …

Added PrincipalSeg.ltEquiv View on Github →