measurableSMul₂_iterateMulAct — Mathlib

English

A compositional version: if f is Measurable and g is Measurable, then the uncurry composition yields a measurable function.

Русский

Композиционная версия: если f и g измеримы, то развёрнутое отображение измеримо.

LaTeX

$$$\text{Measurable}(\text{uncurry}(f))$ и т.д.$$

Lean4

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

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