measurableSet_Ici

Mathlib.MeasureTheory.Constructions.BorelSpace.Order

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

English

For every a ∈ α, the right ray {x ∈ α | x ≥ a} is a measurable set.

Русский

Для каждого a ∈ α множество {x ∈ α | x ≥ a} измеримо.

LaTeX

$$$\text{MeasurableSet}([a, \infty))$.$$

Lean4

@[simp, measurability]
theorem measurableSet_Ici : MeasurableSet (Ici a) :=
  isClosed_Ici.measurableSet

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

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

Разделы

Аффилиация

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