Zulip Chat Archive

Stream: new members

Topic: exists element in nonempty set


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?)

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.

Lucas V. (May 20 2020 at 22:30):

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

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.

Lucas V. (May 20 2020 at 22:34):

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

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: Dec 20 2023 at 11:08 UTC