Commit 2024-11-03 19:54 8bb0ad68

View on Github →

feat(Order/InitialSeg): extra lemmas on α ≤i β (#17632)

Estimated changes

Modified Mathlib/Order/InitialSeg.lean

added theorem InitialSeg.isLowerSet_range

added theorem InitialSeg.map_bot

added theorem InitialSeg.map_isMin

added theorem PrincipalSeg.isLowerSet_range

added theorem PrincipalSeg.map_bot

added theorem PrincipalSeg.map_isMin