Zulip Chat Archive

Stream: new members

Topic: exists element in nonempty set


view this post on Zulip Lucas V. (May 20 2020 at 22:18):

I feel this is very simple, but library_search is not helping me:

lemma exists_element (a : set α) : ¬(a = )  x, x  a :=
    by library_search

It fails :(
Is there something like this in the library? Or am I missing something?

(side question: does library_search also search in the default libraries?)

view this post on Zulip Alex J. Best (May 20 2020 at 22:22):

I'm not sure why library search doesn't find this: set.ne_empty_iff_nonempty.mp, maybe because the way the library writes the right hand side is just a.nonempty now.

view this post on Zulip Lucas V. (May 20 2020 at 22:30):

If I write a.nonempty it actually suggests using nmem_singleton_empty.mp

view this post on Zulip Alex J. Best (May 20 2020 at 22:33):

Yeah I saw that, library search doesn't always find the perfect answer, if you do by suggest instead the second suggestion is better here.

view this post on Zulip Lucas V. (May 20 2020 at 22:34):

Uuh, didn't know about suggest, thank you :)

view this post on Zulip Kevin Buzzard (May 20 2020 at 22:47):

The canonical way of writing aa\not=\emptyset in Lean is a.nonempty(maybe set.nonempty(a) looks better for mathematicians?), so the library lemmas will be stated in this form.


Last updated: May 15 2021 at 00:39 UTC