measurable_restrict_apply — Mathlib

English

If f: α → γ is measurable, then its restriction to a subset s ⊆ α, viewed as a function s → γ, is measurable.

Русский

Если f: α → γ измерима, то её ограничение на подмножество s ⊆ α, рассматриваемое как функция s → γ, также измеримо.

LaTeX

$$$\\mathrm{Measurable}(f) \\Rightarrow \\mathrm{Measurable}(f|_s)$$$

Lean4

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

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