borelSpace — Mathlib

English

The Borel measurable structure on the Lp-type WithLp p (X × Y) coincides with the Borel structure of the product X × Y (under suitable measurability/topology hypotheses).

Русский

Борелевская структура пространства WithLp p (X × Y) совпадает с борелевской структурой произведения X × Y (при соответствующих предположениях про измеримость и топологию).

LaTeX

$$$\\mathcal{B}\\bigl(\\mathrm{WithLp}(p, X\\times Y)\\bigr)=\\mathcal{B}(X\\times Y)\\,,$$$

Lean4

instance borelSpace : BorelSpace (WithLp p (X × Y)) :=
  inferInstanceAs <| BorelSpace (X × Y)

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