Theorem Besicovitch.tendsto_filterAt

Modification history

2024-07-12 22:59

Mathlib/MeasureTheory/Covering/Besicovitch.lean

feat(Decomposition/Lebesgue): `SigmaFinite -> SFinite` (#14658) …

Modified Besicovitch.tendsto_filterAt View on Github →

2023-06-07 15:05

Mathlib/MeasureTheory/Covering/Besicovitch.lean

feat: port MeasureTheory.Covering.Besicovitch (#4794)

Added Besicovitch.tendsto_filterAt View on Github →