generateFrom_singleton_univ

Mathlib.MeasureTheory.MeasurableSpace.Defs

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

English

The generated sigma-algebra from the singleton {univ} is the bottom (trivial) sigma-algebra.

Русский

Порожденная сигма-алгебра из множества { Univ } равна нижней сигма-алгебре.

LaTeX

$$$\\operatorname{generateFrom}\\{\\operatorname{Set.univ}\\} = \\perp$$$

Lean4

theorem generateFrom_singleton_univ : generateFrom { Set.univ } = (⊥ : MeasurableSpace α) :=
  bot_unique <| generateFrom_le <| by simp

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

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

Разделы

Аффилиация

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