mathlib3
ab6bcd63 - feat(order/upper_lower): Upper closure of a set (#15581)

Commit

3 years ago

feat(order/upper_lower): Upper closure of a set (#15581) Define the upper/lower set generated by a set. Co-authored-by: Peter Nelson

Author

YaelDillies

Parents