Field of sets

Stream: Is there code for X?

[Etienne Marion]

Hello, is there a way of manipulating fields of sets? In the sense defined here: https://en.wikipedia.org/wiki/Field_of_sets
In particular the field generated by some collection of subsets.

[Matt Diamond]

if we don't have it, I'm sure you could define something similar to the way we define docs#MeasurableSpace but with the countable union condition replaced with binary unions

[Etienne Marion]

All right thanks, I thought I would do that.
It’s just that I need a property (the field generated by a countable family is countable) and I didn’t think a lot about it but it seems to be painful :sweat_smile:

[Etienne Marion]

Also, should it be defined as a Set X → Prop function like in docs#MeasurableSpace or rather as a Set (Set X) like in docs#Filter for example? I don't really get what are the advantages and drawbacks of these two methods.

[Rémy Degenne]

We have rings of sets (= field that may not contain univ if I recall correctly) here: docs#MeasureTheory.IsSetRing
This is a recent addition and there is almost nothing about them.

[Etienne Marion]

Oh thanks! Indeed there's a lot to add

[Rémy Degenne]

I am planning to add a bit more about them because I have material about Caratheodory's and Kolmogorov's extension theorems that I want to PR (and IsSetSemiring and IsSetRing were added for that use)... but that progress has stalled for now.

[Etienne Marion]

I see, indeed it would be interesting to have those!

[Junyan Xu]

It’s just that I need a property (the field generated by a countable family is countable) and I didn’t think a lot about it but it seems to be painful :sweat_smile:

I think you can mimic the proof using W-types in this file which is for subfields of a field or division ring (the algebraic structure). Alternatively you can convert the problem to one about Boolean algebras, where we have docs#Algebra.adjoin_eq_range and docs#MvPolynomial.cardinal_mk_eq_max.

[Etienne Marion]

All right thank you, I'll look that up.