instBorelSpaceRealOfFinite — Mathlib

English

If ι is finite, then the Euclidean space ℝ^ι carries a canonical Borel structure (is a Borel space).

Русский

Если ι конечен, то евклидово пространство ℝ^ι имеет каноническую Борелеву структуру (является Борелевым пространством).

LaTeX

$$$[Finite\;\iota]\Rightarrow BorelSpace(\mathbb{R}^{\iota})$$$

Lean4

instance [Finite ι] : BorelSpace (EuclideanSpace ℝ ι) :=
  Pi.borelSpace

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