Theorem PrincipalSeg.isLowerSet_range

Modification history

2025-03-05 06:23
Mathlib/Order/InitialSeg.lean
feat: generalize order typeclasses (#22569) …
Modified PrincipalSeg.isLowerSet_rangeView on Github →
2024-11-03 19:54
Mathlib/Order/InitialSeg.lean
feat(Order/InitialSeg): extra lemmas on `α ≤i β` (#17632)
Added PrincipalSeg.isLowerSet_rangeView on Github →