isPiSystem_measurableCylinders

Mathlib.MeasureTheory.Constructions.Cylinders

URI: https://scilib.ai/kg/mathlib#MeasureTheory.isPiSystem_measurableCylinders

English

The family of measurable cylinders forms a Pi-system.

Русский

Семейство измеримых цилиндров образует Pi-систему.

LaTeX

$$$ \\text{IsPiSystem}(\\mathrm{measurableCylinders}(\\alpha)). $$$

Lean4

theorem isPiSystem_measurableCylinders : IsPiSystem (measurableCylinders α) := fun _ hS _ hT _ ↦
  inter_mem_measurableCylinders hS hT

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

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

Разделы

Аффилиация

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