Mathlib v3 is deprecated. Go to Mathlib v4

Def clopen_upper_set.to_upper_set

Modification history

2022-03-30 16:05
src/topology/sets/order.lean
feat(topology/sets/order): Clopen upper sets (#12670) …
Added clopen_upper_set.to_upper_setView on Github →