Theorem PrincipalSeg.map_isMin

Modification history

2024-11-29 04:10
Mathlib/Order/InitialSeg.lean
feat(Order/InitialSeg): initial segments preserve successor limits (#19053) …
Deleted PrincipalSeg.map_isMinView on Github →
2024-11-03 19:54
Mathlib/Order/InitialSeg.lean
feat(Order/InitialSeg): extra lemmas on `α ≤i β` (#17632)
Added PrincipalSeg.map_isMinView on Github →