Stream: new members
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):
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 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 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
Last updated: May 14 2021 at 06:16 UTC