mathlib3
177020e4 - feat(topology/separation): `(closure s).subsingleton ↔ s.subsingleton` (#6707)

Commit

4 years ago

feat(topology/separation): `(closure s).subsingleton ↔ s.subsingleton` (#6707) Also migrate `set.subsingleton_of_image` to `set.subsingleton`.

Author

urkud

Parents