measurable_restrict₂_apply — Mathlib

English

If s ⊆ t ⊆ α and f: t → γ is measurable, then the restriction of f to s, treated as a function s → γ, is measurable.

Русский

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

LaTeX

$$$\\mathrm{Measurable\\text{(restrict}_2(hst,f))}$, i.e. $\\mathrm{Measurable}(\\text{restrict}_2(hst)\\, f)$$$

Lean4

@[measurability, fun_prop]
theorem measurable_restrict₂_apply {s t : Set α} (hst : s ⊆ t) {f : t → γ} (hf : Measurable f) :
    Measurable (restrict₂ (π := fun _ ↦ γ) hst f) :=
  hf.comp (measurable_inclusion hst)

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