le_eventuallyMeasurableSpace

Mathlib.MeasureTheory.MeasurableSpace.EventuallyMeasurable

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

English

The original measurable space m is contained in the eventualMeasurableSpace m l.

Русский

Начальное пространство измеримости m вложено в пространство eventuallyMeasurableSpace(m,l).

LaTeX

$$$m \leqslant \text{eventuallyMeasurableSpace}(m,l).$$$

Lean4

theorem le_eventuallyMeasurableSpace : m ≤ eventuallyMeasurableSpace m l := fun _ hs => hs.eventuallyMeasurableSet

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

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

Разделы

Аффилиация

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