Commit 2025-11-04 23:41 10db0083
View on Github →feat: uniqueness of measures in the Riesz–Markov–Kakutani representation theorem (#28061) This PR adds the proof of the uniqueness of measures in the Riesz–Markov–Kakutani representation theorem (i.e. if two regular measures on a locally compact Hausdorff space induce the same linear functionals on the set of compactly supported continuous functions, then these two measures are equal). cf. https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Uniqueness.20in.20Riesz.E2.80.93Markov.E2.80.93Kakutani.20representation.20theorem