integrable — Mathlib

English

If f is integrable on a set s with respect to μ, then f is integrable with respect to the restricted measure μ|s.

Русский

Если функция интегрируема на множесте s по мере μ, то она интегрируема по ограниченной мере μ|s.

LaTeX

$$$ \text{IntegrableOn}(f,s,\mu) \Rightarrow \text{Integrable}(f,\mu\restriction s) $$$

Lean4

theorem integrable (h : IntegrableOn f s μ) : Integrable f (μ.restrict s) :=
  h

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