Theorem PrincipalSeg.map_bot

Modification history

2024-11-03 19:54
Mathlib/Order/InitialSeg.lean
feat(Order/InitialSeg): extra lemmas on `α ≤i β` (#17632)
Added PrincipalSeg.map_botView on Github →