measurableSet_Iio

Mathlib.MeasureTheory.Constructions.BorelSpace.Order

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

English

For any a, the open ray Iio a = {x ∈ α | x < a} is measurable.

Русский

Для любого a множество Iio a = {x < a} измеримо.

LaTeX

$$$\text{MeasurableSet}(\{x \in \alpha : x < a\})$.$$

Lean4

@[simp, measurability]
theorem measurableSet_Iio : MeasurableSet (Iio a) :=
  isOpen_Iio.measurableSet

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

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

Разделы

Аффилиация

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