mul_iff_right — Mathlib

English

If f is almost everywhere measurable, then f·g is a.e.-measurable iff g is a.e.-measurable.

Русский

Если f измерима почти всюду, то f·g измеримо почти всюду тогда и только тогда, когда g измеримо почти всюду.

LaTeX

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

Lean4

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

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