Theorem InitialSeg.isLowerSet_range

Modification history

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