mathlib3
3e679326 - feat(topology/algebra/ordered): an `order_closed_topology` restricted to a subset is an `order_closed_topology` (#8364)

Commit
4 years ago
feat(topology/algebra/ordered): an `order_closed_topology` restricted to a subset is an `order_closed_topology` (#8364)
Author
Parents
Loading