of_subsingleton_codomain — Mathlib

English

If the codomain is a singleton, then any function is integrable on any set.

Русский

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

LaTeX

$$$[Subsingleton\;\varepsilon'] \{f:\alpha\to\varepsilon'\} : \mathrm{IntegrableOn} f s \mu$$

Lean4

@[simp]
theorem of_subsingleton_codomain [Subsingleton ε'] {f : α → ε'} : IntegrableOn f s μ :=
  Integrable.of_subsingleton_codomain

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