eq_mp — Mathlib

English

For a family X indexed by δ and a predicate p on δ, the coordinate-reindexing map on the product space along p is measurable.

Русский

Для семейства X, индексируемого δ, и предиката p на δ, отображение реиндексации координат по p измеримо.

LaTeX

$$$\\mathrm{Measurable}(\\mathrm{Equiv.piEquivPiSubtypeProd}\\ p\\ X)$$$

Lean4

theorem eq_mp {β} [MeasurableSpace β] {i i' : δ} (h : i = i') {f : β → X i} (hf : Measurable f) :
    Measurable fun x => (congr_arg X h).mp (f x) :=
  (measurable_eq_mp X h).comp hf

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