## 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

(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