Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-01-25 10:49 494f7199

View on Github →

feat(data/fun_like): define embedding_like and equiv_like (#10759) These extend fun_like with a proof of injectivity resp. an inverse. The number of new generic lemmas is quite low at the moment, so their use is more in defining derived classes such as mul_equiv_class.

Estimated changes

modified theorem equiv.apply_eq_iff_eq
modified theorem equiv.bijective_comp
modified theorem equiv.coe_fn_injective
modified theorem equiv.comp_bijective
modified theorem equiv.comp_injective
modified theorem equiv.comp_surjective
modified theorem equiv.ext
modified theorem equiv.ext_iff
modified theorem equiv.injective_comp
modified theorem equiv.surjective_comp
added structure cooler_embedding
added theorem do_something
added theorem map_cool
added theorem map_op
added structure cooler_iso
added theorem do_something
added theorem map_cool
modified theorem function.embedding.ext
modified theorem function.embedding.ext_iff