Zulip Chat Archive

Stream: new members

Topic: Set theory


view this post on Zulip Frédéric Le Roux (Dec 06 2019 at 15:03):

Where can I search for lemmas that Lean already knows about set theory?

To be more precise, I need to know the following fact about set.sUnion :
that the union of a family of sets contains every set of the family. I was expecting to have something like set.sUnion.intro, working similarly to or.intro, but I do not know where to search for this.
(I guess I should not call this a Lemma, it should holds by definition of set.sUnion).

view this post on Zulip Johan Commelin (Dec 06 2019 at 15:06):

There are lots of ways.

view this post on Zulip Johan Commelin (Dec 06 2019 at 15:06):

1) Ask here. (Encouraged, for beginners. Don't feel bad about it.)

view this post on Zulip Johan Commelin (Dec 06 2019 at 15:06):

2) Use search in VScode. And Ctrl-Shift-P, start typing with #your_guess_of_the_name

view this post on Zulip Johan Commelin (Dec 06 2019 at 15:07):

3) Use ordinary system tools, like git grep.

view this post on Zulip Johan Commelin (Dec 06 2019 at 15:07):

4) Type your statement into Lean, and ask library_search or suggest to see if they can prove it. (These are two tactics.)

view this post on Zulip Johan Commelin (Dec 06 2019 at 15:09):

@Frédéric Le Roux For your specific lemma, I guess set.subset_sU and autocomplete shows me the rest.

view this post on Zulip Patrick Massot (Dec 06 2019 at 15:12):

import data.set

open set

example (α : Type) (s : set (set α)) :  t : set α, t  s   t  sUnion s :=
begin
  library_search,
end

view this post on Zulip Frédéric Le Roux (Dec 06 2019 at 15:20):

Great, thanks!


Last updated: May 16 2021 at 21:11 UTC