Mathlib v3 is deprecated. Go to Mathlib v4

Theorem vitali_family.ae_eventually_measure_zero_of_singular

Modification history

2023-02-12 08:45

src/measure_theory/covering/differentiation.lean

refactor(measure_theory/measure/mutually_singular): use ⟂ PERPENDICULAR instead of ⊥ UP TACK (#18423) …

Modified vitali_family.ae_eventually_measure_zero_of_singular View on Github →

2021-11-21 21:47

src/measure_theory/covering/differentiation.lean

feat(measure_theory/covering/differentiation): differentiation of measures (#10101) …

Added vitali_family.ae_eventually_measure_zero_of_singular View on Github →