mathlib3

9f796b5a - feat(measure_theory): define Borel hiearchy and reprove cardinality bound on σ-algebras

feat(measure_theory): define Borel hiearchy and reprove cardinality bound on σ-algebras I give an inductive definition of the Borel hierarchy (as suggested by Junyan Xu) and I provide a basic API. This file serves as a refactor of `measure_theory.card_measurable_space` since all the relevant results are proved using this engineering.