measurableSMul_iterateMulAct — Mathlib

English

If [MeasurableSMul₂ M X], and f,g are measurable, then the pointwise smul x ↦ f(x) • g(x) is measurable.

Русский

Если есть измеримое двумерное действие SMul и функции f,g измеримы, то точечное произведение измеримо.

LaTeX

$$$\text{smul}([MeasurableSMul_2 M X])\; (f,g) \Rightarrow \text{Measurable}(x \mapsto f(x) \cdot g(x))$$$

Lean4

@[to_additive (attr := simp)]
theorem measurableSMul_iterateMulAct : MeasurableSMul (IterateMulAct f) α ↔ Measurable f :=
  ⟨fun _ ↦ measurable_const_smul (IterateMulAct.mk (f := f) 1), fun h ↦
    have := h.measurableSMul₂_iterateMulAct;
    inferInstance⟩

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