Def MeasureTheory.Measure.sigmaFiniteSetWRT'

Modification history

2026-07-24 07:15

Mathlib/MeasureTheory/Measure/Decomposition/Exhaustion.lean

chore: add missing `noncomputable` (#41446) …

Deleted MeasureTheory.Measure.sigmaFiniteSetWRT'View on Github →

2024-08-15 14:22

Mathlib/MeasureTheory/Decomposition/Exhaustion.lean

feat(MeasureTheory): method of exhaustion (#14471) …

Added MeasureTheory.Measure.sigmaFiniteSetWRT'View on Github →