compl_mem_measurableCylinders — Mathlib

English

If s is in measurableCylinders α, then its complement s^c is also in measurableCylinders α.

Русский

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

LaTeX

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

Lean4

theorem compl_mem_measurableCylinders (hs : s ∈ measurableCylinders α) : sᶜ ∈ measurableCylinders α :=
  by
  rw [mem_measurableCylinders] at hs ⊢
  obtain ⟨s, S, hS, rfl⟩ := hs
  refine ⟨s, Sᶜ, hS.compl, ?_⟩
  rw [compl_cylinder]

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