Theorem PrincipalSeg.map_succ

Modification history

2024-11-29 04:10
Mathlib/Order/SuccPred/InitialSeg.lean
feat(Order/InitialSeg): initial segments preserve successor limits (#19053) …
Added PrincipalSeg.map_succView on Github →