mul_iff_right — Mathlib

English

If f is measurable, then the map g ↦ f·g is measurable iff g is measurable.

Русский

Если f измерим, то отображение g ↦ f·g измеримо тогда и только тогда, когда g измеримо.

LaTeX

$$$\\text{Measurable}(f) \\Rightarrow (\\text{Measurable}(f\\ast g) \\iff \\text{Measurable}(g))$$$

Lean4

@[to_additive]
theorem mul_iff_right {G : Type*} [MeasurableSpace G] [MeasurableSpace α] [CommGroup G] [MeasurableMul₂ G]
    [MeasurableInv G] {f g : α → G} (hf : Measurable f) : Measurable (f * g) ↔ Measurable g :=
  ⟨fun h ↦ show g = f * g * f⁻¹ by simp only [mul_inv_cancel_comm] ▸ h.mul hf.inv, fun h ↦ hf.mul h⟩

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