isPiSystem_pi — Mathlib

English

Boxes form a π-system: the image under univ.pi of univ.pi of C is a π-system when each C_i is a π-system of sets.

Русский

Коробки образуют π-систему: образ Set.univ.pi из Set.univ.pi C является π-системой, если каждая C_i — π-система множеств.

LaTeX

$$$\\text{IsPiSystem}(\\mathrm{Set.image} \\mathrm{Set.univ.pi} (\\mathrm{Set.univ.pi} C))$$$

Lean4

/-- Boxes form a π-system. -/
theorem isPiSystem_pi [∀ i, MeasurableSpace (α i)] :
    IsPiSystem (pi univ '' pi univ fun i => {s : Set (α i) | MeasurableSet s}) :=
  IsPiSystem.pi fun _ => isPiSystem_measurableSet

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