Commit 2023-11-08 23:58 049141bc

feat: new class InnerRegular of measures (#8251) Towards general uniqueness results for the Haar measure, we introduce a new class of regular measures called InnerRegular, for measures which are inner regular with respect to compact sets. We also introduce InnerRegularWRT for more general classes of inner regular measures with properties to be prescribed, and InnerRegularCompactLTTop for measures which are regular for finite measure sets with respect to compact sets -- the latter property is the common denominator to the two main classes of Haar measures, the regular ones and the inner regular ones.