mul_iff_right — Mathlib

English

If f is AEStronglyMeasurable, then f*g is AEStronglyMeasurable iff g is AEStronglyMeasurable (under commutative group structure).

Русский

Если f является AEStronglyMeasurable, то f·g является AEStronglyMeasurable тогда и только тогда, когда g является AEStronglyMeasurable (при условии коммутированной группы).

LaTeX

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

Lean4

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

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