English
If μ is left-invariant on H and f: G →* H is a measurable embedding, then the pulled-back measure μ.comap f is left-invariant on G.
Русский
Если μ слева-инвариантна на H и f: G →* H — измеримое вложение, то вытянутый обратно по f меру μ.comap f слева-инвариантна на G.
LaTeX
$$$ (\mu \mathrm{.comap} f) \text{ IsMulLeftInvariant}$, для измеримого внедрения f.$$
Lean4
@[to_additive]
protected theorem comap {H} [Group H] {mH : MeasurableSpace H} [MeasurableMul H] (μ : Measure H) [IsMulLeftInvariant μ]
{f : G →* H} (hf : MeasurableEmbedding f) : (μ.comap f).IsMulLeftInvariant where
map_mul_left_eq_self
g := by
ext s hs
rw [map_apply (by fun_prop) hs]
repeat rw [hf.comap_apply]
have : f '' ((g * ·) ⁻¹' s) = (f g * ·) ⁻¹' (f '' s) := by
ext
constructor
· rintro ⟨y, hy, rfl⟩
exact ⟨g * y, hy, by simp⟩
· intro ⟨y, yins, hy⟩
exact ⟨g⁻¹ * y, by simp [yins], by simp [hy]⟩
rw [this, ← map_apply (by fun_prop), IsMulLeftInvariant.map_mul_left_eq_self]
exact hf.measurableSet_image.mpr hs
