subset_generatePiSystem_self

Mathlib.MeasureTheory.PiSystem

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

English

Every element of a π-system S is contained in generatePiSystem S.

Русский

Каждый элемент π-системы S принадлежит generatePiSystem S.

LaTeX

$$$$ S \subseteq \mathrm{generatePiSystem}(S) $$$$

Lean4

theorem subset_generatePiSystem_self (S : Set (Set α)) : S ⊆ generatePiSystem S := fun _ => generatePiSystem.base

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

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

Разделы

Аффилиация

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