of_finite — Mathlib

English

If α is finite, then any measurable f is integrable under certain typical finite measure assumptions.

Русский

Если множество конечно и мера конечна, то любая измеримая функция интегрируема.

LaTeX

$$$\operatorname{of_finite} \Rightarrow \operatorname{Integrable}(f, \mu)$$$

Lean4

@[fun_prop, simp]
theorem of_finite [Finite α] [MeasurableSingletonClass α] [IsFiniteMeasure μ] {f : α → β} : Integrable f μ :=
  ⟨.of_discrete, .of_finite⟩

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