Mathlib v3 is deprecated. Go to Mathlib v4

Theorem clopen_upper_set.coe_top

Modification history

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