Commit 2024-08-04 11:42 b29f5cc9

View on Github →

chore(VitaliFamily): rename α → X (#15428) The module docstring uses X while the code used α.

Estimated changes

Modified Mathlib/MeasureTheory/Covering/VitaliFamily.lean

modified theorem Filter.HasBasis.vitaliFamily

modified theorem VitaliFamily.FineSubfamilyOn.covering_mem

modified theorem VitaliFamily.FineSubfamilyOn.covering_mem_family

modified theorem VitaliFamily.FineSubfamilyOn.index_countable

modified theorem VitaliFamily.FineSubfamilyOn.index_subset

modified theorem VitaliFamily.FineSubfamilyOn.measure_le_tsum

modified theorem VitaliFamily.FineSubfamilyOn.measure_le_tsum_of_absolutelyContinuous

modified def VitaliFamily.FineSubfamilyOn

modified theorem VitaliFamily.eventually_filterAt_iff

modified theorem VitaliFamily.eventually_filterAt_measurableSet

modified theorem VitaliFamily.eventually_filterAt_mem_setsAt

modified theorem VitaliFamily.eventually_filterAt_subset_closedBall

modified theorem VitaliFamily.eventually_filterAt_subset_of_nhds

modified def VitaliFamily.filterAt

modified theorem VitaliFamily.filterAt_basis_closedBall

modified theorem VitaliFamily.fineSubfamilyOn_of_frequently

modified theorem VitaliFamily.frequently_filterAt_iff

modified theorem VitaliFamily.mem_filterAt_iff

modified def VitaliFamily.mono

modified theorem VitaliFamily.tendsto_filterAt_iff

modified structure VitaliFamily