mathlib
fc75aea8 - feat(topology/algebra/ordered): `{prod,pi}.order_closed_topology` (#9073)

Commit

4 years ago

feat(topology/algebra/ordered): `{prod,pi}.order_closed_topology` (#9073)

Author

urkud

urkud

Parents

Loading