measurableSet_coe — Mathlib

English

For a Box I on a countable index set ι, the subset I (viewed as a subset of ι → ℝ) is measurable.

Русский

Для коробки I над счётным множеством индексов ι множество I (рассматриваемое как подмножество ι→ℝ) является измеримым.

LaTeX

$$$\\text{MeasurableSet}(I)$$$

Lean4

theorem measurableSet_coe : MeasurableSet (I : Set (ι → ℝ)) :=
  by
  rw [coe_eq_pi]
  exact MeasurableSet.univ_pi fun i => measurableSet_Ioc

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