isPiSystem_generatePiSystem

Mathlib.MeasureTheory.PiSystem

URI: https://scilib.ai/kg/mathlib#isPiSystem_generatePiSystem

← MathLib Explorer

English

The generated π-system by a subset S, generatePiSystem(S), is itself a π-system.

Русский

Сгенерированная π-система generatePiSystem(S) является π-системой.

LaTeX

$$$$ \mathrm{IsPiSystem}\big(\mathrm{generatePiSystem}(S)\big) $$$$

Lean4

theorem isPiSystem_generatePiSystem (S : Set (Set α)) : IsPiSystem (generatePiSystem S) := fun _ h_s _ h_t h_nonempty =>
  generatePiSystem.inter h_s h_t h_nonempty

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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