English
In a commutative group, any inner regular Haar measure is invariant under inversion.
Русский
В коммутативной группе любая внутренняя регулярная мера Хаара инвариантна относительно инверсии.
LaTeX
$$$\\forall G \\; [CommGroup G] \\; [TopologicalSpace G] \\; [IsTopologicalGroup G] \\; [MeasurableSpace G] \\; [BorelSpace G] \\; (μ : \\mathrm{Measure}(G)) \\, [\\text{IsHaarMeasure } μ] \\, [\\text{LocallyCompactSpace } G] \\, [\\text{InnerRegular } μ],\\; IsInvInvariant μ$$
Lean4
/-- A sequence of continuous functions `X → [0,1]` tending to the indicator of a closed set. -/
noncomputable def _root_.IsClosed.apprSeq : ℕ → (X →ᵇ ℝ≥0) :=
Exists.choose (HasOuterApproxClosed.exAppr F hF)