locallyIntegrable

Mathlib.MeasureTheory.Function.LocallyIntegrable

URI: https://scilib.ai/kg/mathlib#Antitone.locallyIntegrable

English

If f is antitone on s, then f is LocallyIntegrableOn s μ when μ is locally finite.

Русский

Если f антитононна на s, то LocallyIntegrableOn(f,s,μ) при локально конечной мере μ.

LaTeX

$$$\text{LocallyIntegrableOn}(f,s,\mu)$$$

Lean4

theorem locallyIntegrable [IsLocallyFiniteMeasure μ] (hanti : Antitone f) : LocallyIntegrable f μ :=
  hanti.dual_right.locallyIntegrable

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru