## Stream: general

### Topic: Newb question / not-true example in TPIL?

#### Ben Weinstein-Raun (Jun 04 2018 at 03:27):

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 (Jun 04 2018 at 03:29):

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

#### Simon Hudon (Jun 04 2018 at 03:29):

that's the right place to come

#### Simon Hudon (Jun 04 2018 at 03:31):

I think you may be right

#### Simon Hudon (Jun 04 2018 at 03:33):

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 (Jun 04 2018 at 03:35):

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

#### Ben Weinstein-Raun (Jun 04 2018 at 03:35):

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 (Jun 04 2018 at 03:35):

ah, yeah, sorry about that

No worries

(also, thanks!)

#### Simon Hudon (Jun 04 2018 at 03:39):

:smile: :thumbs_up:

Last updated: May 13 2021 at 06:15 UTC