measurableSet_Ico

Mathlib.MeasureTheory.Constructions.BorelSpace.Order

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

English

For all a ≤ b, the half-open interval Ico(a,b) is measurable.

Русский

Для любых a ≤ b полу-открытый интервал Ico(a,b) измерим.

LaTeX

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

Lean4

@[simp, measurability]
theorem measurableSet_Ico : MeasurableSet (Ico a b) :=
  measurableSet_Ici.inter measurableSet_Iio

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

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

Разделы

Аффилиация

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