Countable union

Stream: new members

[Brandon Brown]

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]

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

[Reid Barton]

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

[Brandon Brown]

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]

#print notation ⋃

[Brandon Brown]

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

[Jalex Stark]

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

[Jalex Stark]

#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]

⋃ 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]

thank you both, I got it now

[Brandon Brown]

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]

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

[Brandon Brown]

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]

I think you have an older mathlib/Lean

[Reid Barton]

It used to be -s

[Brandon Brown]

oh must be right, -s works

[Brandon Brown]

thanks

[Kevin Buzzard]

Then you should upgrade

[Brandon Brown]

I did! All is working now