# Borel sigma algebras on (pseudo-)metric spaces #

## Main statements #

`measurable_dist`

,`measurable_infEdist`

,`measurable_norm`

,`Measurable.dist`

,`Measurable.infEdist`

,`Measurable.norm`

: measurability of various metric-related notions;`tendsto_measure_thickening_of_isClosed`

: the measure of a closed set is the limit of the measure of its ε-thickenings as ε → 0.`exists_borelSpace_of_countablyGenerated_of_separatesPoints`

: if a measurable space is countably generated and separates points, it arises as the Borel sets of some second countable separable metrizable topology.

If a set has a closed thickening with finite measure, then the measure of its `r`

-closed
thickenings converges to the measure of its closure as `r`

tends to `0`

.

If a closed set has a closed thickening with finite measure, then the measure of its closed
`r`

-thickenings converge to its measure as `r`

tends to `0`

.

If a set has a thickening with finite measure, then the measures of its `r`

-thickenings
converge to the measure of its closure as `r > 0`

tends to `0`

.

If a closed set has a thickening with finite measure, then the measure of its
`r`

-thickenings converge to its measure as `r > 0`

tends to `0`

.

Given a compact set in a proper space, the measure of its `r`

-closed thickenings converges to
its measure as `r`

tends to `0`

.

If a measurable space is countably generated and separates points, it arises as the borel sets of some second countable t4 topology (i.e. a separable metrizable one).

If a measurable space on `α`

is countably generated and separates points, there is some
second countable t4 topology on `α`

(i.e. a separable metrizable one) for which every
open set is measurable.