inf_of_left

Mathlib.MeasureTheory.Integral.IntegrableOn

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

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_left (hl : IntegrableAtFilter f l μ) : IntegrableAtFilter f (l ⊓ l') μ :=
  hl.filter_mono inf_le_left

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

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

Разделы

Аффилиация

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