Commit 2024-10-10 07:55 f7673a18

View on Github →

chore(Order/InitialSeg): topLTtop → top_rel_top (#17608)

Estimated changes

Modified Mathlib/Order/InitialSeg.lean

deleted theorem PrincipalSeg.topLTTop

added theorem PrincipalSeg.top_rel_top