Commit 2023-05-10 01:01 c7a6fc05

View on Github →

feat: port MeasureTheory.Covering.VitaliFamily (#3867)

Estimated changes

Modified Mathlib.lean

Created Mathlib/MeasureTheory/Covering/VitaliFamily.lean

added theorem VitaliFamily.FineSubfamilyOn.covering_disjoint

added theorem VitaliFamily.FineSubfamilyOn.covering_disjoint_subtype

added theorem VitaliFamily.FineSubfamilyOn.covering_mem

added theorem VitaliFamily.FineSubfamilyOn.covering_mem_family

added theorem VitaliFamily.FineSubfamilyOn.exists_disjoint_covering_ae

added theorem VitaliFamily.FineSubfamilyOn.index_countable

added theorem VitaliFamily.FineSubfamilyOn.index_subset

added theorem VitaliFamily.FineSubfamilyOn.measure_diff_bunionᵢ

added theorem VitaliFamily.FineSubfamilyOn.measure_le_tsum

added theorem VitaliFamily.FineSubfamilyOn.measure_le_tsum_of_absolutelyContinuous

added def VitaliFamily.FineSubfamilyOn

added def VitaliFamily.enlarge

added theorem VitaliFamily.eventually_filterAt_iff

added theorem VitaliFamily.eventually_filterAt_measurableSet

added theorem VitaliFamily.eventually_filterAt_mem_sets

added theorem VitaliFamily.eventually_filterAt_subset_closedBall

added theorem VitaliFamily.eventually_filterAt_subset_of_nhds

added def VitaliFamily.filterAt

added theorem VitaliFamily.fineSubfamilyOn_of_frequently

added theorem VitaliFamily.frequently_filterAt_iff

added theorem VitaliFamily.mem_filterAt_iff

added def VitaliFamily.mono

added theorem VitaliFamily.tendsto_filterAt_iff

added structure VitaliFamily