Commit 2024-09-24 07:14 ac554e73

View on Github →

chore(Order/InitialSeg): init → mem_range_of_rel (#16994) We rename some init theorems that had very vague names beforehand, and we state them in terms of (the definitionally equal) Set.range.

Estimated changes

Modified Mathlib/Order/InitialSeg.lean

added theorem InitialSeg.exists_eq_iff_rel

deleted theorem InitialSeg.init

deleted theorem InitialSeg.init_iff

added theorem InitialSeg.mem_range_of_rel

added theorem PrincipalSeg.exists_eq_iff_rel

deleted theorem PrincipalSeg.init

deleted theorem PrincipalSeg.init_iff

added theorem PrincipalSeg.mem_range_of_rel

Modified Mathlib/SetTheory/Ordinal/Arithmetic.lean

Modified Mathlib/SetTheory/Ordinal/Basic.lean