measurable_eq_mp — Mathlib

English

For δ with a family X, if i = i' and f: β → X_i is measurable, then the function β → X_i' given by f mapped through the transport along h is measurable.

Русский

Для индексов δ, имеющих семейство X, если i = i' и f: β → X_i измерима, то функция β → X_i', получаемая перенесением через h, измерима.

LaTeX

$$$\\mathrm{Measurable}(f) \\Rightarrow \\mathrm{Measurable}( (\\congr_arg X h).mp \\circ f)$$$

Lean4

theorem measurable_eq_mp {i i' : δ} (h : i = i') : Measurable (congr_arg X h).mp :=
  by
  cases h
  exact measurable_id

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