mathlib
mathlib copied to clipboard
Published
20 hours ago •
leanprover-community
leanprover-community
feat(logic/function/basic): refine extend_apply
Add function.extend_apply_of_unique
which allows to rewrite function.extend f g e (f a) = g a
not only when f is injective, what function.extend_apply does,
but when f a = f b → g a = g b.
Generalize a few similar lemmas in the same way.
TODO ? : rewrite function.extend_apply to use this function.
