mul_iff_left — Mathlib

English

For a commutative group β with a topological group structure, if f is strongly measurable, then g*f is strongly measurable iff g is strongly measurable.

Русский

Для коммутативной группы β с топологической группой, если f сильно измерим, то g*f сильно измеримо тогда и только тогда, когда g сильно измеримо.

LaTeX

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

Lean4

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

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