borelSpace — Mathlib

English

If each X_i has a Borel structure and the appropriate topological/measure-theoretic hypotheses hold, then the product space PiLp p X carries a canonical Borel structure (i.e., BorelSpace).

Русский

Если каждый X_i имеет бореловаe строение и соблюдены необходимые топологические/измерительные условия, то пространство PiLp p X обладает каноническим бореловым строением.

LaTeX

$$$\\mathrm{BorelSpace}(\\PiLp(p, X))$$$

Lean4

instance borelSpace : BorelSpace (PiLp p X) :=
  inferInstanceAs <| BorelSpace (Π i, X i)

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