{"id":"palomar/PALOMAR-2026-09-12-000001","url":"https://github.com/KiringYJ/mathlib4/tree/9e0a67ce31f1dbac121879a94e9e02319e273a50/Palomar/BroughtonHuff","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-09-12-000001-v1.json","repo":"https://github.com/KiringYJ/mathlib4","tags":["math.PR","msc:28A05","measure-theory","lean","sigma-algebras"],"score":0,"title":"The Broughton--Huff theorem on increasing unions of sigma-fields","trust":"high","domain":"math.PR","source":"palomar","authors":["Yi-Jing Tseng"],"reviews":0,"subject":"math.PR","summary":"A Lean formalization of the Broughton--Huff theorem that the ordinary union of a strictly increasing sequence of sigma-fields is not a sigma-field. The proof also proves the existence of a set measurable in the lattice supremum but in none of the individual sigma-fields.","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-09-12","reactions":{},"formalized":true,"formalizes":[{"title":"A Comment on Unions of Sigma-Fields","identifier":"https://doi.org/10.2307/2320022","relationship":"formalizes"}]}