inf_of_right

Mathlib.MeasureTheory.Integral.IntegrableOn

URI: https://scilib.ai/kg/mathlib#MeasureTheory.IntegrableAtFilter.inf_of_right

English

IntegrableAtFilter f l μ implies IntegrableAtFilter f (l' ⊓ l) μ.

Русский

Из интегрируемости следует интегрируемость на l' ∧ l.

LaTeX

$$$\\operatorname{IntegrableAtFilter}(f, l, \\mu) \\Rightarrow \\operatorname{IntegrableAtFilter}(f, l' \\cap l, \\mu).$$$

Lean4

theorem inf_of_right (hl : IntegrableAtFilter f l μ) : IntegrableAtFilter f (l' ⊓ l) μ :=
  hl.filter_mono inf_le_right

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

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

Разделы

Аффилиация

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