## Stream: new members

### Topic: Countable union

#### Brandon Brown (Aug 12 2020 at 23:11):

I'm trying to re-create a measurable space. In looking at the mathlib definition, the structure field for closed under countable unions is encoded like this lean
∀ f : ℕ → set α, (∀ i : ℕ, is_measurable (f i)) → is_measurable (⋃i, f i))

This doesn't look anything like the "on paper" way of describing closed under countable unions.. just to check my understanding, is the space of functions f : ℕ → set α acting as an indexed set of subsets? Can I also just use  ( closed_unions : ∀ f : ℕ → set α, set.Union f ∈ σ)  ?


#### Scott Morrison (Aug 12 2020 at 23:16):

Your alternative doesn't make (mathematical) sense, as it doesn't have any hypothesis about the measurability of the sets f i.

#### Reid Barton (Aug 12 2020 at 23:30):

(You can fix the formatting of your message by adding a newline before the triple backticks)

#### Brandon Brown (Aug 13 2020 at 01:53):

Ok I see ⋃ i, f i  is like what we'd do on paper but now I don't understand what is going on in lean. Is it just an alias for set.Union ?

#### Jalex Stark (Aug 13 2020 at 01:59):

#print notation ⋃

#### Brandon Brown (Aug 13 2020 at 02:06):

⋃:1024 binders ,:0 (scoped 0) := #0

#### Jalex Stark (Aug 13 2020 at 02:09):

oh, sorry, I copied the character from your last message, which is not the same as one that's used in mathlib

#### Jalex Stark (Aug 13 2020 at 02:10):

#print notation ∪
yields
_ ∪:65 _:65 := has_union.union #1 #0
and then you might #check has_union.union or right click on that and go to definition

#### Reid Barton (Aug 13 2020 at 02:20):

⋃ i, f i is indeed notation for set.Union f. The #print notation output for notation that uses the binders feature is not very helpful, but you can use hover/jump-to-definition to see what it means.

#### Brandon Brown (Aug 13 2020 at 02:31):

thank you both, I got it now

#### Brandon Brown (Aug 13 2020 at 02:34):

Related question. Do you know how I get the complement notation to work e.g. sᶜ right now it says unexpected token so I have to do set.compl s

#### Brandon Brown (Aug 13 2020 at 02:35):

I assume I need to import something but I couldn't find it in the docs

#### Brandon Brown (Aug 13 2020 at 02:35):

import data.set.basic
import data.set.disjointed
import data.set.countable
import tactic
open set


this is what I have imported so far

#### Reid Barton (Aug 13 2020 at 02:41):

I think you have an older mathlib/Lean

#### Reid Barton (Aug 13 2020 at 02:41):

It used to be -s

#### Brandon Brown (Aug 13 2020 at 02:42):

oh must be right, -s` works

thanks