Commit 2024-10-10 10:38 058869fd

View on Github →

chore(Order/InitialSeg): small cleanup (#17607) We rewrap a few lines and replace simp only by rw.

Estimated changes

Modified Mathlib/Order/InitialSeg.lean

modified theorem InitialSeg.ltOrEq_apply_left

modified theorem InitialSeg.ltOrEq_apply_right

modified def PrincipalSeg.ltEquiv