aecover_Icc

Mathlib.MeasureTheory.Integral.IntegralEqImproper

URI: https://scilib.ai/kg/mathlib#MeasureTheory.aecover_Icc

← MathLib Explorer

English

Under joint assumptions on endpoints a_i ≤ b_i, the interval Icc(a_i, b_i) forms an AECover.

Русский

При условии a_i ≤ b_i интервал Icc(a_i, b_i) образует покрытие.

LaTeX

$$$\\text{AECover } μ l (i \\mapsto \\mathbf{Icc}(a_i,b_i))$$$

Lean4

theorem aecover_Icc (ha : Tendsto a l atBot) (hb : Tendsto b l atTop) : AECover μ l fun i => Icc (a i) (b i) :=
  (aecover_Ici ha).inter (aecover_Iic hb)

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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