# Zulip Chat Archive

## Stream: maths

### Topic: How to parse this example?

#### None proffered (Aug 07 2018 at 18:11):

How to parse this example?

#### None proffered (Aug 07 2018 at 18:11):

example : (∃ x, p x → r) ↔ (∀ x, p x) → r

#### None proffered (Aug 07 2018 at 18:11):

(deleted)

#### None proffered (Aug 07 2018 at 18:17):

Is it (1) [(∃ x, p x → r)] ↔[ (∀ x, p x) → r] for CCCC CCCC TNTN TTTT in M8/VL4; or

Is it (2) [(∃ x, p x → r) ↔ (∀ x, p x)] → r for CCCC TTTT TNTN TTTT in M8/VL4.

In either case, Eqs. 1 or 2 are not tautologous (all designated proof value of T).

#### Kevin Buzzard (Aug 07 2018 at 20:36):

variables (α : Type) (p : α → Prop) (r : Prop) example : ( (∃ x, p x → r) ↔ (∀ x, p x) → r ) = ( (∃ x, p x → r) ↔ ( (∀ x, p x) → r ) ) := rfl

Apparently it's the former: (1).

#### Mario Carneiro (Aug 08 2018 at 00:24):

@None proffered the parse is (1) as Kevin says. I don't know what "CCCC CCCC TNTN TTTT" means; what is M8/VL4? This theorem is not true when the domain of `x`

is empty. I assume you got this example from `tests/finish3.lean`

, which proves two versions of this:

variables (A : Type) (p : A → Prop) (r : Prop) example (a : A) : (∃ x, p x → r) ↔ (∀ x, p x) → r := begin safe [iff_def]; exact h a end example : (∃ x, p x → r) → (∀ x, p x) → r := by finish

So it is provable in one direction unconditionally, but the bidirectional version requires some `a : A`

, i.e. `A`

has to be nonempty.

Last updated: May 06 2021 at 17:38 UTC