Set theory

Stream: new members

[Frédéric Le Roux]

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

[Johan Commelin]

There are lots of ways.

[Johan Commelin]

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

[Johan Commelin]

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

[Johan Commelin]

3) Use ordinary system tools, like git grep.

[Johan Commelin]

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

[Johan Commelin]

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

[Patrick Massot]

import data.set

open set

example (α : Type) (s : set (set α)) : ∀ t : set α, t ∈ s →  t ⊆ sUnion s :=
begin
  library_search,
end

[Frédéric Le Roux]

Great, thanks!