Singleton images under an injective function

Mirror of Mathlib/Data/Set/Image.lean: the image of a set under an injective function is a singleton iff the set is, the singleton rung beside Function.Injective.subsingleton_image_iff. [UPSTREAM]

theorem Function.Injective.exists_image_eq_singleton_iff {α : Type u_1} {β : Type u_2} {f : α → β} (hf : Injective f) {s : Set α} : (∃ (b : β), f '' s = {b}) ↔ ∃ (a : α), s = {a}

The image of a set under an injective function is a singleton iff the set is. [UPSTREAM]