mul_iff_right — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

@[to_additive]
theorem mul_iff_right [CommGroup β] [IsTopologicalGroup β] (hf : StronglyMeasurable f) :
    StronglyMeasurable (f * g) ↔ StronglyMeasurable g :=
  ⟨fun h ↦ show g = f * g * f⁻¹ by simp only [mul_inv_cancel_comm] ▸ h.mul hf.inv, fun h ↦ hf.mul h⟩

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