mathlib
7f450cb8 - feat(topology/sets/order): Clopen upper sets (#12670)

Commit
4 years ago
feat(topology/sets/order): Clopen upper sets (#12670) Define `clopen_upper_set`, the type of clopen upper sets of an ordered topological space.
Author
Parents
Loading