isSetRing_measurableCylinders

Mathlib.MeasureTheory.Constructions.ProjectiveFamilyContent

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

English

The collection of measurable cylinders forms a set algebra.

Русский

Множество измеримых цилиндров образует множество-алгебру.

LaTeX

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

Lean4

theorem isSetRing_measurableCylinders : IsSetRing (measurableCylinders α) :=
  isSetAlgebra_measurableCylinders.isSetRing

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

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

Разделы

Аффилиация

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