pi_countable — Mathlib

English

A countable product of standard Borel spaces is standard Borel.

Русский

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

LaTeX

$$$ \text{StandardBorelSpace}(\prod_{n\in \mathbb{N}} α_n) $ with countable index$$

Lean4

/-- A product of countably many standard Borel spaces is standard Borel. -/
instance pi_countable {ι : Type*} [Countable ι] {α : ι → Type*} [∀ n, MeasurableSpace (α n)]
    [∀ n, StandardBorelSpace (α n)] : StandardBorelSpace (∀ n, α n) :=
  letI := fun n => upgradeStandardBorel (α n)
  inferInstance

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