generatePiSystem

Mathlib.MeasureTheory.PiSystem

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

Lean4

/-- Given a collection `S` of subsets of `α`, then `generatePiSystem S` is the smallest
π-system containing `S`. -/
inductive generatePiSystem (S : Set (Set α)) : Set (Set α)
  | base {s : Set α} (h_s : s ∈ S) : generatePiSystem S s
  |
  inter {s t : Set α} (h_s : generatePiSystem S s) (h_t : generatePiSystem S t) (h_nonempty : (s ∩ t).Nonempty) :
    generatePiSystem S (s ∩ t)

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

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

Разделы

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

Аффилиация

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