Theorem MeasureTheory.Measure.InnerRegularWRT.eq_of_innerRegularWRT_of_forall_eq

Modification history

2025-11-04 23:41
Mathlib/MeasureTheory/Measure/Regular.lean
feat: uniqueness of measures in the Riesz–Markov–Kakutani representation theorem (#28061) …
Added MeasureTheory.Measure.InnerRegularWRT.eq_of_innerRegularWRT_of_forall_eqView on Github →