Commit 2024-11-29 04:10 a3890372

View on Github →

feat(Order/InitialSeg): initial segments preserve successor limits (#19053) Initial segments preserve the covering relation, successors, and successor limits.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Order/InitialSeg.lean

added theorem InitialSeg.isMin_apply_iff

deleted theorem InitialSeg.map_isMin

added theorem PrincipalSeg.isMin_apply_iff

deleted theorem PrincipalSeg.map_isMin

Modified Mathlib/Order/SuccPred/Basic.lean

modified theorem OrderIso.map_succ

Created Mathlib/Order/SuccPred/InitialSeg.lean

added theorem InitialSeg.apply_covBy_apply_iff

added theorem InitialSeg.apply_wCovBy_apply_iff

added theorem InitialSeg.isSuccLimit_apply_iff

added theorem InitialSeg.isSuccPrelimit_apply_iff

added theorem InitialSeg.map_pred

added theorem InitialSeg.map_succ

added theorem PrincipalSeg.apply_covBy_apply_iff

added theorem PrincipalSeg.apply_wCovBy_apply_iff

added theorem PrincipalSeg.isSuccLimit_apply_iff

added theorem PrincipalSeg.isSuccPrelimit_apply_iff

added theorem PrincipalSeg.map_pred

added theorem PrincipalSeg.map_succ