Mathlib v3 is deprecated. Go to Mathlib v4

Theorem set.subsingleton.closure

Modification history

2021-03-16 21:43

src/topology/separation.lean

feat(topology/separation): `(closure s).subsingleton ↔ s.subsingleton` (#6707) …

Added set.subsingleton.closure View on Github →