# Results about indicator functions, their integrals, and measures #

This file has a few measure theoretic or integration-related results on indicator functions.

## Implementation notes #

This file exists to avoid importing `Mathlib.MeasureTheory.Constructions.BorelSpace.Metrizable`

in `Mathlib.MeasureTheory.Integral.Lebesgue`

.

## TODO #

The result `MeasureTheory.tendsto_measure_of_tendsto_indicator`

here could be proved without
integration, if we had convergence of measures results for countably generated filters. Ideally,
the present file would then become unnecessary: lemmas such as
`MeasureTheory.tendsto_measure_of_ae_tendsto_indicator`

would not need integration so could be
moved out of `Mathlib.MeasureTheory.Integral.Lebesgue`

, and the lemmas in this file could be
moved to, e.g., `Mathlib.MeasureTheory.Constructions.BorelSpace.Metrizable`

.

If the indicators of measurable sets `Aᵢ`

tend pointwise to the indicator of a set `A`

and we eventually have `Aᵢ ⊆ B`

for some set `B`

of finite measure, then the measures of `Aᵢ`

tend to the measure of `A`

.

If `μ`

is a finite measure and the indicators of measurable sets `Aᵢ`

tend pointwise to
the indicator of a set `A`

, then the measures `μ Aᵢ`

tend to the measure `μ A`

.