Commit 2024-01-22 13:53 585f7a48

View on Github →

refactor(MeasureTheory/Covering): redefine filterAt using smallSets (#9852)

Estimated changes

Modified Mathlib/MeasureTheory/Covering/Differentiation.lean

Modified Mathlib/MeasureTheory/Covering/VitaliFamily.lean

added theorem Filter.HasBasis.vitaliFamily

deleted theorem VitaliFamily.eventually_filterAt_mem_sets

added theorem VitaliFamily.eventually_filterAt_mem_setsAt

modified def VitaliFamily.filterAt

added theorem VitaliFamily.filterAt_basis_closedBall