restrict — Mathlib

English

If a function f has finite integral with respect to a measure μ, then for every subset s of the space, f also has finite integral with respect to the restricted measure μ|_s.

Русский

Если функция f имеет конечный интеграл по мере μ, то для любого подмножества s она также имеет конечный интеграл по ограниченной мере μ|_s.

LaTeX

$$$\operatorname{HasFiniteIntegral}(f, \mu) \Rightarrow \operatorname{HasFiniteIntegral}(f, \mu\restriction s)$$$

Lean4

@[fun_prop]
theorem restrict (h : HasFiniteIntegral f μ) {s : Set α} : HasFiniteIntegral f (μ.restrict s) :=
  by
  refine lt_of_le_of_lt ?_ h
  simpa [Measure.restrict_univ] using lintegral_mono_set (subset_univ s)

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