comap — Mathlib

English

The comap of a Haar measure under an open embedding is Haar.

Русский

Обратная композиция меры Хаара по открытого вложения тоже является мерой Хаара.

LaTeX

$$$\text{IsHaarMeasure}(\mu\text{.comap } f)$$$

Lean4

protected theorem comap [BorelSpace G] [MeasurableMul G] [Group H] [TopologicalSpace H] [BorelSpace H]
    {mH : MeasurableMul H} (μ : Measure H) [IsHaarMeasure μ] {f : G →* H} (hf : Topology.IsOpenEmbedding f) :
    (μ.comap f).IsHaarMeasure
    where
  map_mul_left_eq_self := (IsMulLeftInvariant.comap μ hf.measurableEmbedding).map_mul_left_eq_self
  lt_top_of_isCompact := (IsFiniteMeasureOnCompacts.comap' μ hf.continuous hf.measurableEmbedding).lt_top_of_isCompact
  open_pos := (IsOpenPosMeasure.comap μ hf).open_pos

Похожие утверждения