Commit 2024-11-12 06:14 2364e40b

View on Github →

chore(Order/InitialSeg): fix simp lemmas (#17602) See Zulip.

Estimated changes

Modified Mathlib/Order/InitialSeg.lean

modified theorem PrincipalSeg.apply_subrelIso

modified def PrincipalSeg.ofElement

deleted theorem PrincipalSeg.ofElement_top

Modified Mathlib/Order/RelIso/Set.lean