Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-03-16 21:43 177020e4

View on Github →

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

Estimated changes

Modified src/data/set/basic.lean

added theorem function.injective.subsingleton_image_iff

modified theorem set.subsingleton_empty

modified theorem set.subsingleton_singleton

Modified src/topology/separation.lean

added theorem set.subsingleton.closure

added theorem subsingleton_closure