Topic: rewrite only right hand side
Danny Ofek (Dec 11 2021 at 00:19):
I have an equation x = f(f(x)) and a goal f(x) \leq x.
I want to replace x on the right hand side by f(f(x)) in the goal but when I attempt to use the rw command it replaces x in both sides of the inequality. Anyone knows how to do this? Spent half an hour on this already and I am quite frustrated.
David Renshaw (Dec 11 2021 at 00:23):
Eric Rodriguez (Dec 11 2021 at 00:28):
David Renshaw (Dec 11 2021 at 00:30):
ah... I was struggling to remember the name of
Danny Ofek (Dec 11 2021 at 00:35):
Couldn't get conv to work (it does not seem to affect the goal after the begin .... end environment) but the nth_rewrite worked! Thank you!
Last updated: Aug 03 2023 at 10:10 UTC