aemeasurable_pi_lambda — Mathlib

English

If f: α → (δ → X δ) satisfies that for each a, the a-th coordinate is AEMeasurable, then f is AEMeasurable.

Русский

Если f: α → (δ → X δ) удовлетворяет условию, что для каждого a координатная функция AEMeasurable, тогда сама функция f AEMeasurable.

LaTeX

$$$(\forall a, AEMeasurable(\lambda c. f c a)\mu) \rightarrow AEMeasurable f \mu$$

Lean4

@[fun_prop, aesop safe 100 apply (rule_sets := [Measurable])]
theorem aemeasurable_pi_lambda (f : α → Π a, X a) (hf : ∀ a, AEMeasurable (fun c ↦ f c a) μ) : AEMeasurable f μ :=
  aemeasurable_pi_iff.mpr hf

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