mathlib
e9ce88cd - feat(order/upper_lower/basic): The upper closure is bounded below (#18637)

Commit
2 years ago
feat(order/upper_lower/basic): The upper closure is bounded below (#18637) and its lower bounds are the same as those of the original set.
Author
Parents
Loading