Restricting an additive Haar measure to the whole space #
Restricting a measure to the top open set ⊤ : Opens G gives back the measure, but instance search
does not see through the coercion of ⊤ to Set.univ. Function spaces on an open set Ω, such as
test functions and Sobolev spaces, use the restricted measure μ.restrict Ω; the instance
TauCeti.instIsAddHaarMeasureRestrictTop lets their whole-space versions use the Haar measure API.
instance
TauCeti.instIsAddHaarMeasureRestrictTop
{G : Type u_1}
[MeasurableSpace G]
[TopologicalSpace G]
[AddGroup G]
{μ : MeasureTheory.Measure G}
[μ.IsAddHaarMeasure]
:
(μ.restrict ↑⊤).IsAddHaarMeasure
The whole-space restriction of an additive Haar measure is an additive Haar measure.