Theorem PrincipalSeg.isMin_apply_iff

Modification history

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