measurable_restrict_apply — Mathlib

English

If i = i' and f: β → X_i is measurable, then the map x ↦ (congr_arg X h).mp (f x) from β to X_i' is measurable.

Русский

Пусть i = i' и f: β → X_i измерима; тогда отображение x ↦ (congr_arg X h).mp (f x) из β в X_i' измеримо.

LaTeX

$$$\\mathrm{Measurable}((\\mathrm{congr\\_arg}\\ X\\ h).\\mathrm{mp})$$$

Lean4

@[measurability, fun_prop]
theorem measurable_restrict_apply (s : Finset α) {f : α → γ} (hf : Measurable f) : Measurable (s.restrict f) :=
  hf.comp measurable_subtype_coe

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