union_mem_measurableCylinders — Mathlib

English

The union of two measurable cylinder sets is measurable.

Русский

Объединение двух измеримых цилиндров измеримо.

LaTeX

$$$ s,t \\in \\mathrm{measurableCylinders}(\\alpha) \\Rightarrow s \\cup t \\in \\mathrm{measurableCylinders}(\\alpha). $$$

Lean4

theorem union_mem_measurableCylinders (hs : s ∈ measurableCylinders α) (ht : t ∈ measurableCylinders α) :
    s ∪ t ∈ measurableCylinders α := by
  rw [union_eq_compl_compl_inter_compl]
  exact
    compl_mem_measurableCylinders
      (inter_mem_measurableCylinders (compl_mem_measurableCylinders hs) (compl_mem_measurableCylinders ht))

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