integrable_zero — Mathlib

English

The zero AEEqFun is integrable with respect to any μ; i.e., the zero function in the AEEqFun space has finite integral.

Русский

Нулевая функция в пространстве AEEqFun интегрируема по любой мере μ; т.е. нулевая функция имеет конечный интеграл.

LaTeX

$$$\mathrm{Integrable}(0 : \alpha \to_{\mu} \varepsilon')$$$

Lean4

theorem integrable_zero : Integrable (0 : α →ₘ[μ] ε') :=
  (MeasureTheory.integrable_zero α ε' μ).congr (coeFn_mk _ _).symm

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