Email Gateway (Aug 19 2022 at 13:32): Email Gateway (Aug 19 2022 at 13:32):From: "Roger H." <s57076@hotmail.com>
Hi,
how can i prove
"the (f a) = b ⟶ ((f |` (- {a}))(a ↦ b)) = f"
Thank you!
Email Gateway (Aug 19 2022 at 13:33):From: John Wickerson <johnwickerson@cantab.net>
I don't think you can. The fact that "the (f a)" is equal to "b" does not mean that "a" is in the domain of "f". Isabelle functions are always total, even "the". So the fact that "the (f a)" is equal to something doesn't actually tell you anything.
What you might have more luck with is this:
"f a = Some b ⟶ ((f |` (- {a}))(a ↦ b)) = f"
John
Email Gateway (Aug 19 2022 at 13:33):From: "Roger H." <s57076@hotmail.com>
Hi,
thank you, but i dont know how to prove this either :-)
"f a = Some b ⟶ ((f |` (- {a}))(a ↦ b)) = f"Can you help me?
Email Gateway (Aug 19 2022 at 13:33):From: "Roger H." <s57076@hotmail.com>
Nevermind
i used sledgehammer and got it.
Thank you anyway
Last updated: Apr 26 2024 at 08:19 UTC