Commit 2024-01-18 09:44 158d8524
View on Github →feat: construct Haar measure in locally compact non-Hausdorff groups (#9746)
The construction we have is given in T2 spaces, but it works in non-Hausdorff spaces modulo a few modifications.
For this, we introduce an ad hoc class T2OrLocallyCompactRegularSpace
, which is just enough to unify the arguments, as a replacement for the class ClosableCompactSubsetOpenSpace
(which is not strong enough). In the file Separation.lean
, we move some material that was only available on T2 spaces to this new class.
The construction is needed for a forthcoming improvement of uniqueness results for Haar measures, based on https://mathoverflow.net/questions/456670/uniqueness-of-left-invariant-borel-probability-measure-on-compact-groups.