set singletons injective

Stream: Is there code for X?

[Joachim Breitner]

I can’t find a lemma for function.injective (λ (x : B), {x}). Insufficient search ability, or does that not exist for some reasons (e.g. because this is a very classical view on sets)?
(I found a different way to do my proof, so not super important.)

[Yaël Dillies]

docs#finset.singleton_injective

[Yaël Dillies]

and it seems we're missing the set version?

[Joachim Breitner]

Somehow that didn't work for me; it’s for finset and I needed set.

[Eric Wieser]

Yeah, I agree that docs#set.singleton_injective is missing. Want to PR it, @Joachim Breitner? The proof ought to be trivial

[Eric Wieser]

(note the statement is better as lemma singleton_injective : injective (singleton : α → set α) as this doesn't introduce unnecessary λ binders)

[Eric Wieser]

It belongs right before docs#set.singleton_eq_singleton_iff

[Joachim Breitner]

I’ll give it a shot later