## Stream: new members

### Topic: reasoning about empty set in lean

#### Marcus Klaas (Dec 02 2018 at 17:09):

Hi y'all. Sorry to bother again. I'm having trouble working with the empty set. Specifically, I'd like to prove that a set is not empty whenever I can produce a concrete element of it:

example : { x | x = nat.succ nat.zero } ≠ ∅ := sorry


but so far, I haven't been successful. What can I do here?

#### Rob Lewis (Dec 02 2018 at 17:10):

set.ne_empty_of_mem will probably be helpful!

#### Rob Lewis (Dec 02 2018 at 17:10):

You'll have to import data.set.basic from mathlib.

#### Marcus Klaas (Dec 02 2018 at 17:10):

Thanks! I will try it.

#### Kenny Lau (Dec 02 2018 at 17:12):

no import needed :)

example : { x | x = nat.succ nat.zero } ≠ ∅ :=
λ H, (congr_fun H 1).mp rfl


#### Kevin Buzzard (Dec 02 2018 at 17:13):

...says the person with over 1 year's Lean experience ;-)

#### Kevin Buzzard (Dec 02 2018 at 17:13):

import data.set.basic

example : { x | x = nat.succ nat.zero } ≠ ∅ :=
begin
rw set.ne_empty_iff_exists_mem,
use 1,
exact rfl, -- refl doesn't work!
end


#### Kevin Buzzard (Dec 02 2018 at 17:14):

refl is really bad at set membership.

#### Kevin Buzzard (Dec 02 2018 at 17:15):

example (a : ℕ) : a ∈ {x : ℕ | x = a} := by refl -- fails

#### Reid Barton (Dec 02 2018 at 17:15):

I wonder whether we could fool it into working somehow

#### Marcus Klaas (Dec 02 2018 at 17:15):

Hmmm I don't seem to have the mathlib tho.. can I install it using elan? I have found a way to do it ^^

#### Reid Barton (Dec 02 2018 at 17:15):

basically by adding what Kevin just wrote as a relfexivity lemma

#### Kevin Buzzard (Dec 02 2018 at 17:17):

@Marcus Klaas mathlib is great. It's not just for mathematicians. It has a bunch of useful tactics in, and a whole host of useful data structures. If you work with Lean projects (as I do -- all my files, even scratch files, are within a Lean project) then you can just make mathlib a dependency for that project and then leanpkg upgrade will download mathlib.

Last updated: May 12 2021 at 04:19 UTC