Newb question / not-true example in TPIL?

Stream: general

[Ben Weinstein-Raun]

Hi, I'm a total newb to Lean and to proof assistants generally. I'm working through Chapter 4 of TPIL, and in particular the example statements in 4.4. I haven't been able to prove the last two of them, and I'm beginning to suspect that the last one, at least, is actually false.

example : (∃ x : α, r → p x) ↔ (r → ∃ x : α, p x) := sorry.

If r is false and α is uninhabited, the left side of this equivalence is false while the right side is true, no?

[Ben Weinstein-Raun]

(sorry if there's a better place to ask this)

[Simon Hudon]

that's the right place to come

[Simon Hudon]

I think you may be right

[Simon Hudon]

As you say, if r is false, the statement reduces to (∃ x, true) ↔ true which is another way of saying that α is inhabited, which does not seem to be an assumption

[Simon Hudon]

Sorry, I take it back: I just saw variable a : α which means that α is inhabited

[Ben Weinstein-Raun]

oh, wait, there is a line
variable a : α
further up; I hadn't noticed this. Is that equivalent to an assumption that α is inhabited?

[Ben Weinstein-Raun]

ah, yeah, sorry about that

[Simon Hudon]

No worries

[Ben Weinstein-Raun]

(also, thanks!)

[Simon Hudon]

:smile: :thumbs_up: