isPiSystem_measurableSet

Mathlib.MeasureTheory.PiSystem

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

English

The collection of all measurable sets forms a π-system.

Русский

Объединение всех измеримых множеств образует π-систему.

LaTeX

$$IsPiSystem {s : Set α | MeasurableSet s}$$

Lean4

theorem isPiSystem_measurableSet {α : Type*} [MeasurableSpace α] : IsPiSystem {s : Set α | MeasurableSet s} :=
  fun _ hs _ ht _ => hs.inter ht

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

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

Разделы

Аффилиация

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