measurableSet_top

Mathlib.MeasureTheory.MeasurableSpace.Defs

URI: https://scilib.ai/kg/mathlib#MeasurableSpace.measurableSet_top

English

In the top sigma-algebra every subset is measurable.

Русский

В верхней сигма-алгебре каждый подмножество измеримо.

LaTeX

$$$\\text{MeasurableSet}[\\top] s$ for all $s$$$

Lean4

@[simp, measurability]
theorem measurableSet_top {s : Set α} : MeasurableSet[⊤] s :=
  trivial

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

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

Разделы

Аффилиация

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