prod — Mathlib

English

There is a product MeasurableSpace structure on α × β defined as the smallest σ-algebra making both projections measurable.

Русский

Существует пространство измеримости произведения на α × β, минимальной сигма‑алгеброй, делающей обе проекции измеримыми.

LaTeX

$$$$ \mathcal{M}_{\alpha \times \beta} = \sigma\{ A \times B : A \in \mathcal{M}_{\alpha}, B \in \mathcal{M}_{\beta} \} $$$$

Lean4

/-- A `MeasurableSpace` structure on the product of two measurable spaces. -/
def prod {α β} (m₁ : MeasurableSpace α) (m₂ : MeasurableSpace β) : MeasurableSpace (α × β) :=
  m₁.comap Prod.fst ⊔ m₂.comap Prod.snd

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