Commit 2024-09-15 15:14 b657f45a

feat(Data/Set/Image): the image of a nontrivial set is nontrivial (#16823) Add two lemmas about the image of a nontrivial set under a function injective on that set: existing lemmas only work for globally injective functions. Also add a local variable so lemma statements can be condensed, since the variable f was used in many statements.