measurable_pi_lambda — Mathlib

English

A function f: α → ∀ a, X a is measurable if for all a, the projection onto the a-th coordinate is measurable.

Русский

Функция f: α → ∀ a, X(a) измерима, если для каждого a проекция на a-ю координату измерима.

LaTeX

$$$\text{Measurable}(f) \Leftarrow \forall a, \text{Measurable}(\lambda x. f x a)$$$$

Lean4

@[fun_prop, aesop safe 100 apply (rule_sets := [Measurable])]
theorem measurable_pi_lambda (f : α → ∀ a, X a) (hf : ∀ a, Measurable fun c => f c a) : Measurable f :=
  measurable_pi_iff.mpr hf

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