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