mathlib3
9ec2778f - chore(data/{equiv,set}/basic): image_preimage (#5465)

Commit
5 years ago
chore(data/{equiv,set}/basic): image_preimage (#5465) * `equiv.symm_image_image`: add `@[simp]`; * `equiv.image_preimage`, `equiv.preimage_image`: new `simp` lemmas; * `set.image_preimage_eq`, `set.preimage_image_eq`: make `s : set _` an explicit argument; * `function.injective.preimage_image`, `function.surjective.image_preimage`: new aliases for `set.preimage_image_eq` and `set.image_preimage_eq` with arguments reversed Also golf a proof about `separated`.
Author
Parents
Loading