mul_iff_left — Mathlib

English

If f is AEStronglyMeasurable, then g*f is AEStronglyMeasurable iff g is AEStronglyMeasurable (via commutativity).

Русский

Если f является AEStronglyMeasurable, тогда g*f является AEStronglyMeasurable тогда и только тогда, когда g является AEStronglyMeasurable (через коммутативную структуру).

LaTeX

$$$(\text{hf}) \Rightarrow (AEStronglyMeasurable\ (g * f) μ \iff AEStronglyMeasurable\ g μ)$$$

Lean4

@[to_additive]
theorem mul_iff_left [CommGroup β] [IsTopologicalGroup β] (hf : AEStronglyMeasurable[m] f μ) :
    AEStronglyMeasurable[m] (g * f) μ ↔ AEStronglyMeasurable[m] g μ :=
  mul_comm g f ▸ AEStronglyMeasurable.mul_iff_right hf

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