Zulip Chat Archive

Stream: new members

Topic: Countable union


view this post on Zulip 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  σ) ``` ?

view this post on Zulip 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.

view this post on Zulip Reid Barton (Aug 12 2020 at 23:30):

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

view this post on Zulip 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 ?

view this post on Zulip Jalex Stark (Aug 13 2020 at 01:59):

#print notation ⋃

view this post on Zulip Brandon Brown (Aug 13 2020 at 02:06):

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Brandon Brown (Aug 13 2020 at 02:31):

thank you both, I got it now

view this post on Zulip 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

view this post on Zulip Brandon Brown (Aug 13 2020 at 02:35):

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

view this post on Zulip 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

view this post on Zulip Reid Barton (Aug 13 2020 at 02:41):

I think you have an older mathlib/Lean

view this post on Zulip Reid Barton (Aug 13 2020 at 02:41):

It used to be -s

view this post on Zulip Brandon Brown (Aug 13 2020 at 02:42):

oh must be right, -s works

view this post on Zulip Brandon Brown (Aug 13 2020 at 02:42):

thanks

view this post on Zulip Kevin Buzzard (Aug 13 2020 at 07:15):

Then you should upgrade

view this post on Zulip Brandon Brown (Aug 13 2020 at 14:10):

I did! All is working now


Last updated: May 17 2021 at 22:15 UTC