measurableSet — Mathlib

English

If s is in measurable cylinders, then the complement s^c is also in measurable cylinders.

Русский

Если множество s принадлежит измеримым цилиндрам, то и его комплемент s^c принадлежит измеримым цилиндрам.

LaTeX

$$$ s \\in \\mathrm{measurableCylinders}(\\alpha) \\Rightarrow s^{c} \\in \\mathrm{measurableCylinders}(\\alpha) $$$

Lean4

theorem measurableSet (ht : t ∈ measurableCylinders α) : MeasurableSet (measurableCylinders.set ht) :=
  ((mem_measurableCylinders t).mp ht).choose_spec.choose_spec.left

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