pi_le_borel_pi — Mathlib

English

The type of all functions from ι to X_i has a Borel space structure when ι is countable and each X_i is Borel.

Русский

Тип всех функций из ι в X_i имеет борелевское пространство, если ι счётно и каждый X_i борелевское пространство.

LaTeX

$$$\\mathrm{Pi}.\\mathrm{borelSpace}$$$

Lean4

theorem pi_le_borel_pi {ι : Type*} {X : ι → Type*} [∀ i, TopologicalSpace (X i)] [∀ i, MeasurableSpace (X i)]
    [∀ i, BorelSpace (X i)] : MeasurableSpace.pi ≤ borel (∀ i, X i) :=
  by
  have : ‹∀ i, MeasurableSpace (X i)› = fun i => borel (X i) := funext fun i => BorelSpace.measurable_eq
  rw [this]
  exact iSup_le fun i => comap_le_iff_le_map.2 <| (continuous_apply i).borel_measurable

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