measurable_IocProdIoc — Mathlib

English

The map IocProdIoc (a,b,c) is measurable with respect to the product σ-algebra on the index family.

Русский

Функция IocProdIoc(a,b,c) измерима относительно произведённой сигма-алгебры индекса.

LaTeX

$$$Measurable( IocProdIoc (X := X) a b c )$$$

Lean4

@[measurability, fun_prop]
theorem measurable_IocProdIoc [∀ i, MeasurableSpace (X i)] {a b c : ι} : Measurable (IocProdIoc (X := X) a b c) :=
  by
  refine measurable_pi_lambda _ (fun i ↦ ?_)
  by_cases h : i ≤ b
  · simpa [IocProdIoc, h] using measurable_fst.eval
  · simpa [IocProdIoc, h] using measurable_snd.eval

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