mul_iff_left — Mathlib

English

If f is aemeasurable, then g·f is aemeasurable iff g is aemeasurable.

Русский

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

LaTeX

$$$AEMeasurable\\ f\\mu \\Rightarrow (AEMeasurable\\ (g\\cdot f)\\mu \\iff AEMeasurable\\ g\\mu)$$$

Lean4

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

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