exists_mem_of_ne_empty

Stream: Is there code for X?

[Eric Wieser]

Can you edit your post to change the title to a new thread?

[Hunter Monroe]

This may have been eliminated--it is the contrapositive of set.eq_empty_iff_forall_not_mem.

[Mario Carneiro]

more likely it's one half of an iff

[Mario Carneiro]

docs#set.ne_empty_iff_nonempty

[Eric Wieser]

Note that s.nonempty = ∃ (x : α), x ∈ s by definition