measurable_IicProdIoc — Mathlib

English

If each fiber X i is provided with a measurable space, then the gluing map IicProdIoc is a measurable function from the product space (Iic a) × (Ioc a b) to the index space Iic b.

Русский

Если для каждого i задано пространство измеримости, то функция IicProdIoc является измеримой из произведения (Iic a) × (Ioc a b) в пространство Iic b.

LaTeX

$$$\mathrm{Measurable}(\mathrm{IicProdIoc}(m,n))$$$

Lean4

@[measurability, fun_prop]
theorem measurable_IicProdIoc {m n : ι} : Measurable (IicProdIoc (X := X) m n) :=
  by
  refine measurable_pi_lambda _ (fun i ↦ ?_)
  by_cases h : i ≤ m
  · simpa [IicProdIoc, h] using measurable_fst.eval
  · simpa [IicProdIoc, h] using measurable_snd.eval

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