## 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 $a\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