measurable_pi_iff — Mathlib

English

A function g: α → ∀ a, X a is measurable if and only if for every a, the coordinate map x ↦ g x a is measurable.

Русский

Функция g: α → ∀ a, X(a) измерима тогда и только тогда, когда для каждого a сопряжённая координатная функция x ↦ g(x)(a) измерима.

LaTeX

$$$\operatorname{Measurable} g \iff \forall a, \operatorname{Measurable}(\lambda x. g x a)$$$

Lean4

theorem measurable_pi_iff {g : α → ∀ a, X a} : Measurable g ↔ ∀ a, Measurable fun x => g x a := by
  simp_rw [measurable_iff_comap_le, MeasurableSpace.pi, MeasurableSpace.comap_iSup, MeasurableSpace.comap_comp,
    Function.comp_def, iSup_le_iff]

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