Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] THE-operator


view this post on Zulip Email Gateway (Aug 19 2022 at 11:13):

From: "Roger H." <s57076@hotmail.com>
Hello,

i would like to prove the following:

( THE A. {a. f a = {c1, c2, c3}} = {a. f a = A} ) = {c1, c2, c3}

It may well be a 1 line proof but unfortunately im unfamiliar with substitution on THE-operator).

Many thanks!

view this post on Zulip Email Gateway (Aug 19 2022 at 11:13):

From: Lars Noschinski <noschinl@in.tum.de>
As you were already told on the -dev list, this theorem does not hold.
Please read the answers you get.

-- Lars


Last updated: Mar 28 2024 at 12:29 UTC