From df203bc8cd89bd676b2b3bc0db9e00f9033c235c Mon Sep 17 00:00:00 2001 From: Reid Barton Date: Fri, 29 Jul 2022 08:40:27 +0000 Subject: [PATCH] docs(measure_theory/measure/haar): Mention uniqueness in module docstring (#15740) --- src/measure_theory/measure/haar.lean | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) diff --git a/src/measure_theory/measure/haar.lean b/src/measure_theory/measure/haar.lean index b0dd4792f8e1b..7f81eef302559 100644 --- a/src/measure_theory/measure/haar.lean +++ b/src/measure_theory/measure/haar.lean @@ -9,8 +9,8 @@ import measure_theory.group.prod /-! # Haar measure -In this file we prove the existence of Haar measure for a locally compact Hausdorff topological -group. +In this file we prove the existence and uniqueness (up to scalar multiples) of Haar measure +for a locally compact Hausdorff topological group. For the construction, we follow the write-up by Jonathan Gleason, *Existence and Uniqueness of Haar Measure*. @@ -46,6 +46,8 @@ where `ᵒ` denotes the interior. it is invariant and gives finite mass to compact sets and positive mass to nonempty open sets. * `haar` : some choice of a Haar measure, on a locally compact Hausdorff group, constructed as `haar_measure K` where `K` is some arbitrary choice of a compact set with nonempty interior. +* `haar_measure_unique`: Every σ-finite left invariant measure on a locally compact Hausdorff group + is a scalar multiple of the Haar measure. ## References * Paul Halmos (1950), Measure Theory, §53