Zulip Chat Archive

Stream: new members

Topic: Question about `classical.some`


view this post on Zulip Pedro Minicz (Aug 12 2020 at 17:26):

Do we have that classical.some (Exists.intro x hx) = x?

variables {x : } (hx : x = 1)

set_option pp.proofs true

example : classical.some (Exists.intro x hx) = x :=
sorry

example : classical.some (Exists.intro x hx) = 1 :=
sorry

view this post on Zulip Reid Barton (Aug 12 2020 at 17:32):

No, certainly not

view this post on Zulip Reid Barton (Aug 12 2020 at 17:33):

because Exists.intro x hx = Exists.intro x' hx' even if x and x' are different


Last updated: May 13 2021 at 06:15 UTC