Finset powerset is measurable

Stream: new members

[Iocta]

I'm looking at

https://leanprover-community.github.io/mathlib4_docs/Mathlib/MeasureTheory/MeasurableSpace/Basic.html
https://leanprover-community.github.io/mathlib4_docs/Mathlib/Data/Finset/Powerset.html

I want to say some basic stuff like {{}, {1}, {2}, {1,2}} for {1,2} is measurable and generally the powerset of a finite set is measurable. But idk how to even state them.

application type mismatch
  MeasurableSet (Finset.powerset (Finset.range 3))
argument
  Finset.powerset (Finset.range 3)
has type
  Finset (Finset ℕ) : Type
but is expected to have type
  Set ?m.12 : Type

[Josha Dekker]

Whether every set in the power set is measurable depends on the sigma algebra that you pick. This is not true in general, consider the trivial sigma algebra for sets with 2 or more elements.

[Iocta]

If s = {1,2}, the trivial sigma algebra is b = {{}, {1,2}}: complement {} = {1,2} which is in b and complement {1,2} = {} which is in b. union {} {1,2} = {1,2} which is in b. So it's closed under complementation and union. In the docs we have

A measurable space is a set equipped with a σ-algebra, a collection of subsets closed under complementation and countable union.

which I think we've satisfied. What am I missing?

[Josha Dekker]

My point was that any finite set with at least two elements admits at least two sigma algebras: one in which every element in the power set is measurable, and one in which only the empty set and the full set are measurable. As such, I guess you’d need to specify which sigma algebra you want to use? Perhaps there is a default one on a finite set. So my point was that the sets that you wanted to show are measurable, are only measurable for one sigma algebra, and not for the other.

[Josha Dekker]

So you may want to determine first what the default sigma algebra is on a finite set (if there is one), and if that is the one for which you want to state this.

[Matt Diamond]

there's also the issue that you're passing in a Finset instead of a Set... that's the immediate cause of the error

[Matt Diamond]

MeasurableSet (Set.powerset {0, 1, 2}) typechecks just fine

[Matt Diamond]

or you could do MeasurableSet (Set.powerset { n | n < 3 })