singleton

Mathlib.MeasureTheory.MeasurableSpace.Defs

URI: https://scilib.ai/kg/mathlib#MeasurableSet.singleton

English

For any α with a measurable space and a measurable singleton class, the singleton set {a} is measurable.

Русский

Пусть задано пространство измеримости на множество; множество {a} измеримо.

LaTeX

$$$\mathrm{MeasurableSet}({a})$$$

Lean4

@[simp]
theorem singleton [MeasurableSpace α] [MeasurableSingletonClass α] (a : α) : MeasurableSet { a } :=
  measurableSet_singleton a

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

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

Разделы

Аффилиация

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