English
A compositional variant: if f,g,h are appropriately measurable (with g : α → β → X, h : α → β), then the composite a ↦ (f a • g a) (h a) is measurable.
Русский
Композиционный вариант: если f,g,h измеримы в нужном виде, то отображение a ↦ (f(a) • g(a)) (h(a)) измеримо.
LaTeX
$$$\text{Measurable}(\lambda a. (f(a)\cdot g(a))(h(a)))$$$
Lean4
/-- Compositional version of `Measurable.smul` for use by `fun_prop`. -/
@[to_additive (attr := fun_prop) /-- Compositional version of `Measurable.vadd` for use by `fun_prop`. -/
]
theorem smul' [MeasurableSMul₂ M X] {f : α → β → M} {g : α → β → X} {h : α → β} (hf : Measurable ↿f)
(hg : Measurable ↿g) (hh : Measurable h) : Measurable fun a ↦ (f a • g a) (h a) := by dsimp; fun_prop
