## Stream: new members

### Topic: Confused with double "exists"

#### Walter Moreira (May 07 2020 at 01:50):

I'm going over the tutorial proposed by @Patrick Massot . I'm confused about what it means the double "exists" in a judgement like

key : ∀ (n : ℕ), ∃ (a : ℝ) (H : a ∈ A), a < x + 1 / (↑n + 1)


How does that notation translates into bare Exists? Is it a way to ask Lean to display the unfolding of the definition?

#### Reid Barton (May 07 2020 at 02:05):

It means

key : ∀ (n : ℕ), ∃ (a : ℝ), ∃ (H : a ∈ A), a < x + 1 / (↑n + 1)


#### Walter Moreira (May 07 2020 at 02:27):

Thank you @Reid Barton That's what I was expecting. I got confused about it with the application of choose u hu using key which added

hu : ∀ (n : ℕ), u n ∈ A ∧ u n < x + 1 / (↑n + 1)


and I couldn't see how Lean was generating the $\wedge$ in that clause. It seems that it becomes more clear when doing choose u v hu which generates two functions.

I guess that Lean automatically combines them with $\wedge$ if I provide only one variable?

#### Reid Barton (May 07 2020 at 02:29):

I think the choose tactic has some specific magic to get rid of unnecessary ∃ (in the sense that the variable, here H, is not used) and turn them into ∧.

#### Patrick Massot (May 07 2020 at 08:00):

This is very similar to what is explained at https://github.com/leanprover-community/tutorials/blob/a1b5620e098deb0c06c902b1151b02aca5f46033/src/exercises/06_sub_sequences.lean#L67-L73 but I should probably repeat that comment. Also, you can ask Lean to rewrite this abbreviation using rw exists_prop.

Last updated: May 14 2021 at 06:16 UTC