mul_iff_left — Mathlib

English

If f is measurable, then the map g ↦ g·f is measurable iff g is measurable (in a commutative group with measurable multiplication).

Русский

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

LaTeX

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

Lean4

@[to_additive]
theorem mul_iff_left {G : Type*} [MeasurableSpace G] [MeasurableSpace α] [CommGroup G] [MeasurableMul₂ G]
    [MeasurableInv G] {f g : α → G} (hf : Measurable f) : Measurable (g * f) ↔ Measurable g :=
  mul_comm g f ▸ Measurable.mul_iff_right hf

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