Mathlib v3 is deprecated. Go to Mathlib v4

Theorem is_clopen_discrete

Modification history

2021-08-03 20:19
src/topology/subset_properties.lean
feat(topology/discrete_quotient): add two lemmas (#8464) …
Added is_clopen_discreteView on Github →