has_univ

Mathlib.MeasureTheory.PiSystem

URI: https://scilib.ai/kg/mathlib#MeasurableSpace.DynkinSystem.has_univ

English

Every Dynkin system contains the universal set univ.

Русский

Каждая Dynkin-система содержит вселенное множество univ.

LaTeX

$$$\forall d,\ d.Has(\mathrm{univ})$$$

Lean4

theorem has_univ : d.Has univ := by simpa using d.has_compl d.has_empty

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

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

Разделы

Аффилиация

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