measure_Ioo_lt_top

Mathlib.MeasureTheory.Measure.Typeclasses.Finite

URI: https://scilib.ai/kg/mathlib#measure_Ioo_lt_top

English

μ(Ioo(a,b)) < ∞ for locally finite μ.

Русский

μ(Ioo(a,b)) < ∞ при локально конечной мере μ.

LaTeX

$$$$\mu((a,b)) < \infty.$$$$

Lean4

theorem measure_Ioo_lt_top : μ (Ioo a b) < ∞ :=
  (measure_mono Ioo_subset_Icc_self).trans_lt measure_Icc_lt_top

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

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

Разделы

Аффилиация

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