The sigma algebra of countable and cocountable Sets

Stream: Is there code for X?

[Bolton Bailey]

Do we have the concept described on this page in mathlib somewhere?

[Yury G. Kudryashov]

You can define it in 1 line: .generateFrom (Set.range fun x => {x})

[Yury G. Kudryashov]

(if you don't care about defeq)

[Yury G. Kudryashov]

I haven't found it as a definition or as a part of a theorem.

[Yury G. Kudryashov]

So, if you need some API about it, then you have to prove it (possibly, by reusing theorems about generateFrom).