measurableSet_uIoc

Mathlib.MeasureTheory.Constructions.BorelSpace.Order

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

English

Similarly, the set uIoc(a, b) is a measurable subset for all a, b in α.

Русский

Аналогично, множество uIoc(a, b) измеримо для всех a, b ∈ α.

LaTeX

$$$\MeasurableSet(\mathrm{uIoc}(a,b))$$$

Lean4

@[measurability]
theorem measurableSet_uIoc : MeasurableSet (uIoc a b) :=
  measurableSet_Ioc

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

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

Разделы

Аффилиация

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