prod — Mathlib

English

The product of two standard Borel spaces is again a standard Borel space.

Русский

Произведение двух стандартных Борелевых пространств снова стандартно Борелово пространство.

LaTeX

$$$ \text{StandardBorelSpace}(α × β) $$$

Lean4

/-- A product of two standard Borel spaces is standard Borel. -/
instance prod [StandardBorelSpace α] [StandardBorelSpace β] : StandardBorelSpace (α × β) :=
  letI := upgradeStandardBorel α
  letI := upgradeStandardBorel β
  inferInstance

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