isPiSystem_prod — Mathlib

English

Rectangles form a π-system: the intersection of two rectangles s1 × t1 and s2 × t2 is again a rectangle (s1 ∩ s2) × (t1 ∩ t2) with s1,s2 and t1,t2 measurable.

Русский

Прямоугольники образуют π-систему: пересечение двух прямоугольников s1 × t1 и s2 × t2 равно (s1 ∩ s2) × (t1 ∩ t2), где s1,s2 и t1,t2 измеримы.

LaTeX

$$$IsPiSystem\Bigl(\{ s \times t \mid s \text{ MeasurableSet in } α,\ t \text{ MeasurableSet in } β \}\Bigr)$$$

Lean4

/-- Rectangles form a π-system. -/
theorem isPiSystem_prod : IsPiSystem (image2 (· ×ˢ ·) {s : Set α | MeasurableSet s} {t : Set β | MeasurableSet t}) :=
  isPiSystem_measurableSet.prod isPiSystem_measurableSet

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