measurableSet_uIcc — Mathlib

English

For any α with an appropriate topology and measurable space, the set uIcc(a, b) is a measurable subset for all a, b ∈ α.

Русский

Для любого α с подходящей топологией и измерялым пространством множество uIcc(a, b) измеримо для всех a, b ∈ α.

LaTeX

$$$\MeasurableSet(\mathrm{uIcc}(a,b))$$$

Lean4

@[measurability]
theorem measurableSet_uIcc : MeasurableSet (uIcc a b) :=
  measurableSet_Icc

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