Theorem PrincipalSeg.isSuccPrelimit_apply_iff

Modification history

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