Zulip Chat Archive

Stream: new members

Topic: Applying a function to both sides of an equation

Tung Tran (Dec 08 2021 at 05:32):

I'm looking for a lemma that can do the following: ?a=?b?f?a=?f?b?a = ?b \to ?f ?a = ?f ?b. Is there such a lemma or do we have to go around the problem? Thanks in advance!

Andrew Yang (Dec 08 2021 at 05:46):

Its docs#congr_arg .

Andrew Yang (Dec 08 2021 at 05:48):

This also gives you the answer

example (α β) (f : α  β) (x : α) (y = x) : f y = f x := by library_search

Last updated: Dec 20 2023 at 11:08 UTC