Commit 2022-08-16 13:24 d9992ade

feat(data/set/basic): Add natural missing lemmas to set.subsingleton and slightly refactor (#15886)

subsingleton.image is moved and documentation is added so that it is near related lemmas.
subsingleton_of_preimage is added to go with subsingleton.preimage, subsingleton_of_image., and subsingleton.image.
We add subsingleton_anti analogously to nontrivial_mono.
Some small style tweaks are made.
subsingleton.mono is renamed to subsingleton.anti.