Stream: new members
kana (Feb 18 2021 at 19:30):
How to move from
a = b goal to
f a = f b?
Yakov Pechersky (Feb 18 2021 at 19:37):
Do you know that
f is injective?
kana (Feb 18 2021 at 19:42):
Oh, my bad, I understood why it is not correct in the general case. Thanks
Eric Wieser (Feb 18 2021 at 20:08):
apply (_ : function.injective f) would probably do it.
Last updated: May 13 2021 at 21:12 UTC