Mathlib v3 is deprecated. Go to Mathlib v4

Theorem is_open_compl_singleton

Modification history

2020-12-09 04:36
src/topology/separation.lean
feat(analysis/special_functions): `real.log` is infinitely smooth away from zero (#5116) …
Added is_open_compl_singletonView on Github →